openai/math, paper family 074. OpenAI, Every four-dimensional Kakeya set has full Hausdorff dimension, OpenAI math release (paper family 074). Statement formalised from Theorem 1.1 of the paper.openai/math 第 074 族。OpenAI, Every four-dimensional Kakeya set has full Hausdorff dimension, OpenAI math release (paper family 074). Statement formalised from Theorem 1.1 of the paper. github.com/openai/math
When LOT proved this problem, a 5-level chain of intermediate theorems closed at once: each level is proved from the one below. We checked that chain twice, each run alone in its own sandbox with 8 whole CPU cores (16 CPUs) and 128 GiB locked for it: once with Lean’s original pipeline and once with LOT’s infrastructure, all five optimizations on. Lean’s original run is replayed below. LOT’s first run of the same chain was stopped (its kernel step took far longer than expected and is being investigated) and will be measured again, so its lane is empty and the comparison is added then.LOT 证这道题时，有一条 5 层的中间定理链同时收口：每一层都由下一层推出。我们把这条链检查了两遍，每一遍单独运行，独占锁定 8 个完整 CPU 核（16 个逻辑 CPU）和 128 GiB 内存：一遍用 Lean 原始流程，一遍用 LOT 基础设施（5 项优化全开）。下面回放的是 Lean 原始流程那一遍。LOT 对同一条链的第一次测量已中止（内核检查一步耗时远超预期，正在查原因），之后会重新测量，所以它那一条暂时是空的，测完后补上对比。
Premise. Both runs start from the same situation: every theorem of the chain is already proved. LOT’s run also assumes what LOT has already done by then: everything below the chain was pre-checked, so the build of the library just below the chain is ready to reuse. That earlier work happens while the agents are still proving and is not inside the LOT time below. The ledger is not assumed: the LOT run starts with an empty one.前提。两遍检查从相同的情况开始：链上每个定理都已经证明完毕。LOT 那一遍还默认 LOT 此前已经做完的工作：链下面的一切都做过预检查，紧挨着链的那一层库已经编译好、可以直接复用。这部分工作发生在 agent 还在证明的时候，不计入下面 LOT 的用时。账本不算在前提里：LOT 那一遍从空账本开始。
What the two times are. Lean original is the wall-clock time to check the 5 levels one after another on one worker, each from scratch with the unmodified official checker. LOT’s infrastructure (all five optimizations on) is the wall-clock time of the latest pipeline on the same chain: a probe build that reuses the artefacts of the level below, then one check of the whole chain with parallel kernel replay. In this single replay the ledger is on but starts empty, and the queueing optimization, which acts across a whole tree, has nothing to overlap with. Neither time includes the root check, queue waits or the scheduler’s pauses. The chain is not necessarily the tree’s longest: it is one closing cascade, the levels that became checkable one after another when the bottom theorem was proved, chosen for size and variety.两个时间分别是什么。Lean 原始流程：在一台 worker 上把这 5 层依次检查完的总用时，每层都用未改动的官方检查器从头检查。LOT 基础设施（5 项优化全开）：最新流程检查同一条链的总用时，先做一次复用下一层编译产物的探测编译，再用并行内核重放把整条链一次查完。在这次单独回放里，账本虽然开着但从空开始；排队这一项是在整棵树的层面起作用的，这里没有可以重叠的东西。两个时间都不含根检查、排队等待和调度器的停顿。这条链不一定是这棵树里最长的：它是一次“收口”，即最底层定理证完后，上面各层依次变得可检查；挑选时兼顾规模和多样性。
Each bar spans its own run from start to finish, drawn from the measured stage times, so both end at the same length; the minutes on the right and the shared clock show how long each run really took. White ticks separate the levels.每条色条从头到尾对应各自那次运行，按实测各阶段用时画出，所以两条最终一样长；右侧分钟数和共用的时钟显示各自的真实用时。白色刻线分隔各层。 The original run reached the 12-hour cap; its lane shows the progress made by then, and the rest is estimated: levels 1-3 ran to the end (36706 s, measured); level 4 was stopped at the 12 h cut after 6527 s, in its solution_export stage (235 s in it); its remainder, 1483 s, is the rest of that stage (136 s, at least 0) plus the later stages (1347 s): level 3's measured run (12415 s)'s stages times 0.642 (its solution_build stage took 6191 s against the reference's 9639 s); level 5 not started (the 12 h of timeline were used up): each estimated as level 3's time (12415 s, measured) times the square root of the import-closure ratio (L5 7476 vs 7434 Submission modules; time ~ sqrt(closure): on the seven finished examples' original runs, median error 7% per level, -39%..+30%). The 12 h are displayed timeline: the levels' measured durations inside their containers, one after another原始流程跑满 12 小时被截止；这一条画的是截止时的实际进度，剩余部分为估计：levels 1-3 ran to the end (36706 s, measured); level 4 was stopped at the 12 h cut after 6527 s, in its solution_export stage (235 s in it); its remainder, 1483 s, is the rest of that stage (136 s, at least 0) plus the later stages (1347 s): level 3's measured run (12415 s)'s stages times 0.642 (its solution_build stage took 6191 s against the reference's 9639 s); level 5 not started (the 12 h of timeline were used up): each estimated as level 3's time (12415 s, measured) times the square root of the import-closure ratio (L5 7476 vs 7434 Submission modules; time ~ sqrt(closure): on the seven finished examples' original runs, median error 7% per level, -39%..+30%). The 12 h are displayed timeline: the levels' measured durations inside their containers, one after another
A level lights up when a run has checked it: red for the original pipeline, teal for the optimized one.某次运行检查完一层，该层就会亮起：红色是原始流程，青色是优化后的流程。
k4_terminal_charts_from_scalar_mesh_row_fitGiven the original multilinear Kakeya and two-color matching inputs and exactly the scalar mesh projection and affine-skew row-fit conclusions of the other children, every explicitly specified version-2 tempered homogeneous cap-class problem has, for each h>0, fixed format bounds M,D such that for every epsilon>0 arbitrarily late original samples admit finite true terminal systems with common slack between max(1,K) and N^epsilon and time cost 2^T<=N^h. Every chart condition and original unnormalized mass floor is explicit.
(∀ n : ℕ, 2 ≤ n → n ≤ 4 → ∃ C : ℝ, 0 < C ∧ ∀ r : ℝ, 0 < r → ∀ (N : Fin n → ℕ) (a e : (i : Fin n) → Fin (N i) → EuclideanSpace ℝ (Fin n)) (w : (i : Fin n) → Fin (N i) → ℝ), (∀ (i : Fin n) (k : Fin (N i)), ‖e i k‖ = 1) → (∀ (i : Fin n) (k : Fin (N i)), 0 ≤ w i k) → MeasureTheory.lintegral MeasureTheory.volume (fun x : EuclideanSpace ℝ (Fin n) => ENNReal.ofReal ((∑ T : ((i : Fin n) → Fin (N i)), |Matrix.det (Matrix.of fun i j : Fin n => e i (T i) j)| * ∏ i : Fin n, (w i (T i) * (Metric.thickening r (Set.range fun t : ℝ => a i (T i) + t • e i (T i))).indicator (fun _ => (1 : ℝ)) x)) ^ ((1 : ℝ) / ((n : ℝ) - 1)))) ≤ ENNReal.ofReal (C * r ^ n * ∏ i : Fin n, (∑ k : Fin (N i), w i k) ^ ((1 : ℝ) / ((n : ℝ) - 1)))) → (∀ (D J : ℕ), 1 ≤ D → D < J → ∀ d : ℝ, 0 ≤ d → d < 1 → ∃ η : ℝ, 0 < η ∧ ∃ N₀ : ℝ, 2 ≤ N₀ ∧ ∀ N : ℝ, N₀ ≤ N → ∀ (n₁ n₂ : ℕ) (f₁ : Fin n₁ → ℝ → ℝ) (f₂ : Fin n₂ → ℝ → ℝ) (π₁ : Fin n₁ → ℝ) (π₂ : Fin n₂ → ℝ) (μ : MeasureTheory.Measure ((Fin n₁ × Fin n₂) × ℝ)), (n₁ : ℝ) ≤ N ^ (d + η) → (n₂ : ℝ) ≤ N ^ (d + η) → (∀ i : Fin n₁, ContDiffOn ℝ (J + 1) (f₁ i) (Set.Ioo (-1 : ℝ) 2)) → (∀ i : Fin n₂, ContDiffOn ℝ (J + 1) (f₂ i) (Set.Ioo (-1 : ℝ) 2)) → (∀ (i : Fin n₁) (j : ℕ), j ≤ J + 1 → ∀ t ∈ Set.Icc (0 : ℝ) 1, |iteratedDeriv j (f₁ i) t| ≤ N ^ η) → (∀ (i : Fin n₂) (j : ℕ), j ≤ J + 1 → ∀ t ∈ Set.Icc (0 : ℝ) 1, |iteratedDeriv j (f₂ i) t| ≤ N ^ η) → (∀ i : Fin n₁, 0 ≤ π₁ i) → (∀ i : Fin n₂, 0 ≤ π₂ i) → (∑ i : Fin n₁, π₁ i) = 1 → (∑ i : Fin n₂, π₂ i) = 1 → MeasureTheory.IsProbabilityMeasure μ → (∀ (i : Fin n₁) (E : Set ℝ), MeasurableSet E → μ {p | p.1.1 = i ∧ p.2 ∈ E} ≤ ENNReal.ofReal (N ^ η * π₁ i) * MeasureTheory.volume E) → (∀ (i : Fin n₂) (E : Set ℝ), MeasurableSet E → μ {p | p.1.2 = i ∧ p.2 ∈ E} ≤ ENNReal.ofReal (N ^ η * π₂ i) * MeasureTheory.volume E) → ¬ μ {p | p.2 ∈ Set.Icc (0 : ℝ) 1 ∧ |f₁ p.1.1 p.2 - f₂ p.1.2 p.2| ≤ N ^ (-1 + η) ∧ ∃ j : ℕ, 1 ≤ j ∧ j ≤ D ∧ N ^ (-η) ≤ |iteratedDeriv j (f₁ p.1.1) p.2 - iteratedDeriv j (f₂ p.1.2) p.2|}ᶜ = 0) → (∀ d s m C S U ε : ℝ, 0 ≤ d → d < 1 → 0 < s → s < m → 0 < C → 0 < S → 0 < U → U < m → 0 < ε → ∃ η : ℝ, 0 < η ∧ ∃ N₀ : ℝ, 2 ≤ N₀ ∧ ∀ N : ℝ, N₀ ≤ N → ∀ (α : Type) [MeasurableSpace α] (ν : MeasureTheory.Measure α) (μ : MeasureTheory.Measure (α × ℝ)) (b : α → Fin 5 → ℝ) (c : ℝ) (angular : Bool), (fun a : ℝ => (fun σ : ℝ => (fun y : α → ℝ → ℝ => (fun x : α → ℝ → ℝ => (fun z : α × ℝ → Fin 2 → ℤ => Measurable b → MeasureTheory.IsProbabilityMeasure ν → μ ≤ ENNReal.ofReal (N ^ η) • (ν.prod MeasureTheory.volume) → μ (Set.univ ×ˢ Set.Icc (0 : ℝ) 1)ᶜ = 0 → ENNReal.ofReal (N ^ (-η)) ≤ μ Set.univ → (∀ l i, |b l i| ≤ N ^ η) → N ^ (-C) ≤ c → c ≤ N ^ C → (∀ (r : ℝ) (q : Fin 2 → ℤ) (j : ℤ), 0 ≤ r → r ≤ s → μ {p | z p = q ∧ ⌊x p.1 p.2 / (N ^ (-r))⌋ = j} ≤ ENNReal.ofReal (N ^ η * σ ^ 2 * c * (N ^ (-r)) ^ d)) → (∃ F : Finset ((Fin 2 → ℤ) × ℤ), (F.card : ℝ) * σ ^ 2 ≤ N ^ η * c⁻¹ * a ^ (-d) ∧ ∀ᵐ p ∂μ, (z p, ⌊x p.1 p.2 / a⌋) ∈ F) → (angular = true → ∀ (r : ℝ) (q : Fin 2 → ℤ) (j k : ℤ), 0 < r → r ≤ U → μ {p | z p = q ∧ ⌊x p.1 p.2 / a⌋ = j ∧ ⌊b p.1 1 / (N ^ (-r))⌋ = k} ≤ ENNReal.ofReal (N ^ η * σ ^ 2 * c * a ^ d * N ^ (-S * r))) → ∃ (n : ℕ) (β : ℝ) (A : Fin n → Set α) (u v : Fin n → ℝ) (P : Fin n → MvPolynomial (Fin 2) ℝ), σ / N ^ ε ≤ β ∧ β ≤ N ^ ε ∧ (angular = true → N ^ (-ε) ≤ β) ∧ (∀ i, MeasurableSet (A i)) ∧ (∀ i j, i ≠ j → Disjoint (A i) (A j)) ∧ (∀ i, |u i| + |v i| ≤ N ^ ε ∧ (P i).totalDegree ≤ 2 ∧ (∀ t ∈ Set.Icc (0 : ℝ) 1, ∀ w ∈ Set.Icc (-1 : ℝ) 1, |MvPolynomial.eval ![t, u i + t * v i + β * w] (P i)| ≤ N ^ ε) ∧ (∀ l ∈ A i, ∀ t ∈ Set.Icc (0 : ℝ) 1, |y l t - u i - t * v i| ≤ N ^ ε * β ∧ |x l t - MvPolynomial.eval ![t, y l t] (P i)| ≤ N ^ ε * a) ∧ ENNReal.ofReal (c * a ^ d * β / N ^ ε) ≤ μ (A i ×ˢ Set.Icc (0 : ℝ) 1)) ∧ ENNReal.ofReal (N ^ (-ε)) ≤ μ {p | ∃ i, p.1 ∈ A i}) (fun p => ![⌊p.2 / σ⌋, ⌊y p.1 p.2 / σ⌋])) (fun l t => b l 2 + t * b l 3 + t ^ 2 * b l 4)) (fun l t => b l 0 + t * b l 1)) (N ^ (-m))) (N ^ (-s))) → (∀ S a ε : ℝ, 0 < S → 0 < a → 0 < ε → ∃ η : ℝ, 0 < η ∧ ∃ N₀ : ℝ, 2 ≤ N₀ ∧ ∀ N : ℝ, N₀ ≤ N → ∀ (α : Type) [MeasurableSpace α] (ν : MeasureTheory.Measure α) (μ : MeasureTheory.Measure (α × ℝ)) (b v H : α → ℝ) (T : α × ℝ → Fin 2 → ℝ) (π : MeasureTheory.Measure ℝ) (E : ℝ) (F : (Fin 2 → ℤ) → Finset (Fin 2 → ℤ)), (fun ξ : ℝ => (fun z : α × ℝ → Fin 2 → ℝ => (fun q : α × ℝ → Fin 2 → ℤ => Measurable b → Measurable v → Measurable H → Measurable T → MeasureTheory.IsProbabilityMeasure ν → MeasureTheory.IsProbabilityMeasure π → ξ ≤ E → E ≤ 1 → (∀ l, |b l| + |v l| ≤ N ^ η) → μ ≤ ENNReal.ofReal (N ^ η) • (ν.prod MeasureTheory.volume) → μ (Set.univ ×ˢ Set.Icc (0 : ℝ) 1)ᶜ = 0 → ENNReal.ofReal (N ^ (-η)) ≤ μ Set.univ → (∀ x r : ℝ, ξ ≤ r → r ≤ 1 → π (Set.Icc (x - r) (x + r)) ≤ ENNReal.ofReal (N ^ η * r ^ S)) → (∀ (p₀ : Fin 2 → ℤ) (j : ℤ), μ {p | q p = p₀ ∧ ⌊v p.1 / ξ⌋ = j} ≤ ENNReal.ofReal (N ^ η * ξ ^ 2) * π (Set.Ico ((j : ℝ) * ξ) (((j : ℝ) + 1) * ξ))) → (∀ p₀, ((F p₀).card : ℝ) ≤ N ^ η) → (∀ᵐ p ∂μ, (∀ j, |T p j| ≤ N ^ η) ∧ (fun j => ⌊T p j / E⌋) ∈ F (q p) ∧ |T p 0 + v p.1 * T p 1 - H p.1| ≤ N ^ η * E) → ∃ (B : Fin 2 → ℝ) (ℓ : ℝ), |B 0| + |B 1| + |ℓ| ≤ N ^ ε ∧ ENNReal.ofReal (N ^ (-ε)) ≤ μ {p | |T p 0 - B 0 + ℓ * z p 1| ≤ N ^ ε * E ∧ |T p 1 - B 1 - ℓ * z p 0| ≤ N ^ ε * E}) (fun p j => ⌊z p j / ξ⌋)) (fun p => ![p.2, b p.1 + p.2 * v p.1])) (N ^ (-a))) → (∀ N K : ℕ → ℝ, (fun x : (ℕ × (Fin 6 → ℝ)) → ℝ → Fin 4 → ℝ => (fun y : (ℕ × (Fin 6 → ℝ)) → ℝ → EuclideanSpace ℝ (Fin 2) => (fun v : (ℕ × (Fin 6 → ℝ)) → EuclideanSpace ℝ (Fin 2) => (fun δ : ℝ → ℝ → ℝ => (fun obs : ℝ → ℝ → ((ℕ × (Fin 6 → ℝ)) × ℝ) → EuclideanSpace ℝ (Fin 3) × ℤ => (fun fmt : (n : ℕ) → ℝ → ℕ → Set (Fin n → ℝ) → Prop => (∀ k, 2 ≤ N k) → Filter.Tendsto N Filter.atTop Filter.atTop → ((∀ k, 1 ≤ K k) ∧ ∀ ε : ℝ, 0 < ε → ∀ᶠ k in Filter.atTop, K k ≤ N k ^ ε) → ∀ L d S η : ℝ, 0 < L → 0 < d → d < 1 → 0 < S → 0 < η → ∀ (W : ℕ → ℕ) (ω : (k : ℕ) → Fin (W k) → ℝ) (ν : (k : ℕ) → Fin (W k) → MeasureTheory.Measure ((ℕ × (Fin 6 → ℝ)))) (E : (k : ℕ) → Fin (W k) → Set (((ℕ × (Fin 6 → ℝ)) × ℝ))) (P : (k : ℕ) → Fin (W k) → MvPolynomial (Fin 4) ℝ) (B : (k : ℕ) → Fin (W k) → ℝ) (f : ℝ → ℝ), ∀ (g : (k : ℕ) → Fin (W k) → ℝ → (EuclideanSpace ℝ (Fin 3) × ℤ) → ENNReal) (G : (k : ℕ) → Fin (W k) → ℝ → ((EuclideanSpace ℝ (Fin 3) × ℤ) × (Fin 2 → ℤ)) → ENNReal), (fun μ : (k : ℕ) → Fin (W k) → MeasureTheory.Measure ((ℕ × (Fin 6 → ℝ)) × ℝ) => (∃ M D : ℕ, ∀ k, (W k : ℝ) ≤ N k ^ M ∧ (∀ γ, 0 ≤ ω k γ) ∧ (∑ γ, ω k γ) = 1 ∧ (∀ γ, MeasureTheory.IsProbabilityMeasure (ν k γ) ∧ 0 < B k γ ∧ B k γ ≤ N k ^ M ∧ (B k γ)⁻¹ ≤ N k ^ M ∧ (P k γ).totalDegree ≤ 2 ∧ (∀ b, |(P k γ).coeff b| ≤ N k ^ M) ∧ (∃ m : ℕ, (m : ℝ) ≤ N k ^ M ∧ ∃ (c : Fin m → ℝ) (i : Fin m → ℕ) (A : Fin m → Set (Fin 6 → ℝ)), (∀ j, 0 ≤ c j ∧ c j ≤ N k ^ M ∧ (i j : ℝ) ≤ N k ^ M ∧ (fmt 6 (N k ^ M) D ((A j))) ∧ (∀ x ∈ A j, ∀ b, |x b| ≤ N k ^ M)) ∧ ν k γ = ∑ j, (ENNReal.ofReal (c j)) • MeasureTheory.Measure.map (fun x => (i j, x)) (MeasureTheory.volume.restrict (A j))) ∧ MeasurableSet (E k γ) ∧ E k γ ⊆ Set.univ ×ˢ Set.Icc (0 : ℝ) 1 ∧ (∀ p ∈ E k γ, (p.1.1 : ℝ) ≤ N k ^ M ∧ ∀ e, |p.1.2 e| ≤ N k ^ M) ∧ (∀ i, (fmt 7 (N k ^ M) D (({x₁ : Fin 7 → ℝ | ((i, fun j₁ : Fin 6 => x₁ j₁.castSucc), x₁ 6) ∈ (E k γ)})))) ∧ (∀ᵐ l ∂ν k γ, ∀ t ∈ Set.Icc (0 : ℝ) 1, ‖(y l t)‖ + ‖(v l)‖ ≤ K k ∧ |MvPolynomial.eval ((x l t)) (P k γ)| ≤ K k ∧ |MvPolynomial.eval ((x l t)) (MvPolynomial.pderiv (3 : Fin 4) (P k γ))| ≤ K k * B k γ ∧ |MvPolynomial.eval ((x l t)) (MvPolynomial.pderiv (3 : Fin 4) (MvPolynomial.pderiv (3 : Fin 4) (P k γ)))| ≤ K k * (B k γ) ^ 2) ∧ (∀ᵐ p ∂(μ k γ), B k γ / K k ≤ |MvPolynomial.eval ((x p.1 p.2)) (MvPolynomial.pderiv (3 : Fin 4) (P k γ))|)) ∧ ENNReal.ofReal ((K k)⁻¹) ≤ ∑ γ, ENNReal.ofReal (ω k γ) * (μ k γ) Set.univ) → (∀ k γ r, 0 ≤ r → r ≤ L → Measurable (g k γ r) ∧ MeasureTheory.Measure.map ((obs (B k γ) (δ (N k) r))) ((μ k γ)) = (MeasureTheory.volume.prod MeasureTheory.Measure.count).withDensity (g k γ r)) → (∀ k γ u, 0 < u → u ≤ η * L → Measurable (G k γ u) ∧ MeasureTheory.Measure.map ((fun p : ((ℕ × (Fin 6 → ℝ)) × ℝ) => ((obs (B k γ) (δ (N k) L)) p, fun j : Fin 2 => ⌊(v p.1) j / (δ (N k) u)⌋))) ((μ k γ)) = ((MeasureTheory.volume.prod MeasureTheory.Measure.count).prod MeasureTheory.Measure.count).withDensity (G k γ u)) → (∀ r s : ℝ, 0 ≤ r → r ≤ s → s ≤ L → 0 ≤ f s - f r ∧ f s - f r ≤ s - r) → (∀ r τ : ℝ, 0 ≤ r → r ≤ L → 0 < τ → ∃ c : ℝ, 0 < c ∧ ∀ᶠ k in Filter.atTop, (∑ γ, ENNReal.ofReal (ω k γ) * (μ k γ) {p | g k γ r ((obs (B k γ) (δ (N k) r)) p) < ENNReal.ofReal (N k ^ (-f r - τ)) ∨ ENNReal.ofReal (N k ^ (-f r + τ)) < g k γ r ((obs (B k γ) (δ (N k) r)) p)}) ≤ ENNReal.ofReal (N k ^ (-c))) → (∀ r : ℝ, 0 ≤ r → r ≤ L → f L - f r ≤ d * (L - r)) → (∀ u τ : ℝ, 0 < u → u ≤ η * L → 0 < τ → ∃ c : ℝ, 0 < c ∧ ∀ᶠ k in Filter.atTop, (∑ γ, ENNReal.ofReal (ω k γ) * (μ k γ) {p | ENNReal.ofReal (N k ^ (-f L - S * u + τ)) < G k γ u ((fun p : ((ℕ × (Fin 6 → ℝ)) × ℝ) => ((obs (B k γ) (δ (N k) L)) p, fun j : Fin 2 => ⌊(v p.1) j / (δ (N k) u)⌋)) p)}) ≤ ENNReal.ofReal (N k ^ (-c))) → ∀ h : ℝ, 0 < h → ∃ M D : ℕ, ∀ ε : ℝ, 0 < ε → ∃ᶠ k in Filter.atTop, ∃ κ : ℝ, 1 ≤ κ ∧ K k ≤ κ ∧ κ ≤ N k ^ ε ∧ ∃ T C' : ℕ, ∃ (γ : Fin (C') → Fin (W k)) (j : Fin (C') → Fin (2 ^ T)) (c u : Fin (C') → EuclideanSpace ℝ (Fin 2)) (Q : Fin (C') → Matrix (Fin 2) (Fin 2) ℝ) (R : Fin (C') → MvPolynomial (Fin 4) ℝ) (A : Fin (C') → Set ((ℕ × (Fin 6 → ℝ)))) (F : Fin (C') → Set (((ℕ × (Fin 6 → ℝ)) × ℝ))), (2 : ℝ) ^ T ≤ N k ^ h ∧ (C' : ℝ) ≤ N k ^ M ∧ (∀ b b', b ≠ b' → γ b = γ b' → j b = j b' → Disjoint (A b) (A b')) ∧ (∀ b, Matrix.det (Q b) ≠ 0 ∧ ‖c b‖ + ‖u b‖ ≤ N k ^ M ∧ (∑ e : Fin 2, ∑ e' : Fin 2, (|Q b e e'| + |(Q b)⁻¹ e e'|)) ≤ N k ^ M ∧ (∑ e : Fin 2, ∑ e' : Fin 2, |Q b e e'|) ≤ κ / (2 : ℝ) ^ T ∧ (R b).totalDegree ≤ 2 ∧ (∀ e, |(R b).coeff e| ≤ N k ^ M) ∧ MeasurableSet (A b) ∧ MeasurableSet (F b) ∧ (∀ i, (fmt 6 (N k ^ M) D ({x | (i, x) ∈ A b})) ∧ (fmt 7 (N k ^ M) D (({x₁ : Fin 7 → ℝ | ((i, fun j₁ : Fin 6 => x₁ j₁.castSucc), x₁ 6) ∈ (F b)})))) ∧ (∀ l ∈ A b, (l.1 : ℝ) ≤ N k ^ M ∧ (∀ e, |l.2 e| ≤ N k ^ M) ∧ ∀ t ∈ (Set.Icc (((j b : ℕ) : ℝ) / (2 : ℝ) ^ T) ((((j b : ℕ) : ℝ) + 1) / (2 : ℝ) ^ T)), ‖Matrix.toEuclideanLin ((Q b)⁻¹) ((y l t) - c b - t • u b)‖ ≤ κ ∧ |MvPolynomial.eval ((x l t)) (R b)| ≤ κ * (δ (N k) L) ∧ |MvPolynomial.eval ((x l t)) (MvPolynomial.pderiv (3 : Fin 4) (R b))| ≤ κ * B k (γ b) ∧ |MvPolynomial.eval ((x l t)) (MvPolynomial.pderiv (3 : Fin 4) (MvPolynomial.pderiv (3 : Fin 4) (R b)))| ≤ κ * (B k (γ b)) ^ 2 / (δ (N k) L)) ∧ (∀ p ∈ F b, p ∈ E k (γ b) ∧ p.1 ∈ A b ∧ p.2 ∈ (Set.Icc (((j b : ℕ) : ℝ) / (2 : ℝ) ^ T) ((((j b : ℕ) : ℝ) + 1) / (2 : ℝ) ^ T)) ∧ B k (γ b) / κ ≤ |MvPolynomial.eval ((x p.1 p.2)) (MvPolynomial.pderiv (3 : Fin 4) (R b))|) ∧ ENNReal.ofReal (N k ^ (-f L) * |Matrix.det (Q b)| / ((2 : ℝ) ^ T * κ)) ≤ (((ν k (γ b)).prod MeasureTheory.volume) (F b))) ∧ ENNReal.ofReal ((κ)⁻¹) ≤ ∑ b, ENNReal.ofReal (ω k (γ b)) * (((ν k (γ b)).prod MeasureTheory.volume) (F b))) (fun k γ => ((ν k γ).prod MeasureTheory.volume).restrict (E k γ))) (fun n H D A => ∃ m₀ : ℕ, (m₀ : ℝ) ≤ H ∧ ∃ p₀ : Fin m₀ → MvPolynomial (Fin n) ℝ, (∀ i₀, (p₀ i₀).totalDegree ≤ D) ∧ ∃ b₀ : (Fin m₀ → Bool) → Bool, ∀ x₀, x₀ ∈ A ↔ b₀ (fun i₀ => decide (0 ≤ MvPolynomial.eval x₀ (p₀ i₀))) = true)) (fun B a p => (WithLp.toLp 2 ![p.2, (x p.1 p.2) 1, (x p.1 p.2) 2], ⌊B * (x p.1 p.2) 3 / a⌋))) (fun N r => (2 : ℝ) ^ (-(⌊r * Real.log N / Real.log 2⌋ : ℤ)))) (fun l => WithLp.toLp 2 ![l.2 3, l.2 4])) (fun l t => WithLp.toLp 2 ![(x l t) 1, (x l t) 2])) (fun l t => ![t, l.2 0 + t * l.2 3, l.2 1 + t * l.2 4, l.2 2 + t * l.2 5]))k4_cap_class_terminal_chartsSections 3--10, the exclusion of bad problems: the eight non-slope-volume inputs of o018 imply actual true terminal charts for every explicitly specified tempered homogeneous version-2 cap-class problem and every positive upper time exponent. Coefficient priors, independent time, selected events, polynomial format, native tests, pure/angular density laws, typical exceptions, both caps, further selections and subsequences, whole-block fits, disjoint assignments, unnormalized true floors and total mass are all expanded in the statement.
(∀ ε : ℝ, 0 < ε → ∃ η : ℝ, 0 < η ∧ ∃ C : ℝ, 0 < C ∧ ∀ (D : ℕ), 1 ≤ D → ∀ (n : ℕ) (b u : Fin n → EuclideanSpace ℝ (Fin 2)) (ω : Fin n → ℝ) (A : ℝ) (J : Fin n → Finset (Fin D)), (∀ i : Fin n, ‖b i‖ ≤ 1 ∧ ‖u i‖ ≤ 1) → (∀ i : Fin n, 0 < ω i) → 0 < A → (∀ (c w e₁ e₂ : EuclideanSpace ℝ (Fin 2)) (a β : ℝ), ‖e₁‖ = 1 → ‖e₂‖ = 1 → inner ℝ e₁ e₂ = 0 → 1 ≤ a → a ≤ β → β ≤ (D : ℝ) → ∀ S : Finset (Fin n), (∀ i ∈ S, ∀ t ∈ Set.Icc (0 : ℝ) 1, |inner ℝ (b i + t • u i - c - t • w) e₁| ≤ a / (D : ℝ) ∧ |inner ℝ (b i + t • u i - c - t • w) e₂| ≤ β / (D : ℝ)) → ∑ i ∈ S, ω i ≤ A * a * β) → (∀ i : Fin n, (D : ℝ) ^ (1 - η) ≤ ((J i).card : ℝ)) → ∑ i : Fin n, ω i * ((J i).card : ℝ) ≤ C * A * (D : ℝ) ^ ε * ((((Finset.univ : Finset (Fin n)).sigma J).image (fun p => ((p.2 : ℕ), fun k : Fin 2 => ⌊(D : ℝ) * (b p.1 + (((((p.2 : ℕ) : ℝ) + 1 / 2) / (D : ℝ)) • u p.1)) k⌋))).card : ℝ)) → (∀ n : ℕ, 2 ≤ n → n ≤ 4 → ∃ C : ℝ, 0 < C ∧ ∀ r : ℝ, 0 < r → ∀ (N : Fin n → ℕ) (a e : (i : Fin n) → Fin (N i) → EuclideanSpace ℝ (Fin n)) (w : (i : Fin n) → Fin (N i) → ℝ), (∀ (i : Fin n) (k : Fin (N i)), ‖e i k‖ = 1) → (∀ (i : Fin n) (k : Fin (N i)), 0 ≤ w i k) → MeasureTheory.lintegral MeasureTheory.volume (fun x : EuclideanSpace ℝ (Fin n) => ENNReal.ofReal ((∑ T : ((i : Fin n) → Fin (N i)), |Matrix.det (Matrix.of fun i j : Fin n => e i (T i) j)| * ∏ i : Fin n, (w i (T i) * (Metric.thickening r (Set.range fun t : ℝ => a i (T i) + t • e i (T i))).indicator (fun _ => (1 : ℝ)) x)) ^ ((1 : ℝ) / ((n : ℝ) - 1)))) ≤ ENNReal.ofReal (C * r ^ n * ∏ i : Fin n, (∑ k : Fin (N i), w i k) ^ ((1 : ℝ) / ((n : ℝ) - 1)))) → (∀ s : ℝ, 0 < s → s ≤ 1 → ∃ n : ℕ, 2 ≤ n ∧ ∃ r₀ ε₀ τ : ℝ, 0 < r₀ ∧ 0 < ε₀ ∧ 0 < τ ∧ ∀ r : ℝ, 0 < r → r < r₀ → ∀ μ : MeasureTheory.Measure ℝ, MeasureTheory.IsProbabilityMeasure μ → μ (Set.Icc (-1 : ℝ) 1)ᶜ = 0 → (∀ x u : ℝ, r ≤ u → u ≤ 1 → μ (Set.Icc (x - u) (x + u)) ≤ ENNReal.ofReal (r ^ (-ε₀) * u ^ s)) → ∀ ξ : ℝ, r⁻¹ ≤ |ξ| → |ξ| ≤ 2 * r⁻¹ → ‖MeasureTheory.integral (MeasureTheory.Measure.pi (fun _ : Fin n => μ)) (fun x : Fin n → ℝ => Complex.exp (((-2 * Real.pi * ξ * (∏ j : Fin n, x j) : ℝ) : ℂ) * Complex.I))‖ ≤ |ξ| ^ (-τ)) → (∃ c C₀ : ℝ, 0 < c ∧ 0 < C₀ ∧ ∀ (G : Type) [AddCommGroup G] [DecidableEq G] (A B : Finset G) (E : Finset (G × G)) (θ : ℝ), A.Nonempty → B.Nonempty → E ⊆ A ×ˢ B → 0 < θ → θ ≤ 1 → θ * (A.card : ℝ) * (B.card : ℝ) ≤ (E.card : ℝ) → ∃ A' : Finset G, ∃ B' : Finset G, A' ⊆ A ∧ B' ⊆ B ∧ c * θ * (A.card : ℝ) ≤ (A'.card : ℝ) ∧ c * θ * (B.card : ℝ) ≤ (B'.card : ℝ) ∧ c * θ ^ 2 * (A.card : ℝ) * (B.card : ℝ) ≤ ((E ∩ A' ×ˢ B').card : ℝ) ∧ (((A' ×ˢ B').image (fun p : G × G => p.1 + p.2)).card : ℝ) ≤ C₀ * (θ ^ 5)⁻¹ * ((E.image (fun p : G × G => p.1 + p.2)).card : ℝ) ^ 3 / ((A.card : ℝ) * (B.card : ℝ))) → (∀ n D : ℕ, ∃ C : ℝ, 0 < C ∧ ∀ (P : MvPolynomial (Fin (n + 1)) ℂ) (f : EuclideanSpace ℂ (Fin n) → ℂ), P ≠ 0 → P.totalDegree ≤ D → DifferentiableOn ℂ f (Metric.ball 0 4) → (∀ z ∈ Metric.ball (0 : EuclideanSpace ℂ (Fin n)) 4, MvPolynomial.eval (Fin.snoc (fun i : Fin n => z i) (f z)) P = 0) → (∀ x : EuclideanSpace ℝ (Fin n), ‖x‖ ≤ (1 : ℝ) / 2 → ‖f (WithLp.toLp 2 (fun i : Fin n => (x i : ℂ)))‖ ≤ 1) → ∀ z : EuclideanSpace ℂ (Fin n), ‖z‖ ≤ 1 → ‖f z‖ ≤ C) → (∀ (D J : ℕ), 1 ≤ D → D < J → ∀ d : ℝ, 0 ≤ d → d < 1 → ∃ η : ℝ, 0 < η ∧ ∃ N₀ : ℝ, 2 ≤ N₀ ∧ ∀ N : ℝ, N₀ ≤ N → ∀ (n₁ n₂ : ℕ) (f₁ : Fin n₁ → ℝ → ℝ) (f₂ : Fin n₂ → ℝ → ℝ) (π₁ : Fin n₁ → ℝ) (π₂ : Fin n₂ → ℝ) (μ : MeasureTheory.Measure ((Fin n₁ × Fin n₂) × ℝ)), (n₁ : ℝ) ≤ N ^ (d + η) → (n₂ : ℝ) ≤ N ^ (d + η) → (∀ i : Fin n₁, ContDiffOn ℝ (J + 1) (f₁ i) (Set.Ioo (-1 : ℝ) 2)) → (∀ i : Fin n₂, ContDiffOn ℝ (J + 1) (f₂ i) (Set.Ioo (-1 : ℝ) 2)) → (∀ (i : Fin n₁) (j : ℕ), j ≤ J + 1 → ∀ t ∈ Set.Icc (0 : ℝ) 1, |iteratedDeriv j (f₁ i) t| ≤ N ^ η) → (∀ (i : Fin n₂) (j : ℕ), j ≤ J + 1 → ∀ t ∈ Set.Icc (0 : ℝ) 1, |iteratedDeriv j (f₂ i) t| ≤ N ^ η) → (∀ i : Fin n₁, 0 ≤ π₁ i) → (∀ i : Fin n₂, 0 ≤ π₂ i) → (∑ i : Fin n₁, π₁ i) = 1 → (∑ i : Fin n₂, π₂ i) = 1 → MeasureTheory.IsProbabilityMeasure μ → (∀ (i : Fin n₁) (E : Set ℝ), MeasurableSet E → μ {p | p.1.1 = i ∧ p.2 ∈ E} ≤ ENNReal.ofReal (N ^ η * π₁ i) * MeasureTheory.volume E) → (∀ (i : Fin n₂) (E : Set ℝ), MeasurableSet E → μ {p | p.1.2 = i ∧ p.2 ∈ E} ≤ ENNReal.ofReal (N ^ η * π₂ i) * MeasureTheory.volume E) → ¬ μ {p | p.2 ∈ Set.Icc (0 : ℝ) 1 ∧ |f₁ p.1.1 p.2 - f₂ p.1.2 p.2| ≤ N ^ (-1 + η) ∧ ∃ j : ℕ, 1 ≤ j ∧ j ≤ D ∧ N ^ (-η) ≤ |iteratedDeriv j (f₁ p.1.1) p.2 - iteratedDeriv j (f₂ p.1.2) p.2|}ᶜ = 0) → (∀ d c ε : ℝ, 0 ≤ d → d < 1 → 0 < c → 0 < ε → ∃ η : ℝ, 0 < η ∧ ∃ N₀ : ℝ, 2 ≤ N₀ ∧ ∀ N : ℝ, N₀ ≤ N → ∀ (α : Type) [MeasurableSpace α] (ν : MeasureTheory.Measure α) (a : α → EuclideanSpace ℝ (Fin 3)) (E : Set (α × ℝ)) (F : Finset (ℤ × ℤ)), Measurable a → MeasurableSet E → E ⊆ Set.univ ×ˢ Set.Icc (0 : ℝ) 1 → (∀ l : α, ‖a l‖ ≤ N ^ η) → ν Set.univ ≤ ENNReal.ofReal (N ^ η) → ENNReal.ofReal (N ^ (-η)) ≤ (ν.prod MeasureTheory.volume) E → (F.card : ℝ) ≤ N ^ η * (N ^ (-c)) ^ (-1 - d) → (∀ l : α, ∀ t : ℝ, (l, t) ∈ E → (⌊t / (N ^ (-c))⌋, ⌊(a l 0 + t * a l 1 + t ^ 2 * a l 2) / (N ^ (-c))⌋) ∈ F) → (∀ (b : EuclideanSpace ℝ (Fin 3)) (r : ℝ), N ^ (-c) ≤ r → ν {l | a l ∈ Metric.ball b r} ≤ ENNReal.ofReal (N ^ η * r ^ d)) → ∃ q : Fin 3 → ℤ, ENNReal.ofReal (N ^ (-c * d - ε)) ≤ ν {l | (∀ j : Fin 3, ⌊a l j / (N ^ (-c))⌋ = q j) ∧ ENNReal.ofReal (N ^ (-ε)) ≤ MeasureTheory.volume {t : ℝ | (l, t) ∈ E}}) → (∃ C : ℝ, 1 ≤ C ∧ ∀ A : ℝ, 2 ≤ A → ∀ (p : Fin 7 → EuclideanSpace ℝ (Fin 3)) (Q : Matrix (Fin 3) (Fin 3) ℝ) (ε : ℝ), (∀ i : Fin 7, p i 0 = 1 ∧ ‖p i‖ ≤ A) → (∀ i j k : Fin 7, i ≠ j → i ≠ k → j ≠ k → A⁻¹ ≤ |Matrix.det (Matrix.of fun a b : Fin 3 => (![p i, p j, p k] a) b)|) → Q.IsSymm → A⁻¹ ≤ (∑ a : Fin 3, ∑ b : Fin 3, |Q a b|) → (∑ a : Fin 3, ∑ b : Fin 3, |Q a b|) ≤ A → 0 ≤ ε → ε ≤ A ^ (-C) → (∀ i : Fin 7, |∑ a : Fin 3, ∑ b : Fin 3, p i a * Q a b * p i b| ≤ ε) → A ^ (-C) ≤ |Matrix.det Q| ∧ ∃ p' : Fin 7 → EuclideanSpace ℝ (Fin 3), (∀ i : Fin 7, p' i 0 = 1 ∧ (∑ a : Fin 3, ∑ b : Fin 3, p' i a * Q a b * p' i b) = 0 ∧ ‖p' i - p i‖ ≤ A ^ C * ε) ∧ (∀ i j k : Fin 7, i ≠ j → i ≠ k → j ≠ k → (2 * A)⁻¹ ≤ |Matrix.det (Matrix.of fun a b : Fin 3 => (![p' i, p' j, p' k] a) b)|)) → (∀ N K : ℕ → ℝ, (∀ k, 2 ≤ N k) → Filter.Tendsto N Filter.atTop Filter.atTop → ((∀ k, 1 ≤ K k) ∧ ∀ ε : ℝ, 0 < ε → ∀ᶠ k in Filter.atTop, K k ≤ N k ^ ε) → ∀ L d S η : ℝ, 0 < L → 0 < d → d < 1 → 0 < S → 0 < η → ∀ (W : ℕ → ℕ) (ω : (k : ℕ) → Fin (W k) → ℝ) (ν : (k : ℕ) → Fin (W k) → MeasureTheory.Measure (ℕ × (Fin 6 → ℝ))) (E : (k : ℕ) → Fin (W k) → Set ((ℕ × (Fin 6 → ℝ)) × ℝ)) (P : (k : ℕ) → Fin (W k) → MvPolynomial (Fin 4) ℝ) (B : (k : ℕ) → Fin (W k) → ℝ) (f : ℝ → ℝ), ∀ (g : (k : ℕ) → Fin (W k) → ℝ → (EuclideanSpace ℝ (Fin 3) × ℤ) → ENNReal) (G : (k : ℕ) → Fin (W k) → ℝ → ((EuclideanSpace ℝ (Fin 3) × ℤ) × (Fin 2 → ℤ)) → ENNReal), (∃ M D : ℕ, ∀ k, (W k : ℝ) ≤ N k ^ M ∧ (∀ γ, 0 ≤ ω k γ) ∧ (∑ γ, ω k γ) = 1 ∧ (∀ γ, MeasureTheory.IsProbabilityMeasure (ν k γ) ∧ 0 < B k γ ∧ B k γ ≤ N k ^ M ∧ (B k γ)⁻¹ ≤ N k ^ M ∧ (P k γ).totalDegree ≤ 2 ∧ (∀ b, |(P k γ).coeff b| ≤ N k ^ M) ∧ (∃ m : ℕ, (m : ℝ) ≤ N k ^ M ∧ ∃ (c : Fin m → ℝ) (i : Fin m → ℕ) (A : Fin m → Set (Fin 6 → ℝ)), (∀ j, 0 ≤ c j ∧ c j ≤ N k ^ M ∧ (i j : ℝ) ≤ N k ^ M ∧ (∃ m₀ : ℕ, (m₀ : ℝ) ≤ (N k ^ M) ∧ ∃ p₀ : Fin m₀ → MvPolynomial (Fin 6) ℝ, (∀ i₀, (p₀ i₀).totalDegree ≤ D) ∧ ∃ b₀ : (Fin m₀ → Bool) → Bool, ∀ x₀, x₀ ∈ (A j) ↔ b₀ (fun i₀ => decide (0 ≤ MvPolynomial.eval x₀ (p₀ i₀))) = true) ∧ (∀ x ∈ A j, ∀ b, |x b| ≤ N k ^ M)) ∧ ν k γ = ∑ j, (ENNReal.ofReal (c j)) • MeasureTheory.Measure.map (fun x => (i j, x)) (MeasureTheory.volume.restrict (A j))) ∧ MeasurableSet (E k γ) ∧ E k γ ⊆ Set.univ ×ˢ Set.Icc (0 : ℝ) 1 ∧ (∀ p ∈ E k γ, (p.1.1 : ℝ) ≤ N k ^ M ∧ ∀ e, |p.1.2 e| ≤ N k ^ M) ∧ (∀ i, (∃ m₀ : ℕ, (m₀ : ℝ) ≤ (N k ^ M) ∧ ∃ p₀ : Fin m₀ → MvPolynomial (Fin 7) ℝ, (∀ i₀, (p₀ i₀).totalDegree ≤ D) ∧ ∃ b₀ : (Fin m₀ → Bool) → Bool, ∀ x₀, x₀ ∈ ({x₁ : Fin 7 → ℝ | ((i, fun j₁ : Fin 6 => x₁ j₁.castSucc), x₁ 6) ∈ (E k γ)}) ↔ b₀ (fun i₀ => decide (0 ≤ MvPolynomial.eval x₀ (p₀ i₀))) = true)) ∧ (∀ᵐ l ∂ν k γ, ∀ t ∈ Set.Icc (0 : ℝ) 1, ‖(WithLp.toLp 2 ![![t, l.2 0 + t * l.2 3, l.2 1 + t * l.2 4, l.2 2 + t * l.2 5] 1, ![t, l.2 0 + t * l.2 3, l.2 1 + t * l.2 4, l.2 2 + t * l.2 5] 2])‖ + ‖(WithLp.toLp 2 ![l.2 3, l.2 4])‖ ≤ K k ∧ |MvPolynomial.eval (![t, l.2 0 + t * l.2 3, l.2 1 + t * l.2 4, l.2 2 + t * l.2 5]) (P k γ)| ≤ K k ∧ |MvPolynomial.eval (![t, l.2 0 + t * l.2 3, l.2 1 + t * l.2 4, l.2 2 + t * l.2 5]) (MvPolynomial.pderiv (3 : Fin 4) (P k γ))| ≤ K k * B k γ ∧ |MvPolynomial.eval (![t, l.2 0 + t * l.2 3, l.2 1 + t * l.2 4, l.2 2 + t * l.2 5]) (MvPolynomial.pderiv (3 : Fin 4) (MvPolynomial.pderiv (3 : Fin 4) (P k γ)))| ≤ K k * (B k γ) ^ 2) ∧ (∀ᵐ p ∂(((ν k γ).prod MeasureTheory.volume).restrict (E k γ)), B k γ / K k ≤ |MvPolynomial.eval (![p.2, p.1.2 0 + p.2 * p.1.2 3, p.1.2 1 + p.2 * p.1.2 4, p.1.2 2 + p.2 * p.1.2 5]) (MvPolynomial.pderiv (3 : Fin 4) (P k γ))|)) ∧ ENNReal.ofReal ((K k)⁻¹) ≤ ∑ γ, ENNReal.ofReal (ω k γ) * (((ν k γ).prod MeasureTheory.volume).restrict (E k γ)) Set.univ) → (∀ k γ r, 0 ≤ r → r ≤ L → Measurable (g k γ r) ∧ MeasureTheory.Measure.map ((fun p : (ℕ × (Fin 6 → ℝ)) × ℝ => ((WithLp.toLp 2 ![p.2, ![p.2, p.1.2 0 + p.2 * p.1.2 3, p.1.2 1 + p.2 * p.1.2 4, p.1.2 2 + p.2 * p.1.2 5] 1, ![p.2, p.1.2 0 + p.2 * p.1.2 3, p.1.2 1 + p.2 * p.1.2 4, p.1.2 2 + p.2 * p.1.2 5] 2] : EuclideanSpace ℝ (Fin 3)), ⌊B k γ * ![p.2, p.1.2 0 + p.2 * p.1.2 3, p.1.2 1 + p.2 * p.1.2 4, p.1.2 2 + p.2 * p.1.2 5] 3 / ((2 : ℝ) ^ (-(⌊r * Real.log (N k) / Real.log 2⌋ : ℤ)))⌋))) ((((ν k γ).prod MeasureTheory.volume).restrict (E k γ))) = (MeasureTheory.volume.prod MeasureTheory.Measure.count).withDensity (g k γ r)) → (∀ k γ u, 0 < u → u ≤ η * L → Measurable (G k γ u) ∧ MeasureTheory.Measure.map ((fun p : (ℕ × (Fin 6 → ℝ)) × ℝ => ((fun p : (ℕ × (Fin 6 → ℝ)) × ℝ => ((WithLp.toLp 2 ![p.2, ![p.2, p.1.2 0 + p.2 * p.1.2 3, p.1.2 1 + p.2 * p.1.2 4, p.1.2 2 + p.2 * p.1.2 5] 1, ![p.2, p.1.2 0 + p.2 * p.1.2 3, p.1.2 1 + p.2 * p.1.2 4, p.1.2 2 + p.2 * p.1.2 5] 2] : EuclideanSpace ℝ (Fin 3)), ⌊B k γ * ![p.2, p.1.2 0 + p.2 * p.1.2 3, p.1.2 1 + p.2 * p.1.2 4, p.1.2 2 + p.2 * p.1.2 5] 3 / ((2 : ℝ) ^ (-(⌊L * Real.log (N k) / Real.log 2⌋ : ℤ)))⌋)) p, fun j : Fin 2 => ⌊(WithLp.toLp 2 ![p.1.2 3, p.1.2 4]) j / ((2 : ℝ) ^ (-(⌊u * Real.log (N k) / Real.log 2⌋ : ℤ)))⌋))) ((((ν k γ).prod MeasureTheory.volume).restrict (E k γ))) = ((MeasureTheory.volume.prod MeasureTheory.Measure.count).prod MeasureTheory.Measure.count).withDensity (G k γ u)) → (∀ r s : ℝ, 0 ≤ r → r ≤ s → s ≤ L → 0 ≤ f s - f r ∧ f s - f r ≤ s - r) → (∀ r τ : ℝ, 0 ≤ r → r ≤ L → 0 < τ → ∃ c : ℝ, 0 < c ∧ ∀ᶠ k in Filter.atTop, (∑ γ, ENNReal.ofReal (ω k γ) * (((ν k γ).prod MeasureTheory.volume).restrict (E k γ)) {p | g k γ r ((fun p : (ℕ × (Fin 6 → ℝ)) × ℝ => ((WithLp.toLp 2 ![p.2, ![p.2, p.1.2 0 + p.2 * p.1.2 3, p.1.2 1 + p.2 * p.1.2 4, p.1.2 2 + p.2 * p.1.2 5] 1, ![p.2, p.1.2 0 + p.2 * p.1.2 3, p.1.2 1 + p.2 * p.1.2 4, p.1.2 2 + p.2 * p.1.2 5] 2] : EuclideanSpace ℝ (Fin 3)), ⌊B k γ * ![p.2, p.1.2 0 + p.2 * p.1.2 3, p.1.2 1 + p.2 * p.1.2 4, p.1.2 2 + p.2 * p.1.2 5] 3 / ((2 : ℝ) ^ (-(⌊r * Real.log (N k) / Real.log 2⌋ : ℤ)))⌋)) p) < ENNReal.ofReal (N k ^ (-f r - τ)) ∨ ENNReal.ofReal (N k ^ (-f r + τ)) < g k γ r ((fun p : (ℕ × (Fin 6 → ℝ)) × ℝ => ((WithLp.toLp 2 ![p.2, ![p.2, p.1.2 0 + p.2 * p.1.2 3, p.1.2 1 + p.2 * p.1.2 4, p.1.2 2 + p.2 * p.1.2 5] 1, ![p.2, p.1.2 0 + p.2 * p.1.2 3, p.1.2 1 + p.2 * p.1.2 4, p.1.2 2 + p.2 * p.1.2 5] 2] : EuclideanSpace ℝ (Fin 3)), ⌊B k γ * ![p.2, p.1.2 0 + p.2 * p.1.2 3, p.1.2 1 + p.2 * p.1.2 4, p.1.2 2 + p.2 * p.1.2 5] 3 / ((2 : ℝ) ^ (-(⌊r * Real.log (N k) / Real.log 2⌋ : ℤ)))⌋)) p)}) ≤ ENNReal.ofReal (N k ^ (-c))) → (∀ r : ℝ, 0 ≤ r → r ≤ L → f L - f r ≤ d * (L - r)) → (∀ u τ : ℝ, 0 < u → u ≤ η * L → 0 < τ → ∃ c : ℝ, 0 < c ∧ ∀ᶠ k in Filter.atTop, (∑ γ, ENNReal.ofReal (ω k γ) * (((ν k γ).prod MeasureTheory.volume).restrict (E k γ)) {p | ENNReal.ofReal (N k ^ (-f L - S * u + τ)) < G k γ u ((fun p : (ℕ × (Fin 6 → ℝ)) × ℝ => ((fun p : (ℕ × (Fin 6 → ℝ)) × ℝ => ((WithLp.toLp 2 ![p.2, ![p.2, p.1.2 0 + p.2 * p.1.2 3, p.1.2 1 + p.2 * p.1.2 4, p.1.2 2 + p.2 * p.1.2 5] 1, ![p.2, p.1.2 0 + p.2 * p.1.2 3, p.1.2 1 + p.2 * p.1.2 4, p.1.2 2 + p.2 * p.1.2 5] 2] : EuclideanSpace ℝ (Fin 3)), ⌊B k γ * ![p.2, p.1.2 0 + p.2 * p.1.2 3, p.1.2 1 + p.2 * p.1.2 4, p.1.2 2 + p.2 * p.1.2 5] 3 / ((2 : ℝ) ^ (-(⌊L * Real.log (N k) / Real.log 2⌋ : ℤ)))⌋)) p, fun j : Fin 2 => ⌊(WithLp.toLp 2 ![p.1.2 3, p.1.2 4]) j / ((2 : ℝ) ^ (-(⌊u * Real.log (N k) / Real.log 2⌋ : ℤ)))⌋)) p)}) ≤ ENNReal.ofReal (N k ^ (-c))) → ∀ h : ℝ, 0 < h → ∃ ψ : ℕ → ℕ, StrictMono ψ ∧ ∃ M D : ℕ, ∃ K' : ℕ → ℝ, ((∀ k, 1 ≤ K' k) ∧ ∀ ε : ℝ, 0 < ε → ∀ᶠ k in Filter.atTop, K' k ≤ N (ψ k) ^ ε) ∧ (∀ k, K (ψ k) ≤ K' k) ∧ ∃ T C' : ℕ → ℕ, ∃ (γ : (k : ℕ) → Fin (C' k) → Fin (W (ψ k))) (j : (k : ℕ) → Fin (C' k) → Fin (2 ^ T k)) (c u : (k : ℕ) → Fin (C' k) → EuclideanSpace ℝ (Fin 2)) (Q : (k : ℕ) → Fin (C' k) → Matrix (Fin 2) (Fin 2) ℝ) (R : (k : ℕ) → Fin (C' k) → MvPolynomial (Fin 4) ℝ) (A : (k : ℕ) → Fin (C' k) → Set (ℕ × (Fin 6 → ℝ))) (F : (k : ℕ) → Fin (C' k) → Set ((ℕ × (Fin 6 → ℝ)) × ℝ)), ∀ k, (2 : ℝ) ^ T k ≤ N (ψ k) ^ h ∧ (C' k : ℝ) ≤ N (ψ k) ^ M ∧ (∀ b b', b ≠ b' → γ k b = γ k b' → j k b = j k b' → Disjoint (A k b) (A k b')) ∧ (∀ b, Matrix.det (Q k b) ≠ 0 ∧ ‖c k b‖ + ‖u k b‖ ≤ N (ψ k) ^ M ∧ (∑ e : Fin 2, ∑ e' : Fin 2, (|Q k b e e'| + |(Q k b)⁻¹ e e'|)) ≤ N (ψ k) ^ M ∧ (∑ e : Fin 2, ∑ e' : Fin 2, |Q k b e e'|) ≤ K' k / (2 : ℝ) ^ T k ∧ (R k b).totalDegree ≤ 2 ∧ (∀ e, |(R k b).coeff e| ≤ N (ψ k) ^ M) ∧ MeasurableSet (A k b) ∧ MeasurableSet (F k b) ∧ (∀ i, (∃ m₀ : ℕ, (m₀ : ℝ) ≤ (N (ψ k) ^ M) ∧ ∃ p₀ : Fin m₀ → MvPolynomial (Fin 6) ℝ, (∀ i₀, (p₀ i₀).totalDegree ≤ D) ∧ ∃ b₀ : (Fin m₀ → Bool) → Bool, ∀ x₀, x₀ ∈ {x | (i, x) ∈ A k b} ↔ b₀ (fun i₀ => decide (0 ≤ MvPolynomial.eval x₀ (p₀ i₀))) = true) ∧ (∃ m₀ : ℕ, (m₀ : ℝ) ≤ (N (ψ k) ^ M) ∧ ∃ p₀ : Fin m₀ → MvPolynomial (Fin 7) ℝ, (∀ i₀, (p₀ i₀).totalDegree ≤ D) ∧ ∃ b₀ : (Fin m₀ → Bool) → Bool, ∀ x₀, x₀ ∈ ({x₁ : Fin 7 → ℝ | ((i, fun j₁ : Fin 6 => x₁ j₁.castSucc), x₁ 6) ∈ (F k b)}) ↔ b₀ (fun i₀ => decide (0 ≤ MvPolynomial.eval x₀ (p₀ i₀))) = true)) ∧ (∀ l ∈ A k b, (l.1 : ℝ) ≤ N (ψ k) ^ M ∧ (∀ e, |l.2 e| ≤ N (ψ k) ^ M) ∧ ∀ t ∈ (Set.Icc (((j k b : ℕ) : ℝ) / (2 : ℝ) ^ T k) ((((j k b : ℕ) : ℝ) + 1) / (2 : ℝ) ^ T k)), ‖Matrix.toEuclideanLin ((Q k b)⁻¹) ((WithLp.toLp 2 ![![t, l.2 0 + t * l.2 3, l.2 1 + t * l.2 4, l.2 2 + t * l.2 5] 1, ![t, l.2 0 + t * l.2 3, l.2 1 + t * l.2 4, l.2 2 + t * l.2 5] 2]) - c k b - t • u k b)‖ ≤ K' k ∧ |MvPolynomial.eval (![t, l.2 0 + t * l.2 3, l.2 1 + t * l.2 4, l.2 2 + t * l.2 5]) (R k b)| ≤ K' k * ((2 : ℝ) ^ (-(⌊L * Real.log (N (ψ k)) / Real.log 2⌋ : ℤ))) ∧ |MvPolynomial.eval (![t, l.2 0 + t * l.2 3, l.2 1 + t * l.2 4, l.2 2 + t * l.2 5]) (MvPolynomial.pderiv (3 : Fin 4) (R k b))| ≤ K' k * B (ψ k) (γ k b) ∧ |MvPolynomial.eval (![t, l.2 0 + t * l.2 3, l.2 1 + t * l.2 4, l.2 2 + t * l.2 5]) (MvPolynomial.pderiv (3 : Fin 4) (MvPolynomial.pderiv (3 : Fin 4) (R k b)))| ≤ K' k * (B (ψ k) (γ k b)) ^ 2 / ((2 : ℝ) ^ (-(⌊L * Real.log (N (ψ k)) / Real.log 2⌋ : ℤ)))) ∧ (∀ p ∈ F k b, p ∈ E (ψ k) (γ k b) ∧ p.1 ∈ A k b ∧ p.2 ∈ (Set.Icc (((j k b : ℕ) : ℝ) / (2 : ℝ) ^ T k) ((((j k b : ℕ) : ℝ) + 1) / (2 : ℝ) ^ T k)) ∧ B (ψ k) (γ k b) / K' k ≤ |MvPolynomial.eval (![p.2, p.1.2 0 + p.2 * p.1.2 3, p.1.2 1 + p.2 * p.1.2 4, p.1.2 2 + p.2 * p.1.2 5]) (MvPolynomial.pderiv (3 : Fin 4) (R k b))|) ∧ ENNReal.ofReal (N (ψ k) ^ (-f L) * |Matrix.det (Q k b)| / ((2 : ℝ) ^ T k * K' k)) ≤ (((ν (ψ k) (γ k b)).prod MeasureTheory.volume) (F k b))) ∧ ENNReal.ofReal ((K' k)⁻¹) ≤ ∑ b, ENNReal.ofReal (ω (ψ k) (γ k b)) * (((ν (ψ k) (γ k b)).prod MeasureTheory.volume) (F k b)))k4_framework_from_matching_clustering_conicThe remaining Theorem 2.17 and Sections 3--10 framework implication: the six original o009 inputs together with the explicit finite conclusions of Lemmas 3.3, 5.1, and 6.7 imply DK4. The new conclusions are written as antecedents of this closed type. The remainder includes smoothing, density profiles, the full exact-problem/cap-class/horizon construction, algebraic continuation and jet/Remez consequences, critical paths and candidate upgrade, scalar-normal fits, tensor kernels and isotropic improvement, retained-edge rigidity, and the three narrowness exclusions.
(∀ ε : ℝ, 0 < ε → ∃ η : ℝ, 0 < η ∧ ∃ C : ℝ, 0 < C ∧ ∀ (D : ℕ), 1 ≤ D → ∀ (n : ℕ) (b u : Fin n → EuclideanSpace ℝ (Fin 2)) (ω : Fin n → ℝ) (A : ℝ) (J : Fin n → Finset (Fin D)), (∀ i : Fin n, ‖b i‖ ≤ 1 ∧ ‖u i‖ ≤ 1) → (∀ i : Fin n, 0 < ω i) → 0 < A → (∀ (c w e₁ e₂ : EuclideanSpace ℝ (Fin 2)) (a β : ℝ), ‖e₁‖ = 1 → ‖e₂‖ = 1 → inner ℝ e₁ e₂ = 0 → 1 ≤ a → a ≤ β → β ≤ (D : ℝ) → ∀ S : Finset (Fin n), (∀ i ∈ S, ∀ t ∈ Set.Icc (0 : ℝ) 1, |inner ℝ (b i + t • u i - c - t • w) e₁| ≤ a / (D : ℝ) ∧ |inner ℝ (b i + t • u i - c - t • w) e₂| ≤ β / (D : ℝ)) → ∑ i ∈ S, ω i ≤ A * a * β) → (∀ i : Fin n, (D : ℝ) ^ (1 - η) ≤ ((J i).card : ℝ)) → ∑ i : Fin n, ω i * ((J i).card : ℝ) ≤ C * A * (D : ℝ) ^ ε * ((((Finset.univ : Finset (Fin n)).sigma J).image (fun p => ((p.2 : ℕ), fun k : Fin 2 => ⌊(D : ℝ) * (b p.1 + (((((p.2 : ℕ) : ℝ) + 1 / 2) / (D : ℝ)) • u p.1)) k⌋))).card : ℝ)) → (∀ n : ℕ, 2 ≤ n → n ≤ 4 → ∃ C : ℝ, 0 < C ∧ ∀ r : ℝ, 0 < r → ∀ (N : Fin n → ℕ) (a e : (i : Fin n) → Fin (N i) → EuclideanSpace ℝ (Fin n)) (w : (i : Fin n) → Fin (N i) → ℝ), (∀ (i : Fin n) (k : Fin (N i)), ‖e i k‖ = 1) → (∀ (i : Fin n) (k : Fin (N i)), 0 ≤ w i k) → MeasureTheory.lintegral MeasureTheory.volume (fun x : EuclideanSpace ℝ (Fin n) => ENNReal.ofReal ((∑ T : ((i : Fin n) → Fin (N i)), |Matrix.det (Matrix.of fun i j : Fin n => e i (T i) j)| * ∏ i : Fin n, (w i (T i) * (Metric.thickening r (Set.range fun t : ℝ => a i (T i) + t • e i (T i))).indicator (fun _ => (1 : ℝ)) x)) ^ ((1 : ℝ) / ((n : ℝ) - 1)))) ≤ ENNReal.ofReal (C * r ^ n * ∏ i : Fin n, (∑ k : Fin (N i), w i k) ^ ((1 : ℝ) / ((n : ℝ) - 1)))) → (∀ s : ℝ, 0 < s → s ≤ 1 → ∃ n : ℕ, 2 ≤ n ∧ ∃ r₀ ε₀ τ : ℝ, 0 < r₀ ∧ 0 < ε₀ ∧ 0 < τ ∧ ∀ r : ℝ, 0 < r → r < r₀ → ∀ μ : MeasureTheory.Measure ℝ, MeasureTheory.IsProbabilityMeasure μ → μ (Set.Icc (-1 : ℝ) 1)ᶜ = 0 → (∀ x u : ℝ, r ≤ u → u ≤ 1 → μ (Set.Icc (x - u) (x + u)) ≤ ENNReal.ofReal (r ^ (-ε₀) * u ^ s)) → ∀ ξ : ℝ, r⁻¹ ≤ |ξ| → |ξ| ≤ 2 * r⁻¹ → ‖MeasureTheory.integral (MeasureTheory.Measure.pi (fun _ : Fin n => μ)) (fun x : Fin n → ℝ => Complex.exp (((-2 * Real.pi * ξ * (∏ j : Fin n, x j) : ℝ) : ℂ) * Complex.I))‖ ≤ |ξ| ^ (-τ)) → (∃ c C₀ : ℝ, 0 < c ∧ 0 < C₀ ∧ ∀ (G : Type) [AddCommGroup G] [DecidableEq G] (A B : Finset G) (E : Finset (G × G)) (θ : ℝ), A.Nonempty → B.Nonempty → E ⊆ A ×ˢ B → 0 < θ → θ ≤ 1 → θ * (A.card : ℝ) * (B.card : ℝ) ≤ (E.card : ℝ) → ∃ A' : Finset G, ∃ B' : Finset G, A' ⊆ A ∧ B' ⊆ B ∧ c * θ * (A.card : ℝ) ≤ (A'.card : ℝ) ∧ c * θ * (B.card : ℝ) ≤ (B'.card : ℝ) ∧ c * θ ^ 2 * (A.card : ℝ) * (B.card : ℝ) ≤ ((E ∩ A' ×ˢ B').card : ℝ) ∧ (((A' ×ˢ B').image (fun p : G × G => p.1 + p.2)).card : ℝ) ≤ C₀ * (θ ^ 5)⁻¹ * ((E.image (fun p : G × G => p.1 + p.2)).card : ℝ) ^ 3 / ((A.card : ℝ) * (B.card : ℝ))) → (∃ C : ℝ, 0 < C ∧ ∀ (P : MvPolynomial (Fin 4) ℝ) (D : Matrix (Fin 2) (Fin 2) ℝ) (c u : EuclideanSpace ℝ (Fin 2)) (t₀ q a K R : ℝ), P.totalDegree ≤ 2 → Matrix.det D ≠ 0 → 0 < q → 0 < a → 1 ≤ K → 1 ≤ R → MeasureTheory.volume {s : EuclideanSpace ℝ (Fin 3) | ‖s‖ ≤ R ∧ ∃ b : EuclideanSpace ℝ (Fin 3), ‖b‖ ≤ R ∧ (∀ t ∈ Set.Icc t₀ (t₀ + q), ‖Matrix.toEuclideanLin (D⁻¹) (WithLp.toLp 2 (fun i : Fin 2 => (b + t • s) i.castSucc - c i - t * u i))‖ ≤ K ∧ |MvPolynomial.eval ![t, (b + t • s) 0, (b + t • s) 1, (b + t • s) 2] P| ≤ K * a) ∧ ∃ t ∈ Set.Icc t₀ (t₀ + q), K⁻¹ ≤ |MvPolynomial.eval ![t, (b + t • s) 0, (b + t • s) 1, (b + t • s) 2] (MvPolynomial.pderiv (3 : Fin 4) P)|} ≤ ENNReal.ofReal (C * K ^ 4 * a * |Matrix.det D| / q ^ 3)) → (∀ n D : ℕ, ∃ C : ℝ, 0 < C ∧ ∀ (P : MvPolynomial (Fin (n + 1)) ℂ) (f : EuclideanSpace ℂ (Fin n) → ℂ), P ≠ 0 → P.totalDegree ≤ D → DifferentiableOn ℂ f (Metric.ball 0 4) → (∀ z ∈ Metric.ball (0 : EuclideanSpace ℂ (Fin n)) 4, MvPolynomial.eval (Fin.snoc (fun i : Fin n => z i) (f z)) P = 0) → (∀ x : EuclideanSpace ℝ (Fin n), ‖x‖ ≤ (1 : ℝ) / 2 → ‖f (WithLp.toLp 2 (fun i : Fin n => (x i : ℂ)))‖ ≤ 1) → ∀ z : EuclideanSpace ℂ (Fin n), ‖z‖ ≤ 1 → ‖f z‖ ≤ C) → (∀ (D J : ℕ), 1 ≤ D → D < J → ∀ d : ℝ, 0 ≤ d → d < 1 → ∃ η : ℝ, 0 < η ∧ ∃ N₀ : ℝ, 2 ≤ N₀ ∧ ∀ N : ℝ, N₀ ≤ N → ∀ (n₁ n₂ : ℕ) (f₁ : Fin n₁ → ℝ → ℝ) (f₂ : Fin n₂ → ℝ → ℝ) (π₁ : Fin n₁ → ℝ) (π₂ : Fin n₂ → ℝ) (μ : MeasureTheory.Measure ((Fin n₁ × Fin n₂) × ℝ)), (n₁ : ℝ) ≤ N ^ (d + η) → (n₂ : ℝ) ≤ N ^ (d + η) → (∀ i : Fin n₁, ContDiffOn ℝ (J + 1) (f₁ i) (Set.Ioo (-1 : ℝ) 2)) → (∀ i : Fin n₂, ContDiffOn ℝ (J + 1) (f₂ i) (Set.Ioo (-1 : ℝ) 2)) → (∀ (i : Fin n₁) (j : ℕ), j ≤ J + 1 → ∀ t ∈ Set.Icc (0 : ℝ) 1, |iteratedDeriv j (f₁ i) t| ≤ N ^ η) → (∀ (i : Fin n₂) (j : ℕ), j ≤ J + 1 → ∀ t ∈ Set.Icc (0 : ℝ) 1, |iteratedDeriv j (f₂ i) t| ≤ N ^ η) → (∀ i : Fin n₁, 0 ≤ π₁ i) → (∀ i : Fin n₂, 0 ≤ π₂ i) → (∑ i : Fin n₁, π₁ i) = 1 → (∑ i : Fin n₂, π₂ i) = 1 → MeasureTheory.IsProbabilityMeasure μ → (∀ (i : Fin n₁) (E : Set ℝ), MeasurableSet E → μ {p | p.1.1 = i ∧ p.2 ∈ E} ≤ ENNReal.ofReal (N ^ η * π₁ i) * MeasureTheory.volume E) → (∀ (i : Fin n₂) (E : Set ℝ), MeasurableSet E → μ {p | p.1.2 = i ∧ p.2 ∈ E} ≤ ENNReal.ofReal (N ^ η * π₂ i) * MeasureTheory.volume E) → ¬ μ {p | p.2 ∈ Set.Icc (0 : ℝ) 1 ∧ |f₁ p.1.1 p.2 - f₂ p.1.2 p.2| ≤ N ^ (-1 + η) ∧ ∃ j : ℕ, 1 ≤ j ∧ j ≤ D ∧ N ^ (-η) ≤ |iteratedDeriv j (f₁ p.1.1) p.2 - iteratedDeriv j (f₂ p.1.2) p.2|}ᶜ = 0) → (∀ d c ε : ℝ, 0 ≤ d → d < 1 → 0 < c → 0 < ε → ∃ η : ℝ, 0 < η ∧ ∃ N₀ : ℝ, 2 ≤ N₀ ∧ ∀ N : ℝ, N₀ ≤ N → ∀ (α : Type) [MeasurableSpace α] (ν : MeasureTheory.Measure α) (a : α → EuclideanSpace ℝ (Fin 3)) (E : Set (α × ℝ)) (F : Finset (ℤ × ℤ)), Measurable a → MeasurableSet E → E ⊆ Set.univ ×ˢ Set.Icc (0 : ℝ) 1 → (∀ l : α, ‖a l‖ ≤ N ^ η) → ν Set.univ ≤ ENNReal.ofReal (N ^ η) → ENNReal.ofReal (N ^ (-η)) ≤ (ν.prod MeasureTheory.volume) E → (F.card : ℝ) ≤ N ^ η * (N ^ (-c)) ^ (-1 - d) → (∀ l : α, ∀ t : ℝ, (l, t) ∈ E → (⌊t / (N ^ (-c))⌋, ⌊(a l 0 + t * a l 1 + t ^ 2 * a l 2) / (N ^ (-c))⌋) ∈ F) → (∀ (b : EuclideanSpace ℝ (Fin 3)) (r : ℝ), N ^ (-c) ≤ r → ν {l | a l ∈ Metric.ball b r} ≤ ENNReal.ofReal (N ^ η * r ^ d)) → ∃ q : Fin 3 → ℤ, ENNReal.ofReal (N ^ (-c * d - ε)) ≤ ν {l | (∀ j : Fin 3, ⌊a l j / (N ^ (-c))⌋ = q j) ∧ ENNReal.ofReal (N ^ (-ε)) ≤ MeasureTheory.volume {t : ℝ | (l, t) ∈ E}}) → (∃ C : ℝ, 1 ≤ C ∧ ∀ A : ℝ, 2 ≤ A → ∀ (p : Fin 7 → EuclideanSpace ℝ (Fin 3)) (Q : Matrix (Fin 3) (Fin 3) ℝ) (ε : ℝ), (∀ i : Fin 7, p i 0 = 1 ∧ ‖p i‖ ≤ A) → (∀ i j k : Fin 7, i ≠ j → i ≠ k → j ≠ k → A⁻¹ ≤ |Matrix.det (Matrix.of fun a b : Fin 3 => (![p i, p j, p k] a) b)|) → Q.IsSymm → A⁻¹ ≤ (∑ a : Fin 3, ∑ b : Fin 3, |Q a b|) → (∑ a : Fin 3, ∑ b : Fin 3, |Q a b|) ≤ A → 0 ≤ ε → ε ≤ A ^ (-C) → (∀ i : Fin 7, |∑ a : Fin 3, ∑ b : Fin 3, p i a * Q a b * p i b| ≤ ε) → A ^ (-C) ≤ |Matrix.det Q| ∧ ∃ p' : Fin 7 → EuclideanSpace ℝ (Fin 3), (∀ i : Fin 7, p' i 0 = 1 ∧ (∑ a : Fin 3, ∑ b : Fin 3, p' i a * Q a b * p' i b) = 0 ∧ ‖p' i - p i‖ ≤ A ^ C * ε) ∧ (∀ i j k : Fin 7, i ≠ j → i ≠ k → j ≠ k → (2 * A)⁻¹ ≤ |Matrix.det (Matrix.of fun a b : Fin 3 => (![p' i, p' j, p' k] a) b)|)) → ∀ σ : ℝ, 0 < σ → σ ≤ 1 → ∀ c : ℝ, 0 < c → ∀ R : ℝ, 1 ≤ R → ∃ k₀ : ℕ, ∀ k : ℕ, k₀ ≤ k → ∀ (n : ℕ) (x v : Fin n → EuclideanSpace ℝ (Fin 4)), c * (2 : ℝ) ^ (3 * k) / ((k : ℝ) + 1) ^ 2 ≤ (n : ℝ) → (∀ i : Fin n, x i 0 = 0 ∧ v i 0 = 1 ∧ ‖v i‖ ≤ 2) → (∀ i j : Fin n, i ≠ j → (2 : ℝ) ^ (-(k : ℤ)) ≤ ‖v i - v j‖) → (∀ i : Fin n, ‖x i‖ ≤ R) → ∀ (m : ℕ) (z : Fin m → EuclideanSpace ℝ (Fin 4)) (ρ : Fin m → ℝ), (m : ℝ) ≤ (2 : ℝ) ^ (((k : ℝ) + 1) * (4 - σ)) → (∀ j : Fin m, (2 : ℝ) ^ (-((k : ℤ) + 1)) < ρ j ∧ ρ j ≤ (2 : ℝ) ^ (-(k : ℤ))) → ¬ (∀ i : Fin n, ENNReal.ofReal (c / ((k : ℝ) + 1) ^ 2) ≤ MeasureTheory.volume {t : ℝ | t ∈ Set.Icc (0 : ℝ) 1 ∧ x i + t • v i ∈ ⋃ j : Fin m, Metric.ball (z j) (ρ j)})k4_core_from_geometric_boundsThe core framework implication assuming the quadratic slope-volume estimate and the algebraic-sheet bound, as well as the four original tools T1,T3,T4,T5. Prove the rest of Theorem 2.17 and Sections 3--10 using these concrete geometric inputs to obtain DK4.
(∀ ε : ℝ, 0 < ε → ∃ η : ℝ, 0 < η ∧ ∃ C : ℝ, 0 < C ∧ ∀ (D : ℕ), 1 ≤ D → ∀ (n : ℕ) (b u : Fin n → EuclideanSpace ℝ (Fin 2)) (ω : Fin n → ℝ) (A : ℝ) (J : Fin n → Finset (Fin D)), (∀ i : Fin n, ‖b i‖ ≤ 1 ∧ ‖u i‖ ≤ 1) → (∀ i : Fin n, 0 < ω i) → 0 < A → (∀ (c w e₁ e₂ : EuclideanSpace ℝ (Fin 2)) (a β : ℝ), ‖e₁‖ = 1 → ‖e₂‖ = 1 → inner ℝ e₁ e₂ = 0 → 1 ≤ a → a ≤ β → β ≤ (D : ℝ) → ∀ S : Finset (Fin n), (∀ i ∈ S, ∀ t ∈ Set.Icc (0 : ℝ) 1, |inner ℝ (b i + t • u i - c - t • w) e₁| ≤ a / (D : ℝ) ∧ |inner ℝ (b i + t • u i - c - t • w) e₂| ≤ β / (D : ℝ)) → ∑ i ∈ S, ω i ≤ A * a * β) → (∀ i : Fin n, (D : ℝ) ^ (1 - η) ≤ ((J i).card : ℝ)) → ∑ i : Fin n, ω i * ((J i).card : ℝ) ≤ C * A * (D : ℝ) ^ ε * ((((Finset.univ : Finset (Fin n)).sigma J).image (fun p => ((p.2 : ℕ), fun k : Fin 2 => ⌊(D : ℝ) * (b p.1 + (((((p.2 : ℕ) : ℝ) + 1 / 2) / (D : ℝ)) • u p.1)) k⌋))).card : ℝ)) → (∀ n : ℕ, 2 ≤ n → n ≤ 4 → ∃ C : ℝ, 0 < C ∧ ∀ r : ℝ, 0 < r → ∀ (N : Fin n → ℕ) (a e : (i : Fin n) → Fin (N i) → EuclideanSpace ℝ (Fin n)) (w : (i : Fin n) → Fin (N i) → ℝ), (∀ (i : Fin n) (k : Fin (N i)), ‖e i k‖ = 1) → (∀ (i : Fin n) (k : Fin (N i)), 0 ≤ w i k) → MeasureTheory.lintegral MeasureTheory.volume (fun x : EuclideanSpace ℝ (Fin n) => ENNReal.ofReal ((∑ T : ((i : Fin n) → Fin (N i)), |Matrix.det (Matrix.of fun i j : Fin n => e i (T i) j)| * ∏ i : Fin n, (w i (T i) * (Metric.thickening r (Set.range fun t : ℝ => a i (T i) + t • e i (T i))).indicator (fun _ => (1 : ℝ)) x)) ^ ((1 : ℝ) / ((n : ℝ) - 1)))) ≤ ENNReal.ofReal (C * r ^ n * ∏ i : Fin n, (∑ k : Fin (N i), w i k) ^ ((1 : ℝ) / ((n : ℝ) - 1)))) → (∀ s : ℝ, 0 < s → s ≤ 1 → ∃ n : ℕ, 2 ≤ n ∧ ∃ r₀ ε₀ τ : ℝ, 0 < r₀ ∧ 0 < ε₀ ∧ 0 < τ ∧ ∀ r : ℝ, 0 < r → r < r₀ → ∀ μ : MeasureTheory.Measure ℝ, MeasureTheory.IsProbabilityMeasure μ → μ (Set.Icc (-1 : ℝ) 1)ᶜ = 0 → (∀ x u : ℝ, r ≤ u → u ≤ 1 → μ (Set.Icc (x - u) (x + u)) ≤ ENNReal.ofReal (r ^ (-ε₀) * u ^ s)) → ∀ ξ : ℝ, r⁻¹ ≤ |ξ| → |ξ| ≤ 2 * r⁻¹ → ‖MeasureTheory.integral (MeasureTheory.Measure.pi (fun _ : Fin n => μ)) (fun x : Fin n → ℝ => Complex.exp (((-2 * Real.pi * ξ * (∏ j : Fin n, x j) : ℝ) : ℂ) * Complex.I))‖ ≤ |ξ| ^ (-τ)) → (∃ c C₀ : ℝ, 0 < c ∧ 0 < C₀ ∧ ∀ (G : Type) [AddCommGroup G] [DecidableEq G] (A B : Finset G) (E : Finset (G × G)) (θ : ℝ), A.Nonempty → B.Nonempty → E ⊆ A ×ˢ B → 0 < θ → θ ≤ 1 → θ * (A.card : ℝ) * (B.card : ℝ) ≤ (E.card : ℝ) → ∃ A' : Finset G, ∃ B' : Finset G, A' ⊆ A ∧ B' ⊆ B ∧ c * θ * (A.card : ℝ) ≤ (A'.card : ℝ) ∧ c * θ * (B.card : ℝ) ≤ (B'.card : ℝ) ∧ c * θ ^ 2 * (A.card : ℝ) * (B.card : ℝ) ≤ ((E ∩ A' ×ˢ B').card : ℝ) ∧ (((A' ×ˢ B').image (fun p : G × G => p.1 + p.2)).card : ℝ) ≤ C₀ * (θ ^ 5)⁻¹ * ((E.image (fun p : G × G => p.1 + p.2)).card : ℝ) ^ 3 / ((A.card : ℝ) * (B.card : ℝ))) → (∃ C : ℝ, 0 < C ∧ ∀ (P : MvPolynomial (Fin 4) ℝ) (D : Matrix (Fin 2) (Fin 2) ℝ) (c u : EuclideanSpace ℝ (Fin 2)) (t₀ q a K R : ℝ), P.totalDegree ≤ 2 → Matrix.det D ≠ 0 → 0 < q → 0 < a → 1 ≤ K → 1 ≤ R → MeasureTheory.volume {s : EuclideanSpace ℝ (Fin 3) | ‖s‖ ≤ R ∧ ∃ b : EuclideanSpace ℝ (Fin 3), ‖b‖ ≤ R ∧ (∀ t ∈ Set.Icc t₀ (t₀ + q), ‖Matrix.toEuclideanLin (D⁻¹) (WithLp.toLp 2 (fun i : Fin 2 => (b + t • s) i.castSucc - c i - t * u i))‖ ≤ K ∧ |MvPolynomial.eval ![t, (b + t • s) 0, (b + t • s) 1, (b + t • s) 2] P| ≤ K * a) ∧ ∃ t ∈ Set.Icc t₀ (t₀ + q), K⁻¹ ≤ |MvPolynomial.eval ![t, (b + t • s) 0, (b + t • s) 1, (b + t • s) 2] (MvPolynomial.pderiv (3 : Fin 4) P)|} ≤ ENNReal.ofReal (C * K ^ 4 * a * |Matrix.det D| / q ^ 3)) → (∀ n D : ℕ, ∃ C : ℝ, 0 < C ∧ ∀ (P : MvPolynomial (Fin (n + 1)) ℂ) (f : EuclideanSpace ℂ (Fin n) → ℂ), P ≠ 0 → P.totalDegree ≤ D → DifferentiableOn ℂ f (Metric.ball 0 4) → (∀ z ∈ Metric.ball (0 : EuclideanSpace ℂ (Fin n)) 4, MvPolynomial.eval (Fin.snoc (fun i : Fin n => z i) (f z)) P = 0) → (∀ x : EuclideanSpace ℝ (Fin n), ‖x‖ ≤ (1 : ℝ) / 2 → ‖f (WithLp.toLp 2 (fun i : Fin n => (x i : ℂ)))‖ ≤ 1) → ∀ z : EuclideanSpace ℂ (Fin n), ‖z‖ ≤ 1 → ‖f z‖ ≤ C) → ∀ σ : ℝ, 0 < σ → σ ≤ 1 → ∀ c : ℝ, 0 < c → ∀ R : ℝ, 1 ≤ R → ∃ k₀ : ℕ, ∀ k : ℕ, k₀ ≤ k → ∀ (n : ℕ) (x v : Fin n → EuclideanSpace ℝ (Fin 4)), c * (2 : ℝ) ^ (3 * k) / ((k : ℝ) + 1) ^ 2 ≤ (n : ℝ) → (∀ i : Fin n, x i 0 = 0 ∧ v i 0 = 1 ∧ ‖v i‖ ≤ 2) → (∀ i j : Fin n, i ≠ j → (2 : ℝ) ^ (-(k : ℤ)) ≤ ‖v i - v j‖) → (∀ i : Fin n, ‖x i‖ ≤ R) → ∀ (m : ℕ) (z : Fin m → EuclideanSpace ℝ (Fin 4)) (ρ : Fin m → ℝ), (m : ℝ) ≤ (2 : ℝ) ^ (((k : ℝ) + 1) * (4 - σ)) → (∀ j : Fin m, (2 : ℝ) ^ (-((k : ℤ) + 1)) < ρ j ∧ ρ j ≤ (2 : ℝ) ^ (-(k : ℤ))) → ¬ (∀ i : Fin n, ENNReal.ofReal (c / ((k : ℝ) + 1) ^ 2) ≤ MeasureTheory.volume {t : ℝ | t ∈ Set.Icc (0 : ℝ) 1 ∧ x i + t • v i ∈ ⋃ j : Fin m, Metric.ball (z j) (ρ j)})k4_coreEverything else: T1, T3, T4, T5 imply the discrete estimate DK4 (no configuration of n ≥ c2^{3k}/(k+1)² 2^-k-separated graph directions v = (1, s), ‖v‖ ≤ 2, base points with x 0 = 0 in closedBall 0 R, whose segments t ↦ x + t v (t ∈ [0,1], time = coordinate 0) each spend time ≥ c/(k+1)² in a union of at most 2^{(k+1)(4-σ)} balls of radii in (2^-k-1, 2^-k], for all large k). Paper: the rest of Theorem 2.17 = thm:model-reduction (smoothing, the three density bounds, cap class C(d) = Def 2.6, positive horizon) and Sections 3-10 (exclusion of a bad problem). The planar dot-product input (paper Theorem 5.5 = a04:planar-input, used in Section 5) is the proved wang_zahl obligation o103: import WangZahlLot.Obl.wz_ad_projection_dichotomy, theorem WangZahlLot.wz_ad_projection_dichotomy. This tree freezes statements of up to 16000 characters, so the paper's own interface fits: the suggested first split (NOTES.md §2.5, route 1) is A = T1 → (no bad problem) → DK4 (the rest of Theorem 2.17) and B = T1 → T3 → T4 → T5 → no bad problem (Sections 3-10), the bad-problem predicate (Def 2.1 exact problem of version 2, tempered, homogeneous, cap class C(d) with 0 < d < 1, horizon H(E) > 0) written once and copied verbatim into both. Alternative (route 2): split off concrete self-contained lemmas as harvest leaves (NOTES.md §7 H8) and keep the framework remainder as one obligation.
(∀ ε : ℝ, 0 < ε → ∃ η : ℝ, 0 < η ∧ ∃ C : ℝ, 0 < C ∧ ∀ (D : ℕ), 1 ≤ D → ∀ (n : ℕ) (b u : Fin n → EuclideanSpace ℝ (Fin 2)) (ω : Fin n → ℝ) (A : ℝ) (J : Fin n → Finset (Fin D)), (∀ i : Fin n, ‖b i‖ ≤ 1 ∧ ‖u i‖ ≤ 1) → (∀ i : Fin n, 0 < ω i) → 0 < A → (∀ (c w e₁ e₂ : EuclideanSpace ℝ (Fin 2)) (a β : ℝ), ‖e₁‖ = 1 → ‖e₂‖ = 1 → inner ℝ e₁ e₂ = 0 → 1 ≤ a → a ≤ β → β ≤ (D : ℝ) → ∀ S : Finset (Fin n), (∀ i ∈ S, ∀ t ∈ Set.Icc (0 : ℝ) 1, |inner ℝ (b i + t • u i - c - t • w) e₁| ≤ a / (D : ℝ) ∧ |inner ℝ (b i + t • u i - c - t • w) e₂| ≤ β / (D : ℝ)) → ∑ i ∈ S, ω i ≤ A * a * β) → (∀ i : Fin n, (D : ℝ) ^ (1 - η) ≤ ((J i).card : ℝ)) → ∑ i : Fin n, ω i * ((J i).card : ℝ) ≤ C * A * (D : ℝ) ^ ε * ((((Finset.univ : Finset (Fin n)).sigma J).image (fun p => ((p.2 : ℕ), fun k : Fin 2 => ⌊(D : ℝ) * (b p.1 + (((((p.2 : ℕ) : ℝ) + 1 / 2) / (D : ℝ)) • u p.1)) k⌋))).card : ℝ)) → (∀ n : ℕ, 2 ≤ n → n ≤ 4 → ∃ C : ℝ, 0 < C ∧ ∀ r : ℝ, 0 < r → ∀ (N : Fin n → ℕ) (a e : (i : Fin n) → Fin (N i) → EuclideanSpace ℝ (Fin n)) (w : (i : Fin n) → Fin (N i) → ℝ), (∀ (i : Fin n) (k : Fin (N i)), ‖e i k‖ = 1) → (∀ (i : Fin n) (k : Fin (N i)), 0 ≤ w i k) → MeasureTheory.lintegral MeasureTheory.volume (fun x : EuclideanSpace ℝ (Fin n) => ENNReal.ofReal ((∑ T : ((i : Fin n) → Fin (N i)), |Matrix.det (Matrix.of fun i j : Fin n => e i (T i) j)| * ∏ i : Fin n, (w i (T i) * (Metric.thickening r (Set.range fun t : ℝ => a i (T i) + t • e i (T i))).indicator (fun _ => (1 : ℝ)) x)) ^ ((1 : ℝ) / ((n : ℝ) - 1)))) ≤ ENNReal.ofReal (C * r ^ n * ∏ i : Fin n, (∑ k : Fin (N i), w i k) ^ ((1 : ℝ) / ((n : ℝ) - 1)))) → (∀ s : ℝ, 0 < s → s ≤ 1 → ∃ n : ℕ, 2 ≤ n ∧ ∃ r₀ ε₀ τ : ℝ, 0 < r₀ ∧ 0 < ε₀ ∧ 0 < τ ∧ ∀ r : ℝ, 0 < r → r < r₀ → ∀ μ : MeasureTheory.Measure ℝ, MeasureTheory.IsProbabilityMeasure μ → μ (Set.Icc (-1 : ℝ) 1)ᶜ = 0 → (∀ x u : ℝ, r ≤ u → u ≤ 1 → μ (Set.Icc (x - u) (x + u)) ≤ ENNReal.ofReal (r ^ (-ε₀) * u ^ s)) → ∀ ξ : ℝ, r⁻¹ ≤ |ξ| → |ξ| ≤ 2 * r⁻¹ → ‖MeasureTheory.integral (MeasureTheory.Measure.pi (fun _ : Fin n => μ)) (fun x : Fin n → ℝ => Complex.exp (((-2 * Real.pi * ξ * (∏ j : Fin n, x j) : ℝ) : ℂ) * Complex.I))‖ ≤ |ξ| ^ (-τ)) → (∃ c C₀ : ℝ, 0 < c ∧ 0 < C₀ ∧ ∀ (G : Type) [AddCommGroup G] [DecidableEq G] (A B : Finset G) (E : Finset (G × G)) (θ : ℝ), A.Nonempty → B.Nonempty → E ⊆ A ×ˢ B → 0 < θ → θ ≤ 1 → θ * (A.card : ℝ) * (B.card : ℝ) ≤ (E.card : ℝ) → ∃ A' : Finset G, ∃ B' : Finset G, A' ⊆ A ∧ B' ⊆ B ∧ c * θ * (A.card : ℝ) ≤ (A'.card : ℝ) ∧ c * θ * (B.card : ℝ) ≤ (B'.card : ℝ) ∧ c * θ ^ 2 * (A.card : ℝ) * (B.card : ℝ) ≤ ((E ∩ A' ×ˢ B').card : ℝ) ∧ (((A' ×ˢ B').image (fun p : G × G => p.1 + p.2)).card : ℝ) ≤ C₀ * (θ ^ 5)⁻¹ * ((E.image (fun p : G × G => p.1 + p.2)).card : ℝ) ^ 3 / ((A.card : ℝ) * (B.card : ℝ))) → ∀ σ : ℝ, 0 < σ → σ ≤ 1 → ∀ c : ℝ, 0 < c → ∀ R : ℝ, 1 ≤ R → ∃ k₀ : ℕ, ∀ k : ℕ, k₀ ≤ k → ∀ (n : ℕ) (x v : Fin n → EuclideanSpace ℝ (Fin 4)), c * (2 : ℝ) ^ (3 * k) / ((k : ℝ) + 1) ^ 2 ≤ (n : ℝ) → (∀ i : Fin n, x i 0 = 0 ∧ v i 0 = 1 ∧ ‖v i‖ ≤ 2) → (∀ i j : Fin n, i ≠ j → (2 : ℝ) ^ (-(k : ℤ)) ≤ ‖v i - v j‖) → (∀ i : Fin n, ‖x i‖ ≤ R) → ∀ (m : ℕ) (z : Fin m → EuclideanSpace ℝ (Fin 4)) (ρ : Fin m → ℝ), (m : ℝ) ≤ (2 : ℝ) ^ (((k : ℝ) + 1) * (4 - σ)) → (∀ j : Fin m, (2 : ℝ) ^ (-((k : ℤ) + 1)) < ρ j ∧ ρ j ≤ (2 : ℝ) ^ (-(k : ℤ))) → ¬ (∀ i : Fin n, ENNReal.ofReal (c / ((k : ℝ) + 1) ^ 2) ≤ MeasureTheory.volume {t : ℝ | t ∈ Set.Icc (0 : ℝ) 1 ∧ x i + t • v i ∈ ⋃ j : Fin m, Metric.ball (z j) (ρ j)})import ChallengeDeps
/-- Theorem 1.1: a subset of `ℝ⁴` containing a unit line segment in every direction has
Hausdorff dimension `4`. -/
theorem kakeya_four_dimensions (K : Set (EuclideanSpace ℝ (Fin 4)))
(hK : ∀ e ∈ Metric.sphere (0 : EuclideanSpace ℝ (Fin 4)) 1,
∃ a : EuclideanSpace ℝ (Fin 4), segment ℝ a (a + e) ⊆ K) :
dimH K = 4 := by
sorry
The official root check is the unmodified pipeline from scratch, as Lean-Eval runs it, alone on the same isolated cores; it accepted the proof. LOT’s side of the root is measured after its chain run is measured again.官方根检查即 Lean-Eval 所用的未改动流程、从头检查，同样在独占锁定的核上单独运行；它接受了这份证明。LOT 一侧的根检查在链的 LOT 重新测完之后再测。
| Configuration配置 | Wall clock (min)用时（分钟） | CPU-hours used实际 CPU 小时 |
|---|---|---|
| Lean's original pipelineLean 原始流程 (12 h measured, rest estimated)（实测 12 小时，其余估计） | ≈ 952.8 | 122.816 (12 h) |
| LOT’s infrastructure (all five optimizations)LOT 基础设施（5 项优化全开） | pending待重测 | – |
| As it ran in the proved tree (that day’s pipeline, queueing included)证明树当时实际用时（当时的流程，含排队） | 44.4 | – |
Conditions: each run alone on 8 whole physical cores (16 CPUs, both hyperthreads) and 128 GiB of one NUMA node of one host (AMD EPYC 7B13), locked exclusively for that run so that no other process could use those CPUs; network off, every tool and library mounted read-only; Lean leanprover/lean4:v4.35.0-rc3. The original pipeline is the unmodified official checker[3,4] run once per level; queue waits and the scheduler’s pauses between levels are not counted for either lane. Measured on 2026-10-24.条件：每次运行单独占用同一台主机（AMD EPYC 7B13）一个 NUMA 节点上的 8 个完整物理核（16 个逻辑 CPU，含超线程）和 128 GiB 内存，运行期间独占锁定，其他进程用不了这些 CPU；断网，所有工具和库只读挂载；Lean leanprover/lean4:v4.35.0-rc3。原始流程是未经改动的官方检查器[3,4]，每层运行一次；两条泳道都不计排队等待和层与层之间调度器的停顿。测于 2026-10-24。