Bochner-Riesz Multipliers in Three Dimensions

What the two times are. Lean original is the wall-clock time to check the 10 levels one after another on one worker, each from scratch with the unmodified official checker. LOT’s infrastructure (all six 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 and speculative-checking optimizations, which act across a whole tree, have 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 上把这 10 层依次检查完的总用时，每层都用未改动的官方检查器从头检查。LOT 基础设施（6 项优化全开）：最新流程检查同一条链的总用时，先做一次复用下一层编译产物的探测编译，再用并行内核重放把整条链一次查完。在这次单独回放里，账本虽然开着但从空开始；排队和推测并行检查这两项是在整棵树的层面起作用的，这里没有可以重叠的东西。两个时间都不含根检查、排队等待和调度器的停顿。这条链不一定是这棵树里最长的：它是一次“收口”，即最底层定理证完后，上面各层依次变得可检查；挑选时兼顾规模和多样性。

Watch both checks, replayed side by side两遍检查并排回放

The chain: 10 levels, bottom to top这条链：10 层，自下而上

A level lights up when a run has checked it: red for the original pipeline, teal for the optimized one.某次运行检查完一层，该层就会亮起：红色是原始流程，青色是优化后的流程。

1. Level第 1 层 br3_selected_critical_information_profile

   From the frozen finite critical-aspect hypotheses and PROJ, construct a selected sorted/grouped information profile with coordinate capacities, mixed signs, obstacle/contact, the four closure rules for every inward affine tuple, and a positive local X-prefix gain at the path.

   Frozen statement (Lean)冻结语句（Lean）

   (∀d s α:ℝ,0 < d → d ≤ 2 → 0 < s → s ≤ 1 → 0 < α → ∃η ρ₁:ℝ,0 < η ∧ 0 < ρ₁ ∧ ∀ρ:ℝ,0 < ρ → ρ < ρ₁ → ∀(X:Finset (EuclideanSpace ℝ (Fin 2))) (μ:EuclideanSpace ℝ (Fin 2) → ℝ) (B:Finset ℕ) (ν a:ℕ → ℝ) (G:Finset (EuclideanSpace ℝ (Fin 2) × ℕ)) (M:ℕ),(∀x ∈ X,0 ≤ μ x ∧ |x 0| ≤ 1 ∧ |x 1| ≤ 1) → ∑ x ∈ X,μ x = 1 → (∀b ∈ B,0 ≤ ν b ∧ |a b| ≤ 1) → ∑ b ∈ B,ν b = 1 → (∀(z:EuclideanSpace ℝ (Fin 2)) (r:ℝ),ρ ≤ r → r ≤ 1 → ∑ x ∈ X.filter (fun x => dist x z ≤ r),μ x ≤ ρ^(-η)*r^d) → (∀t r:ℝ,ρ ≤ r → r ≤ 1 → ∑ b ∈ B.filter (fun b => |a b - t| ≤ r),ν b ≤ ρ^(-η)*r^s) → ρ^η ≤ ∑ p ∈ G.filter (fun p => p.1 ∈ X ∧ p.2 ∈ B),μ p.1*ν p.2 → (∀b ∈ B,∃S:Finset ℝ,S.card ≤ M ∧ ∀x ∈ X,(x,b) ∈ G → ∃c ∈ S,|x 1 - a b*x 0 - c| ≤ ρ) → ρ^(-(min 1 (min d ((d+s) / 2)))+α) ≤ (M:ℝ)) → ∀γ:ℝ,0 < γ → γ < 1 → ∀U:ℝ → ℝ → Prop,(∀β E:ℝ,U β E ↔ ∀κ:ℝ,0 < κ → ∃ρ₀:ℝ,0 < ρ₀ ∧ ∀ρ:ℝ,0 < ρ → ρ < min ρ₀ 1 → ∀a:ℝ,0 ≤ a → a ≤ E → ∀n m:ℕ,∀(p:Fin n → Fin m → ℝ) (μ:Fin n → ℝ) (ν:Fin m → ℝ) (V A₀:Fin n → ℂ) (c:Fin m → ℝ) (r z w:Fin m → ℂ) (h:ℝ),(∀i j,0 ≤ p i j) → (∑ i,∑ j,p i j) = 1 → (∀i,μ i = ∑ j,p i j) → (∀j,ν j = ∑ i,p i j) → (∀i,‖V i‖ ≤ 2 ∧ ‖A₀ i‖ ≤ 2) → (∀j,c j ∈ Set.Icc (0:ℝ) 1 ∧ ‖r j‖ = 1) → (∀j k,c j ≠ c k → ρ ≤ |c j - c k|) → (∀i j,0 < p i j → |((V i - z j)*r j).re| ≤ 1 ∧ |((V i - z j)*r j).im| ≤ ρ^a ∧ |((A₀ i+c j • V i - w j)*r j).re| ≤ ρ ∧ |((A₀ i+c j • V i - w j)*r j).im| ≤ ρ^(a+1)) → (∀B A:ℝ,∀R Z W:ℂ,0 ≤ B → B ≤ A → A ≤ 1+a → ‖R‖ = 1 → ∑ i ∈ Finset.univ.filter (fun i => |((V i - Z)*R).re| ≤ ρ^B ∧ |((V i - Z)*R).im| ≤ ρ^A ∧ |((A₀ i - W)*R).re| ≤ ρ^B ∧ |((A₀ i - W)*R).im| ≤ ρ^A),μ i ≤ ρ^((1+γ)*B+(1 - γ)*A - h)) → (1 - γ)*a - (∑ i,∑ j,p i j*(Real.log (p i j / (μ i*ν j))+2*Real.log ((∑ k,if c k = c j then p i k else 0) / μ i))) / Real.log (1 / ρ) ≤ h+β+κ) → ∀β:ℝ,γ < β → β ≤ 2 → (∀E:ℝ,0 ≤ E → U β E) → ∀m:ℝ,0 < m → (∀δ:ℝ,0 < δ → ¬ U (β - δ) m) → (∀E:ℝ,0 ≤ E → E < m → ∃δ:ℝ,0 < δ ∧ U (β - δ) E) → ∀(L:ℝ) (c:Fin 4 → ℝ) (W:Set (ℝ × ℝ)),L = 1+m → c = ![0,1,m,L] → W = {q|q.2 ∈ Set.Ioo 0 1} → ∃(n:ℕ) (v:Fin n → ℝ) (E:Finset (Fin n × Fin n)) (d:Fin (n+1) → ℝ) (r:Fin 4 → Fin n) (w:Fin 4 → ℝ) (K:NNReal) (f:(Fin (n+1) → ℝ) → ℝ) (b S:ℝ → ℝ) (τ:ℝ) (C Dm:Set (Fin (n+1) → ℝ)) (P:(ℝ × ℝ) → Fin (n+1) → ℝ), 2 ≤ n ∧ StrictMono v ∧ (∀e∈E,e.1 < e.2) ∧ (∀j,0 ≤ d j) ∧ (∀j,0 ≤ w j ∧ w j*d (r j).castSucc ≤ 1 ∧ v (r j)=c j) ∧ (∀k,(∑ j:Fin 4,if r j=k then w j else 0)=1) ∧ w 0=1 ∧ w 3=1 ∧ C={z|∀j k:Fin n,(j,k)∈E → z k.castSucc-z j.castSucc ≤ (v k-v j)*z (Fin.last n)} ∧ Dm={z|z∈C ∧ z (Fin.last n)∈Set.Ioo (0:ℝ) 1} ∧ P=(fun q=>Fin.snoc (fun j=>q.1+v j*q.2) q.2) ∧ LipschitzWith K f ∧ LipschitzWith K b ∧ LipschitzWith K S ∧ (∀z j t,z∈Dm → 0 ≤ t → z+t • Pi.single j 1∈Dm → 0 ≤ f (z+t • Pi.single j 1)-f z ∧ f (z+t • Pi.single j 1)-f z ≤ d j*t) ∧ (∀z j k (t s:ℝ),j ≠ k → 0 ≤ t → 0 ≤ s → z∈Dm → z+t • Pi.single j 1∈Dm → z+s • Pi.single k 1∈Dm → z+t • Pi.single j 1+s • Pi.single k 1∈Dm → f (z+t • Pi.single j 1+s • Pi.single k 1)-f (z+t • Pi.single j 1)-f (z+s • Pi.single k 1)+f z ≤ 0) ∧ (∀u∈Set.Ioo (0:ℝ) 1,0 ≤ b u ∧ b u+L*u ≤ L) ∧ (∀ᵐ u ∂MeasureTheory.volume.restrict (Set.Ioo (0:ℝ) 1),0 ≤ -deriv b u ∧ -deriv b u ≤ L ∧ 0 < deriv S u ∧ deriv S u ≤ 1) ∧ (∀q∈W,0 ≤ q.1 → q.1+L*q.2 ≤ L → 2*q.1+(1-γ)*m*q.2+2*S q.2-β*q.2 ≤ f (P q)+τ) ∧ (∀u∈Set.Ioo (0:ℝ) 1,f (P (b u,u))+τ=2*b u+(1-γ)*m*u+2*S u-β*u) ∧ (∀ᵐ q ∂MeasureTheory.volume.restrict W,0 < q.1 → q.1+L*q.2 < L → ∀(h:ℕ → ℝ) (A:Fin n → ℝ) (D x z s B F:ℝ),(∀l,0 < h l) → Filter.Tendsto h Filter.atTop (nhds (0:ℝ)) → (∀R ε:ℝ,0 < R → 0 < ε → ∀ᶠ l in Filter.atTop,∀ξ∈C,‖ξ‖ ≤ R → |(f (P q+h l • ξ)-f (P q))/h l-((∑ j,A j*ξ j.castSucc)+D*ξ (Fin.last n))| ≤ ε) → x=A (r 0) → z=A (r 3) → s=deriv S q.2 → B=(∑ j,A j)-2 → F=(∑ j,v j*A j)-m → (0 < x → z < 1 → 1+s ≤ F-L/2*B) ∧ (0 < x → 1+s ≤ F+L*(1-z)) ∧ (z < 1 → 1+s ≤ F-L*B+L*x) ∧ (0 < x → z < 1 → ∀t:ℝ,0 ≤ t → t ≤ L/2 → 1+s ≤ F-t*B+(L-t)*(1-z))) ∧ (∀u∈Set.Ioo (0:ℝ) 1,∃μ:ℝ,0 < μ ∧ ∀t:ℝ,0 ≤ t → t ≤ μ → γ*t ≤ f (P (b u,u)+t • Pi.single (r 0).castSucc 1)-f (P (b u,u)))

2. Level第 2 层 br3_critical_aspect_plane_certificate

   The exact universal finite beta cap estimate and a positive least critical aspect, under PROJ, produce bounded measurable matched plane rates and Lipschitz potential, path and time profiles. They obey weak derivative identities, local characteristic order-zero distribution bounds, the last-rate jump inequality, the obstacle and contact relation, generic midpoint/endpoint/capped closure bounds, and the earlier-time X wedge bound. The independent characteristic-plane theorem o079 is used in the proof as the existing dependency.

   Frozen statement (Lean)冻结语句（Lean）

   (∀ d s α:ℝ,0 < d → d ≤ 2 → 0 < s → s ≤ 1 → 0 < α → ∃ η ρ₁:ℝ,0 < η ∧ 0 < ρ₁ ∧ ∀ ρ:ℝ,0 < ρ → ρ < ρ₁ → ∀ (X:Finset (EuclideanSpace ℝ (Fin 2))) (μ:EuclideanSpace ℝ (Fin 2) → ℝ) (B:Finset ℕ) (ν a:ℕ → ℝ) (G:Finset (EuclideanSpace ℝ (Fin 2) × ℕ)) (M:ℕ),(∀ x ∈ X,0 ≤ μ x ∧ |x 0| ≤ 1 ∧ |x 1| ≤ 1) → ∑ x ∈ X,μ x = 1 → (∀ b ∈ B,0 ≤ ν b ∧ |a b| ≤ 1) → ∑ b ∈ B,ν b = 1 → (∀ (z:EuclideanSpace ℝ (Fin 2)) (r:ℝ),ρ ≤ r → r ≤ 1 → ∑ x ∈ X.filter (fun x => dist x z ≤ r),μ x ≤ ρ^(-η)*r^d) → (∀ t r:ℝ,ρ ≤ r → r ≤ 1 → ∑ b ∈ B.filter (fun b => |a b - t| ≤ r),ν b ≤ ρ^(-η)*r^s) → ρ^η ≤ ∑ p ∈ G.filter (fun p => p.1 ∈ X ∧ p.2 ∈ B),μ p.1*ν p.2 → (∀ b ∈ B,∃ S:Finset ℝ,S.card ≤ M ∧ ∀ x ∈ X,(x,b) ∈ G → ∃ c ∈ S,|x 1 - a b*x 0 - c| ≤ ρ) → ρ^(-(min 1 (min d ((d+s) / 2)))+α) ≤ (M:ℝ)) → ∀ γ:ℝ,0 < γ → γ < 1 → ∀ U:ℝ → ℝ → Prop,(∀ β E:ℝ,U β E ↔ ∀ κ:ℝ,0 < κ → ∃ ρ₀:ℝ,0 < ρ₀ ∧ ∀ ρ:ℝ,0 < ρ → ρ < min ρ₀ 1 → ∀ a:ℝ,0 ≤ a → a ≤ E → ∀ n m:ℕ,∀ (p:Fin n → Fin m → ℝ) (μ:Fin n → ℝ) (ν:Fin m → ℝ) (V A₀:Fin n → ℂ) (c:Fin m → ℝ) (r z w:Fin m → ℂ) (h:ℝ),(∀ i j,0 ≤ p i j) → (∑ i,∑ j,p i j) = 1 → (∀ i,μ i = ∑ j,p i j) → (∀ j,ν j = ∑ i,p i j) → (∀ i,‖V i‖ ≤ 2 ∧ ‖A₀ i‖ ≤ 2) → (∀ j,c j ∈ Set.Icc (0:ℝ) 1 ∧ ‖r j‖ = 1) → (∀ j k,c j ≠ c k → ρ ≤ |c j - c k|) → (∀ i j,0 < p i j → |((V i - z j)*r j).re| ≤ 1 ∧ |((V i - z j)*r j).im| ≤ ρ^a ∧ |((A₀ i+c j • V i - w j)*r j).re| ≤ ρ ∧ |((A₀ i+c j • V i - w j)*r j).im| ≤ ρ^(a+1)) → (∀ B A:ℝ,∀ R Z W:ℂ,0 ≤ B → B ≤ A → A ≤ 1+a → ‖R‖ = 1 → ∑ i ∈ Finset.univ.filter (fun i => |((V i - Z)*R).re| ≤ ρ^B ∧ |((V i - Z)*R).im| ≤ ρ^A ∧ |((A₀ i - W)*R).re| ≤ ρ^B ∧ |((A₀ i - W)*R).im| ≤ ρ^A),μ i ≤ ρ^((1+γ)*B+(1 - γ)*A - h)) → (1 - γ)*a - (∑ i,∑ j,p i j*(Real.log (p i j / (μ i*ν j))+2*Real.log ((∑ k,if c k = c j then p i k else 0) / μ i))) / Real.log (1 / ρ) ≤ h+β+κ) → ∀ β:ℝ,γ < β → β ≤ 2 → (∀ E:ℝ,0 ≤ E → U β E) → ∀ m:ℝ,0 < m → (∀ δ:ℝ,0 < δ → ¬ U (β - δ) m) → (∀ E:ℝ,0 ≤ E → E < m → ∃ δ:ℝ,0 < δ ∧ U (β - δ) E) → ∀ (L:ℝ) (c:Fin 4 → ℝ) (W:Set (ℝ × ℝ)),L = 1+m → c = ![0,1,m,L] → W = {q|q.2 ∈ Set.Ioo (0:ℝ) 1} → ∃ (K:NNReal) (a:Fin 4 → (ℝ × ℝ) → ℝ) (D Φ:(ℝ × ℝ) → ℝ) (b S:ℝ → ℝ),LipschitzWith K Φ ∧ LipschitzWith K b ∧ LipschitzWith K S ∧ (∀ j,Measurable (a j)) ∧ Measurable D ∧ (∃ M:ℝ,∀ q,(∀ j,0 ≤ a j q ∧ a j q ≤ 1) ∧ 0 ≤ D q ∧ D q ≤ M) ∧ (∀ φ:(ℝ × ℝ) → ℝ,ContDiff ℝ 1 φ → HasCompactSupport φ → tsupport φ ⊆ W → (∫ q,Φ q*(fderiv ℝ φ q) (1,0)) = -(∫ q,(∑ j,a j q)*φ q) ∧ (∫ q,Φ q*(fderiv ℝ φ q) (0,1)) = -(∫ q,((∑ j,c j*a j q)+D q)*φ q) ∧ ((∀ q,0 ≤ φ q) → (∫ q,a 3 q*(fderiv ℝ φ q) (-L,1)) ≤ (∫ q,D q*(fderiv ℝ φ q) (1,0)))) ∧ (∀ Q:Set (ℝ × ℝ),IsCompact Q → Q ⊆ W → ∃ M:ℝ,∀ φ:(ℝ × ℝ) → ℝ,ContDiff ℝ 1 φ → tsupport φ ⊆ Q → (∀ q,|φ q| ≤ 1) → (∀ j,|(∫ q,a j q*(fderiv ℝ φ q) (-c j,1))| ≤ M) ∧ |(∫ q,D q*(fderiv ℝ φ q) (1,0))| ≤ M) ∧ (∀ u ∈ Set.Ioo (0:ℝ) 1,0 ≤ b u ∧ b u+L*u ≤ L) ∧ (∀ᵐ u ∂MeasureTheory.volume.restrict (Set.Ioo (0:ℝ) 1),0 ≤ -deriv b u ∧ -deriv b u ≤ L ∧ 0 < deriv S u ∧ deriv S u ≤ 1) ∧ (∀ q ∈ W,0 ≤ q.1 → q.1+L*q.2 ≤ L → 2*q.1+(1-γ)*m*q.2+2*S q.2-β*q.2 ≤ Φ q) ∧ (∀ u ∈ Set.Ioo (0:ℝ) 1,Φ (b u,u) = 2*b u+(1-γ)*m*u+2*S u-β*u) ∧ (∀ᵐ q ∂MeasureTheory.volume.restrict W,0 < q.1 → q.1+L*q.2 < L → ∀ x z s B F:ℝ,x = a 0 q → z = a 3 q → s = deriv S q.2 → B = (∑ j,a j q)-2 → F = (∑ j,c j*a j q)-m → (0 < x → z < 1 → 1+s ≤ F-L/2*B) ∧ (0 < x → 1+s ≤ F+L*(1-z)) ∧ (z < 1 → 1+s ≤ F-L*B+L*x) ∧ (0 < x → z < 1 → ∀ v:ℝ,0 ≤ v → v ≤ L/2 → 1+s ≤ F-v*B+(L-v)*(1-z))) ∧ (∀ l:ℝ,0 < l → l < min 1 m → ∀ u ∈ Set.Ioo (0:ℝ) 1,∃ e:ℝ,0 < e ∧ e < u ∧ ∀ᵐ h ∂MeasureTheory.volume.restrict (Set.Ioo (0:ℝ) e),γ*l*h ≤ ∫ i in Set.Icc (b u) (b u+l*h),a 0 (i,u-h))

3. Level第 3 层 br3_positive_least_critical_aspect_exclusion

   Assuming the general characteristic-plane affine-decomposition principle, PROJ and the exact universal beta cap bound forbid a positive least critical compact aspect when gamma<beta<=2: every strictly smaller nonnegative compact aspect already has a strict rate gap. Paths, profiles, transverse curve traces, finite cores and shear laws must be constructed inside its proof.

   Frozen statement (Lean)冻结语句（Lean）

   (∀ n:ℕ,2 ≤ n → ∀ c:Fin n → ℝ,StrictMono c → ∀ E:Finset (Fin n × Fin n),(∀ e ∈ E,e.1 < e.2) → ∀ d:Fin (n+1) → ℝ,(∀ j,0 ≤ d j) → ∀ (K:NNReal) (f:(Fin (n+1) → ℝ) → ℝ),LipschitzWith K f → ∀ (C:Set (Fin (n+1) → ℝ)),C = ({z | ∀ j k:Fin n,(j,k) ∈ E → z k.castSucc - z j.castSucc ≤ (c k - c j)*z (Fin.last n)}) → ∀ (Dm:Set (Fin (n+1) → ℝ)),Dm = ({z | z ∈ C ∧ z (Fin.last n) ∈ Set.Ioo (0:ℝ) 1}) → ∀ (W:Set (ℝ × ℝ)),W = ({q | q.2 ∈ Set.Ioo (0:ℝ) 1}) → ∀ (P:(ℝ × ℝ) → Fin (n+1) → ℝ),P = (fun q => Fin.snoc (fun j => q.1+c j*q.2) q.2) → (∀ (z:Fin (n+1) → ℝ) (j:Fin (n+1)) (t:ℝ),z ∈ Dm → 0 ≤ t → z+t • Pi.single j 1 ∈ Dm → 0 ≤ f (z+t • Pi.single j 1) - f z ∧ f (z+t • Pi.single j 1) - f z ≤ d j*t) → (∀ (z:Fin (n+1) → ℝ) (j k:Fin (n+1)) (t s:ℝ),j ≠ k → 0 ≤ t → 0 ≤ s → z ∈ Dm → z+t • Pi.single j 1 ∈ Dm → z+s • Pi.single k 1 ∈ Dm → z+t • Pi.single j 1+s • Pi.single k 1 ∈ Dm → f (z+t • Pi.single j 1+s • Pi.single k 1) - f (z+t • Pi.single j 1) - f (z+s • Pi.single k 1)+f z ≤ 0) → ∃ (a:Fin n → (ℝ × ℝ) → ℝ) (D:(ℝ × ℝ) → ℝ) (ν:Fin n → Fin n → MeasureTheory.Measure (ℝ × ℝ)) (σ:Fin n → MeasureTheory.Measure (ℝ × ℝ)) (h:ℕ → ℝ),(∀ j,Measurable (a j)) ∧ Measurable D ∧ (∀ j q,0 ≤ a j q ∧ a j q ≤ d j.castSucc) ∧ (∀ q,0 ≤ D q ∧ D q ≤ d (Fin.last n)) ∧ (∀ j k,ν j k = ν k j) ∧ (∀ j,ν j j = 0) ∧ (∀ j k (Q:Set (ℝ × ℝ)),IsCompact Q → Q ⊆ W → ν j k Q < ⊤) ∧ (∀ j (Q:Set (ℝ × ℝ)),IsCompact Q → Q ⊆ W → σ j Q < ⊤) ∧ (∀ φ:(ℝ × ℝ) → ℝ,ContDiff ℝ 1 φ → HasCompactSupport φ → tsupport φ ⊆ W → (∫ q,f (P q)*(fderiv ℝ φ q) (1,0)) = -(∫ q,(∑ j,a j q)*φ q) ∧ (∫ q,f (P q)*(fderiv ℝ φ q) (0,1)) = -(∫ q,((∑ j,c j*a j q)+D q)*φ q) ∧ (∀ j,(∫ q,a j q*(fderiv ℝ φ q) (-c j,1)) = (∫ q,φ q ∂σ j)+∑ k,(c k - c j)*(∫ q,φ q ∂ν j k)) ∧ (∫ q,D q*(fderiv ℝ φ q) (1,0)) = ∑ j,∫ q,φ q ∂σ j) ∧ (∀ l,0 < h l) ∧ Filter.Tendsto h Filter.atTop (nhds (0:ℝ)) ∧ (∀ᵐ q ∂MeasureTheory.volume.restrict W,∀ R ε:ℝ,0 < R → 0 < ε → ∀ᶠ l in Filter.atTop,∀ ξ:Fin (n+1) → ℝ,ξ ∈ C → ‖ξ‖ ≤ R → |(f (P q+h l • ξ) - f (P q)) / h l - ((∑ j,a j q*ξ j.castSucc)+D q*ξ (Fin.last n))| ≤ ε)) → (∀ d s α:ℝ,0 < d → d ≤ 2 → 0 < s → s ≤ 1 → 0 < α → ∃ η ρ₁:ℝ,0 < η ∧ 0 < ρ₁ ∧ ∀ ρ:ℝ,0 < ρ → ρ < ρ₁ → ∀ (X:Finset (EuclideanSpace ℝ (Fin 2))) (μ:EuclideanSpace ℝ (Fin 2) → ℝ) (B:Finset ℕ) (ν a:ℕ → ℝ) (G:Finset (EuclideanSpace ℝ (Fin 2) × ℕ)) (M:ℕ),(∀ x ∈ X,0 ≤ μ x ∧ |x 0| ≤ 1 ∧ |x 1| ≤ 1) → ∑ x ∈ X,μ x = 1 → (∀ b ∈ B,0 ≤ ν b ∧ |a b| ≤ 1) → ∑ b ∈ B,ν b = 1 → (∀ (z:EuclideanSpace ℝ (Fin 2)) (r:ℝ),ρ ≤ r → r ≤ 1 → ∑ x ∈ X.filter (fun x => dist x z ≤ r),μ x ≤ ρ^(-η)*r^d) → (∀ t r:ℝ,ρ ≤ r → r ≤ 1 → ∑ b ∈ B.filter (fun b => |a b - t| ≤ r),ν b ≤ ρ^(-η)*r^s) → ρ^η ≤ ∑ p ∈ G.filter (fun p => p.1 ∈ X ∧ p.2 ∈ B),μ p.1*ν p.2 → (∀ b ∈ B,∃ S:Finset ℝ,S.card ≤ M ∧ ∀ x ∈ X,(x,b) ∈ G → ∃ c ∈ S,|x 1 - a b*x 0 - c| ≤ ρ) → ρ^(-(min 1 (min d ((d+s) / 2)))+α) ≤ (M:ℝ)) → ∀ γ:ℝ,0 < γ → γ < 1 → ∀ U:ℝ → ℝ → Prop,(∀ β E:ℝ,U β E ↔ ∀ κ:ℝ,0 < κ → ∃ ρ₀:ℝ,0 < ρ₀ ∧ ∀ ρ:ℝ,0 < ρ → ρ < min ρ₀ 1 → ∀ a:ℝ,0 ≤ a → a ≤ E → ∀ n m:ℕ,∀ (p:Fin n → Fin m → ℝ) (μ:Fin n → ℝ) (ν:Fin m → ℝ) (V A₀:Fin n → ℂ) (c:Fin m → ℝ) (r z w:Fin m → ℂ) (h:ℝ),(∀ i j,0 ≤ p i j) → (∑ i,∑ j,p i j) = 1 → (∀ i,μ i = ∑ j,p i j) → (∀ j,ν j = ∑ i,p i j) → (∀ i,‖V i‖ ≤ 2 ∧ ‖A₀ i‖ ≤ 2) → (∀ j,c j ∈ Set.Icc (0:ℝ) 1 ∧ ‖r j‖ = 1) → (∀ j k,c j ≠ c k → ρ ≤ |c j - c k|) → (∀ i j,0 < p i j → |((V i - z j)*r j).re| ≤ 1 ∧ |((V i - z j)*r j).im| ≤ ρ^a ∧ |((A₀ i+c j • V i - w j)*r j).re| ≤ ρ ∧ |((A₀ i+c j • V i - w j)*r j).im| ≤ ρ^(a+1)) → (∀ B A:ℝ,∀ R Z W:ℂ,0 ≤ B → B ≤ A → A ≤ 1+a → ‖R‖ = 1 → ∑ i ∈ Finset.univ.filter (fun i => |((V i - Z)*R).re| ≤ ρ^B ∧ |((V i - Z)*R).im| ≤ ρ^A ∧ |((A₀ i - W)*R).re| ≤ ρ^B ∧ |((A₀ i - W)*R).im| ≤ ρ^A),μ i ≤ ρ^((1+γ)*B+(1 - γ)*A - h)) → (1 - γ)*a - (∑ i,∑ j,p i j*(Real.log (p i j / (μ i*ν j))+2*Real.log ((∑ k,if c k = c j then p i k else 0) / μ i))) / Real.log (1 / ρ) ≤ h+β+κ) → ∀ β:ℝ,γ < β → β ≤ 2 → (∀ E:ℝ,0 ≤ E → U β E) → ∀ m:ℝ,0 < m → (∀ δ:ℝ,0 < δ → ¬ U (β - δ) m) → (∀ E:ℝ,0 ≤ E → E < m → ∃ δ:ℝ,0 < δ ∧ U (β - δ) E) → False

4. Level第 4 层 br3_compact_positive_aspect_rate_improvement

   Under the weighted planar projection hypothesis, a universal rate gamma<beta<=2 for the exact finite cap estimate and a strict gap on some positive aspect neighborhood imply a strict gap on each fixed compact aspect range [0,E]. The decrement is allowed to depend on E, as is the precision threshold.

   Frozen statement (Lean)冻结语句（Lean）

   (∀ d s α : ℝ, 0 < d → d ≤ 2 → 0 < s → s ≤ 1 → 0 < α → ∃ η ρ₁ : ℝ, 0 < η ∧ 0 < ρ₁ ∧ ∀ ρ : ℝ, 0 < ρ → ρ < ρ₁ → ∀ (X : Finset (EuclideanSpace ℝ (Fin 2))) (μ : EuclideanSpace ℝ (Fin 2) → ℝ) (B : Finset ℕ) (ν a : ℕ → ℝ) (G : Finset (EuclideanSpace ℝ (Fin 2) × ℕ)) (M : ℕ), (∀ x ∈ X, 0 ≤ μ x ∧ |x 0| ≤ 1 ∧ |x 1| ≤ 1) → ∑ x ∈ X, μ x = 1 → (∀ b ∈ B, 0 ≤ ν b ∧ |a b| ≤ 1) → ∑ b ∈ B, ν b = 1 → (∀ (z : EuclideanSpace ℝ (Fin 2)) (r : ℝ), ρ ≤ r → r ≤ 1 → ∑ x ∈ X.filter (fun x => dist x z ≤ r), μ x ≤ ρ ^ (-η) * r ^ d) → (∀ t r : ℝ, ρ ≤ r → r ≤ 1 → ∑ b ∈ B.filter (fun b => |a b - t| ≤ r), ν b ≤ ρ ^ (-η) * r ^ s) → ρ ^ η ≤ ∑ p ∈ G.filter (fun p => p.1 ∈ X ∧ p.2 ∈ B), μ p.1 * ν p.2 → (∀ b ∈ B, ∃ S : Finset ℝ, S.card ≤ M ∧ ∀ x ∈ X, (x, b) ∈ G → ∃ c ∈ S, |x 1 - a b * x 0 - c| ≤ ρ) → ρ ^ (-(min 1 (min d ((d + s) / 2))) + α) ≤ (M : ℝ)) → ∀ γ : ℝ, 0 < γ → γ < 1 → ∀ U : ℝ → ℝ → Prop, (∀ β E : ℝ, U β E ↔ ∀ κ : ℝ, 0 < κ → ∃ ρ₀ : ℝ, 0 < ρ₀ ∧ ∀ ρ : ℝ, 0 < ρ → ρ < min ρ₀ 1 → ∀ a : ℝ, 0 ≤ a → a ≤ E → ∀ n m : ℕ, ∀ (p : Fin n → Fin m → ℝ) (μ : Fin n → ℝ) (ν : Fin m → ℝ) (V A₀ : Fin n → ℂ) (c : Fin m → ℝ) (r z w : Fin m → ℂ) (h : ℝ), (∀ i j, 0 ≤ p i j) → (∑ i, ∑ j, p i j) = 1 → (∀ i, μ i = ∑ j, p i j) → (∀ j, ν j = ∑ i, p i j) → (∀ i, ‖V i‖ ≤ 2 ∧ ‖A₀ i‖ ≤ 2) → (∀ j, c j ∈ Set.Icc (0 : ℝ) 1 ∧ ‖r j‖ = 1) → (∀ j k, c j ≠ c k → ρ ≤ |c j - c k|) → (∀ i j, 0 < p i j → |((V i - z j) * r j).re| ≤ 1 ∧ |((V i - z j) * r j).im| ≤ ρ ^ a ∧ |((A₀ i + c j • V i - w j) * r j).re| ≤ ρ ∧ |((A₀ i + c j • V i - w j) * r j).im| ≤ ρ ^ (a + 1)) → (∀ B A : ℝ, ∀ R Z W : ℂ, 0 ≤ B → B ≤ A → A ≤ 1 + a → ‖R‖ = 1 → ∑ i ∈ Finset.univ.filter (fun i => |((V i - Z) * R).re| ≤ ρ ^ B ∧ |((V i - Z) * R).im| ≤ ρ ^ A ∧ |((A₀ i - W) * R).re| ≤ ρ ^ B ∧ |((A₀ i - W) * R).im| ≤ ρ ^ A), μ i ≤ ρ ^ ((1 + γ) * B + (1 - γ) * A - h)) → (1 - γ) * a - (∑ i, ∑ j, p i j * (Real.log (p i j / (μ i * ν j)) + 2 * Real.log ((∑ k, if c k = c j then p i k else 0) / μ i))) / Real.log (1 / ρ) ≤ h + β + κ) → ∀ β : ℝ, γ < β → β ≤ 2 → (∀ E : ℝ, 0 ≤ E → U β E) → (∃ A δ : ℝ, 0 < A ∧ 0 < δ ∧ U (β - δ) A) → ∀ E : ℝ, 0 ≤ E → ∃ δ : ℝ, 0 < δ ∧ U (β - δ) E

5. Level第 5 层 br3_positive_aspect_rate_improvement

   Assume the weighted planar projection hypothesis. With U exactly the displayed finite cap estimate, gamma<beta<=2 and a universal beta bound, a strict rate gap on one positive aspect neighborhood forces a strict improvement of the universal beta rate on every compact aspect range. The new precision threshold may depend on that range and the requested loss.

   Frozen statement (Lean)冻结语句（Lean）

   (∀ d s α : ℝ, 0 < d → d ≤ 2 → 0 < s → s ≤ 1 → 0 < α → ∃ η ρ₁ : ℝ, 0 < η ∧ 0 < ρ₁ ∧ ∀ ρ : ℝ, 0 < ρ → ρ < ρ₁ → ∀ (X : Finset (EuclideanSpace ℝ (Fin 2))) (μ : EuclideanSpace ℝ (Fin 2) → ℝ) (B : Finset ℕ) (ν a : ℕ → ℝ) (G : Finset (EuclideanSpace ℝ (Fin 2) × ℕ)) (M : ℕ), (∀ x ∈ X, 0 ≤ μ x ∧ |x 0| ≤ 1 ∧ |x 1| ≤ 1) → ∑ x ∈ X, μ x = 1 → (∀ b ∈ B, 0 ≤ ν b ∧ |a b| ≤ 1) → ∑ b ∈ B, ν b = 1 → (∀ (z : EuclideanSpace ℝ (Fin 2)) (r : ℝ), ρ ≤ r → r ≤ 1 → ∑ x ∈ X.filter (fun x => dist x z ≤ r), μ x ≤ ρ ^ (-η) * r ^ d) → (∀ t r : ℝ, ρ ≤ r → r ≤ 1 → ∑ b ∈ B.filter (fun b => |a b - t| ≤ r), ν b ≤ ρ ^ (-η) * r ^ s) → ρ ^ η ≤ ∑ p ∈ G.filter (fun p => p.1 ∈ X ∧ p.2 ∈ B), μ p.1 * ν p.2 → (∀ b ∈ B, ∃ S : Finset ℝ, S.card ≤ M ∧ ∀ x ∈ X, (x, b) ∈ G → ∃ c ∈ S, |x 1 - a b * x 0 - c| ≤ ρ) → ρ ^ (-(min 1 (min d ((d + s) / 2))) + α) ≤ (M : ℝ)) → (∀ γ : ℝ, 0 < γ → γ < 1 → ∀ U : ℝ → ℝ → Prop, (∀ β E : ℝ, U β E ↔ ∀ κ : ℝ, 0 < κ → ∃ ρ₀ : ℝ, 0 < ρ₀ ∧ ∀ ρ : ℝ, 0 < ρ → ρ < min ρ₀ 1 → ∀ a : ℝ, 0 ≤ a → a ≤ E → ∀ n m : ℕ, ∀ (p : Fin n → Fin m → ℝ) (μ : Fin n → ℝ) (ν : Fin m → ℝ) (V A₀ : Fin n → ℂ) (c : Fin m → ℝ) (r z w : Fin m → ℂ) (h : ℝ), (∀ i j, 0 ≤ p i j) → (∑ i, ∑ j, p i j) = 1 → (∀ i, μ i = ∑ j, p i j) → (∀ j, ν j = ∑ i, p i j) → (∀ i, ‖V i‖ ≤ 2 ∧ ‖A₀ i‖ ≤ 2) → (∀ j, c j ∈ Set.Icc (0 : ℝ) 1 ∧ ‖r j‖ = 1) → (∀ j k, c j ≠ c k → ρ ≤ |c j - c k|) → (∀ i j, 0 < p i j → |((V i - z j) * r j).re| ≤ 1 ∧ |((V i - z j) * r j).im| ≤ ρ ^ a ∧ |((A₀ i + c j • V i - w j) * r j).re| ≤ ρ ∧ |((A₀ i + c j • V i - w j) * r j).im| ≤ ρ ^ (a + 1)) → (∀ B A : ℝ, ∀ R Z W : ℂ, 0 ≤ B → B ≤ A → A ≤ 1 + a → ‖R‖ = 1 → ∑ i ∈ Finset.univ.filter (fun i => |((V i - Z) * R).re| ≤ ρ ^ B ∧ |((V i - Z) * R).im| ≤ ρ ^ A ∧ |((A₀ i - W) * R).re| ≤ ρ ^ B ∧ |((A₀ i - W) * R).im| ≤ ρ ^ A), μ i ≤ ρ ^ ((1 + γ) * B + (1 - γ) * A - h)) → (1 - γ) * a - (∑ i, ∑ j, p i j * (Real.log (p i j / (μ i * ν j)) + 2 * Real.log ((∑ k, if c k = c j then p i k else 0) / μ i))) / Real.log (1 / ρ) ≤ h + β + κ) → ∀ β : ℝ, γ < β → β ≤ 2 → (∀ E : ℝ, 0 ≤ E → U β E) → (∃ A δ : ℝ, 0 < A ∧ 0 < δ ∧ U (β - δ) A) → ∃ δ : ℝ, 0 < δ ∧ ∀ E : ℝ, 0 ≤ E → U (β - δ) E)

6. Level第 6 层 br3_unit_shape_cap_transport

   The weighted planar projection hypothesis implies uniform finite cap transport in the fixed norm-2 domain, for duration one, one common column shape (0,a), and the minimal horizon 1+a, uniformly for a in any prescribed compact interval [0,E].

   Frozen statement (Lean)冻结语句（Lean）

   (∀ d s α : ℝ, 0 < d → d ≤ 2 → 0 < s → s ≤ 1 → 0 < α → ∃ η ρ₁ : ℝ, 0 < η ∧ 0 < ρ₁ ∧ ∀ ρ : ℝ, 0 < ρ → ρ < ρ₁ → ∀ (X : Finset (EuclideanSpace ℝ (Fin 2))) (μ : EuclideanSpace ℝ (Fin 2) → ℝ) (B : Finset ℕ) (ν a : ℕ → ℝ) (G : Finset (EuclideanSpace ℝ (Fin 2) × ℕ)) (M : ℕ), (∀ x ∈ X, 0 ≤ μ x ∧ |x 0| ≤ 1 ∧ |x 1| ≤ 1) → ∑ x ∈ X, μ x = 1 → (∀ b ∈ B, 0 ≤ ν b ∧ |a b| ≤ 1) → ∑ b ∈ B, ν b = 1 → (∀ (z : EuclideanSpace ℝ (Fin 2)) (r : ℝ), ρ ≤ r → r ≤ 1 → ∑ x ∈ X.filter (fun x => dist x z ≤ r), μ x ≤ ρ ^ (-η) * r ^ d) → (∀ t r : ℝ, ρ ≤ r → r ≤ 1 → ∑ b ∈ B.filter (fun b => |a b - t| ≤ r), ν b ≤ ρ ^ (-η) * r ^ s) → ρ ^ η ≤ ∑ p ∈ G.filter (fun p => p.1 ∈ X ∧ p.2 ∈ B), μ p.1 * ν p.2 → (∀ b ∈ B, ∃ S : Finset ℝ, S.card ≤ M ∧ ∀ x ∈ X, (x, b) ∈ G → ∃ c ∈ S, |x 1 - a b * x 0 - c| ≤ ρ) → ρ ^ (-(min 1 (min d ((d + s) / 2))) + α) ≤ (M : ℝ)) → (∀ γ κ E : ℝ, 0 < γ → γ < 1 → 0 < κ → 0 ≤ E → ∃ ρ₀ : ℝ, 0 < ρ₀ ∧ ∀ ρ : ℝ, 0 < ρ → ρ < min ρ₀ 1 → ∀ a : ℝ, 0 ≤ a → a ≤ E → ∀ n m : ℕ, ∀ (p : Fin n → Fin m → ℝ) (μ : Fin n → ℝ) (ν : Fin m → ℝ) (V A₀ : Fin n → ℂ) (c : Fin m → ℝ) (r z w : Fin m → ℂ) (h : ℝ), (∀ i j, 0 ≤ p i j) → (∑ i, ∑ j, p i j) = 1 → (∀ i, μ i = ∑ j, p i j) → (∀ j, ν j = ∑ i, p i j) → (∀ i, ‖V i‖ ≤ 2 ∧ ‖A₀ i‖ ≤ 2) → (∀ j, c j ∈ Set.Icc (0 : ℝ) 1 ∧ ‖r j‖ = 1) → (∀ j k, c j ≠ c k → ρ ≤ |c j - c k|) → (∀ i j, 0 < p i j → |((V i - z j) * r j).re| ≤ 1 ∧ |((V i - z j) * r j).im| ≤ ρ ^ a ∧ |((A₀ i + c j • V i - w j) * r j).re| ≤ ρ ∧ |((A₀ i + c j • V i - w j) * r j).im| ≤ ρ ^ (a + 1)) → (∀ B A : ℝ, ∀ R Z W : ℂ, 0 ≤ B → B ≤ A → A ≤ 1 + a → ‖R‖ = 1 → ∑ i ∈ Finset.univ.filter (fun i => |((V i - Z) * R).re| ≤ ρ ^ B ∧ |((V i - Z) * R).im| ≤ ρ ^ A ∧ |((A₀ i - W) * R).re| ≤ ρ ^ B ∧ |((A₀ i - W) * R).im| ≤ ρ ^ A), μ i ≤ ρ ^ ((1 + γ) * B + (1 - γ) * A - h)) → (1 - γ) * a - (∑ i, ∑ j, p i j * (Real.log (p i j / (μ i * ν j)) + 2 * Real.log ((∑ k, if c k = c j then p i k else 0) / μ i))) / Real.log (1 / ρ) ≤ h + γ + κ)

7. Level第 7 层 br3_transport_of_cap_bounds

   The weighted planar projection hypothesis implies the uniform finite positive-transport estimate for particle laws satisfying an explicit mass bound mu(cap)<=epsilon^(weight-h) for every exact duration-zero cap. This isolates the geometric growth argument from the arbitrary variational root-score premise.

   Frozen statement (Lean)冻结语句（Lean）

   (∀ d s α : ℝ, 0 < d → d ≤ 2 → 0 < s → s ≤ 1 → 0 < α → ∃ η ρ₁ : ℝ, 0 < η ∧ 0 < ρ₁ ∧ ∀ ρ : ℝ, 0 < ρ → ρ < ρ₁ → ∀ (X : Finset (EuclideanSpace ℝ (Fin 2))) (μ : EuclideanSpace ℝ (Fin 2) → ℝ) (B : Finset ℕ) (ν a : ℕ → ℝ) (G : Finset (EuclideanSpace ℝ (Fin 2) × ℕ)) (M : ℕ), (∀ x ∈ X, 0 ≤ μ x ∧ |x 0| ≤ 1 ∧ |x 1| ≤ 1) → ∑ x ∈ X, μ x = 1 → (∀ b ∈ B, 0 ≤ ν b ∧ |a b| ≤ 1) → ∑ b ∈ B, ν b = 1 → (∀ (z : EuclideanSpace ℝ (Fin 2)) (r : ℝ), ρ ≤ r → r ≤ 1 → ∑ x ∈ X.filter (fun x => dist x z ≤ r), μ x ≤ ρ ^ (-η) * r ^ d) → (∀ t r : ℝ, ρ ≤ r → r ≤ 1 → ∑ b ∈ B.filter (fun b => |a b - t| ≤ r), ν b ≤ ρ ^ (-η) * r ^ s) → ρ ^ η ≤ ∑ p ∈ G.filter (fun p => p.1 ∈ X ∧ p.2 ∈ B), μ p.1 * ν p.2 → (∀ b ∈ B, ∃ S : Finset ℝ, S.card ≤ M ∧ ∀ x ∈ X, (x, b) ∈ G → ∃ c ∈ S, |x 1 - a b * x 0 - c| ≤ ρ) → ρ ^ (-(min 1 (min d ((d + s) / 2))) + α) ≤ (M : ℝ)) → ∀ γ κ K τ D : ℝ, 0 < γ → γ < 1 → 0 < κ → 0 < τ → τ ≤ K → 1 ≤ D → ∃ e₀ : ℝ, 0 < e₀ ∧ ∀ e : ℝ, 0 < e → e < min e₀ 1 → ∀ t L : ℝ, τ ≤ t → t ≤ L → L ≤ K → ∀ n m : ℕ, ∀ (p : Fin n → Fin m → ℝ) (μ : Fin n → ℝ) (ν : Fin m → ℝ) (V A₀ : Fin n → ℂ) (b a c : Fin m → ℝ) (r z w : Fin m → ℂ) (h : ℝ), (∀ i j, 0 ≤ p i j) → (∑ i, ∑ j, p i j) = 1 → (∀ i, μ i = ∑ j, p i j) → (∀ j, ν j = ∑ i, p i j) → (∀ i, ‖V i‖ ≤ D ∧ ‖A₀ i‖ ≤ D) → (∀ j, 0 ≤ b j ∧ b j ≤ a j ∧ a j + t ≤ L ∧ c j ∈ Set.Icc (0 : ℝ) 1 ∧ ‖r j‖ = 1) → (∀ j k, c j ≠ c k → e ^ t ≤ |c j - c k|) → (∀ i j, 0 < p i j → |((V i - z j) * r j).re| ≤ e ^ b j ∧ |((V i - z j) * r j).im| ≤ e ^ a j ∧ |((A₀ i + c j • V i - w j) * r j).re| ≤ e ^ (b j + t) ∧ |((A₀ i + c j • V i - w j) * r j).im| ≤ e ^ (a j + t)) → (∀ B A : ℝ, ∀ R Z W : ℂ, 0 ≤ B → B ≤ A → A ≤ L → ‖R‖ = 1 → ∑ i ∈ Finset.univ.filter (fun i => |((V i - Z) * R).re| ≤ e ^ B ∧ |((V i - Z) * R).im| ≤ e ^ A ∧ |((A₀ i - W) * R).re| ≤ e ^ B ∧ |((A₀ i - W) * R).im| ≤ e ^ A), μ i ≤ e ^ ((1 + γ) * B + (1 - γ) * A - h)) → (∑ j, ν j * ((1 + γ) * b j + (1 - γ) * a j)) - (∑ i, ∑ j, p i j * (Real.log (p i j / (μ i * ν j)) + 2 * Real.log ((∑ k, if c k = c j then p i k else 0) / μ i))) / Real.log (1 / e) ≤ h + γ * t + κ

8. Level第 8 层 br3_positive_transport_of_projection

   The weighted planar projection estimate implies uniform finite positive-transport growth. For bounded exact lines A_i+cV_i, a finite compatible aperture law with distinct time representatives epsilon^t-separated, and any real h that bounds expected aperture weight minus particle information for every finite stochastic root-cap assignment, the target score Ew-I(T;G)/log(1/epsilon)+2H(C|T)/log(1/epsilon) is at most h+gamma*t+kappa. The threshold is uniform over all finite table sizes, laws, coordinates and apertures, for fixed gamma, kappa, bounded horizons, positive minimum duration and bounded domains. Complex coordinates represent the real plane; all information is expanded as finite real sums, including aggregation of repeated time labels.

   Frozen statement (Lean)冻结语句（Lean）

   (∀ d s α : ℝ, 0 < d → d ≤ 2 → 0 < s → s ≤ 1 → 0 < α → ∃ η ρ₁ : ℝ, 0 < η ∧ 0 < ρ₁ ∧ ∀ ρ : ℝ, 0 < ρ → ρ < ρ₁ → ∀ (X : Finset (EuclideanSpace ℝ (Fin 2))) (μ : EuclideanSpace ℝ (Fin 2) → ℝ) (B : Finset ℕ) (ν a : ℕ → ℝ) (G : Finset (EuclideanSpace ℝ (Fin 2) × ℕ)) (M : ℕ), (∀ x ∈ X, 0 ≤ μ x ∧ |x 0| ≤ 1 ∧ |x 1| ≤ 1) → ∑ x ∈ X, μ x = 1 → (∀ b ∈ B, 0 ≤ ν b ∧ |a b| ≤ 1) → ∑ b ∈ B, ν b = 1 → (∀ (z : EuclideanSpace ℝ (Fin 2)) (r : ℝ), ρ ≤ r → r ≤ 1 → ∑ x ∈ X.filter (fun x => dist x z ≤ r), μ x ≤ ρ ^ (-η) * r ^ d) → (∀ t r : ℝ, ρ ≤ r → r ≤ 1 → ∑ b ∈ B.filter (fun b => |a b - t| ≤ r), ν b ≤ ρ ^ (-η) * r ^ s) → ρ ^ η ≤ ∑ p ∈ G.filter (fun p => p.1 ∈ X ∧ p.2 ∈ B), μ p.1 * ν p.2 → (∀ b ∈ B, ∃ S : Finset ℝ, S.card ≤ M ∧ ∀ x ∈ X, (x, b) ∈ G → ∃ c ∈ S, |x 1 - a b * x 0 - c| ≤ ρ) → ρ ^ (-(min 1 (min d ((d + s) / 2))) + α) ≤ (M : ℝ)) → ∀ γ κ K τ D : ℝ, 0 < γ → γ < 1 → 0 < κ → 0 < τ → τ ≤ K → 1 ≤ D → ∃ e₀ : ℝ, 0 < e₀ ∧ ∀ e : ℝ, 0 < e → e < min e₀ 1 → ∀ t L : ℝ, τ ≤ t → t ≤ L → L ≤ K → ∀ n m : ℕ, ∀ (p : Fin n → Fin m → ℝ) (μ : Fin n → ℝ) (ν : Fin m → ℝ) (V A : Fin n → ℂ) (b a c : Fin m → ℝ) (r z w : Fin m → ℂ) (h : ℝ), (∀ i j, 0 ≤ p i j) → (∑ i, ∑ j, p i j) = 1 → (∀ i, μ i = ∑ j, p i j) → (∀ j, ν j = ∑ i, p i j) → (∀ i, ‖V i‖ ≤ D ∧ ‖A i‖ ≤ D) → (∀ j, 0 ≤ b j ∧ b j ≤ a j ∧ a j + t ≤ L ∧ c j ∈ Set.Icc (0 : ℝ) 1 ∧ ‖r j‖ = 1) → (∀ j k, c j ≠ c k → e ^ t ≤ |c j - c k|) → (∀ i j, 0 < p i j → |((V i - z j) * r j).re| ≤ e ^ b j ∧ |((V i - z j) * r j).im| ≤ e ^ a j ∧ |((A i + c j • V i - w j) * r j).re| ≤ e ^ (b j + t) ∧ |((A i + c j • V i - w j) * r j).im| ≤ e ^ (a j + t)) → (∀ k : ℕ, ∀ (q : Fin n → Fin k → ℝ) (b a : Fin k → ℝ) (r z w : Fin k → ℂ), (∀ i j, 0 ≤ q i j) → (∀ i, ∑ j, q i j = μ i) → (∀ j, 0 ≤ b j ∧ b j ≤ a j ∧ a j ≤ L ∧ ‖r j‖ = 1) → (∀ i j, 0 < q i j → |((V i - z j) * r j).re| ≤ e ^ b j ∧ |((V i - z j) * r j).im| ≤ e ^ a j ∧ |((A i - w j) * r j).re| ≤ e ^ b j ∧ |((A i - w j) * r j).im| ≤ e ^ a j) → (∑ i, ∑ j, q i j * ((1 + γ) * b j + (1 - γ) * a j - Real.log (q i j / (μ i * ∑ l, q l j)) / Real.log (1 / e))) ≤ h) → (∑ j, ν j * ((1 + γ) * b j + (1 - γ) * a j)) - (∑ i, ∑ j, p i j * (Real.log (p i j / (μ i * ν j)) + 2 * Real.log ((∑ k, if c k = c j then p i k else 0) / μ i))) / Real.log (1 / e) ≤ h + γ * t + κ

9. Level第 9 层 br3_restricted_measurable_of_projection

   The weighted planar projection estimate implies the uniform restricted oscillatory L3 bound for jointly measurable phases in the frozen global definite Gevrey-3 class: for measurable F subset Kv and MemLp f 3 with norm f <= 1_F, the output norm is at most C lambda^(-1+nu) volume(F)^(1/3). This contains the positive-transport and wave-packet growth argument and the restricted part of Section 12.1, after smooth phase normalization.

   Frozen statement (Lean)冻结语句（Lean）

   (∀ d s α : ℝ, 0 < d → d ≤ 2 → 0 < s → s ≤ 1 → 0 < α → ∃ η ρ₁ : ℝ, 0 < η ∧ 0 < ρ₁ ∧ ∀ ρ : ℝ, 0 < ρ → ρ < ρ₁ → ∀ (X : Finset (EuclideanSpace ℝ (Fin 2))) (μ : EuclideanSpace ℝ (Fin 2) → ℝ) (B : Finset ℕ) (ν a : ℕ → ℝ) (G : Finset (EuclideanSpace ℝ (Fin 2) × ℕ)) (M : ℕ), (∀ x ∈ X, 0 ≤ μ x ∧ |x 0| ≤ 1 ∧ |x 1| ≤ 1) → ∑ x ∈ X, μ x = 1 → (∀ b ∈ B, 0 ≤ ν b ∧ |a b| ≤ 1) → ∑ b ∈ B, ν b = 1 → (∀ (z : EuclideanSpace ℝ (Fin 2)) (r : ℝ), ρ ≤ r → r ≤ 1 → ∑ x ∈ X.filter (fun x => dist x z ≤ r), μ x ≤ ρ ^ (-η) * r ^ d) → (∀ t r : ℝ, ρ ≤ r → r ≤ 1 → ∑ b ∈ B.filter (fun b => |a b - t| ≤ r), ν b ≤ ρ ^ (-η) * r ^ s) → ρ ^ η ≤ ∑ p ∈ G.filter (fun p => p.1 ∈ X ∧ p.2 ∈ B), μ p.1 * ν p.2 → (∀ b ∈ B, ∃ S : Finset ℝ, S.card ≤ M ∧ ∀ x ∈ X, (x, b) ∈ G → ∃ c ∈ S, |x 1 - a b * x 0 - c| ≤ ρ) → ρ ^ (-(min 1 (min d ((d + s) / 2))) + α) ≤ (M : ℝ)) → ∀ (Kv Kx : Set (EuclideanSpace ℝ (Fin 2))), Bornology.IsBounded Kv → Bornology.IsBounded Kx → ∀ (a₀ a₁ A : ℝ), 0 < a₀ → 1 ≤ A → ∀ Mb : ℕ → ℝ, ∀ ν : ℝ, 0 < ν → ∃ C : ℝ, ∀ lam : ℝ, 2 ≤ lam → ∀ σ : ℝ, (σ = 1 ∨ σ = -1) → ∀ (ζ : EuclideanSpace ℝ (Fin 2) → EuclideanSpace ℝ (Fin 2) → EuclideanSpace ℝ (Fin 2)) (Φ : ℝ → EuclideanSpace ℝ (Fin 2) → EuclideanSpace ℝ (Fin 2) → ℝ), Measurable (fun q : ℝ × EuclideanSpace ℝ (Fin 2) × EuclideanSpace ℝ (Fin 2) => Φ q.1 q.2.1 q.2.2) → ContDiff ℝ ((⊤ : ℕ∞) : WithTop ℕ∞) (fun q : EuclideanSpace ℝ (Fin 2) × EuclideanSpace ℝ (Fin 2) => ζ q.1 q.2) → (∀ (v p u w : EuclideanSpace ℝ (Fin 2)), inner ℝ (fderiv ℝ (ζ v) p u) w = inner ℝ u (fderiv ℝ (ζ v) p w)) → (∀ (v p u : EuclideanSpace ℝ (Fin 2)), a₀ * ‖u‖ ^ 2 ≤ σ * inner ℝ (fderiv ℝ (ζ v) p u) u ∧ σ * inner ℝ (fderiv ℝ (ζ v) p u) u ≤ a₁ * ‖u‖ ^ 2) → (∀ (j : ℕ) (q : EuclideanSpace ℝ (Fin 2) × EuclideanSpace ℝ (Fin 2)), ‖iteratedFDeriv ℝ j (fun r : EuclideanSpace ℝ (Fin 2) × EuclideanSpace ℝ (Fin 2) => fderiv ℝ (ζ r.1) r.2) q‖ ≤ A ^ (j + 1) * (Nat.factorial j : ℝ) ^ 3) → (∀ c ∈ Set.Icc (0 : ℝ) 1, ∀ (x v : EuclideanSpace ℝ (Fin 2)), HasGradientAt (Φ c x) (ζ v (x - c • v)) v) → ∀ B : ℝ × EuclideanSpace ℝ (Fin 2) × EuclideanSpace ℝ (Fin 2) → ℂ, ContDiff ℝ ((⊤ : ℕ∞) : WithTop ℕ∞) B → (∀ q : ℝ × EuclideanSpace ℝ (Fin 2) × EuclideanSpace ℝ (Fin 2), B q ≠ 0 → q.1 ∈ Set.Icc (0 : ℝ) 1 ∧ q.2.1 ∈ Kx ∧ q.2.2 ∈ Kv) → (∀ (k : ℕ) (q : ℝ × EuclideanSpace ℝ (Fin 2) × EuclideanSpace ℝ (Fin 2)), ‖iteratedFDeriv ℝ k B q‖ ≤ Mb k) → ∀ F : Set (EuclideanSpace ℝ (Fin 2)), MeasurableSet F → F ⊆ Kv → ∀ f : EuclideanSpace ℝ (Fin 2) → ℂ, MeasureTheory.MemLp f 3 MeasureTheory.volume → (∀ v, ‖f v‖ ≤ F.indicator (fun _ => (1 : ℝ)) v) → MeasureTheory.eLpNorm (fun q : ℝ × EuclideanSpace ℝ (Fin 2) => ∫ v, Complex.exp (Complex.I * ((lam * Φ q.1 q.2 v : ℝ) : ℂ)) * B (q.1, q.2, v) * f v) 3 MeasureTheory.volume ≤ ENNReal.ofReal (C * lam ^ (-1 + ν)) * MeasureTheory.volume F ^ ((1 : ℝ) / 3)

10. Level第 10 层 br3_measurable_oscillatory_of_ren_wang

    The canonical finite planar Ren–Wang estimate implies the oscillatory L³ estimate for jointly measurable real phases. Normalize Φ by subtracting Φ(c,x,0); the resulting smooth phase is governed by ζ, while the measurable offset contributes a measurable factor of modulus one.

    Frozen statement (Lean)冻结语句（Lean）

    (∀ s d α : ℝ, 0 < s → s ≤ 1 → 0 < d → d ≤ 2 → 0 < α → ∃ η₀ ρ₀ c : ℝ, 0 < η₀ ∧ 0 < ρ₀ ∧ 0 < c ∧ ∀ ρ : ℝ, 0 < ρ → ρ < ρ₀ → ∀ P : Finset (EuclideanSpace ℝ (Fin 2)), P.Nonempty → (∀ x ∈ P, |x 0| ≤ 1 ∧ |x 1| ≤ 1) → (∀ x ∈ P, ∀ y ∈ P, x ≠ y → ρ ≤ dist x y) → (∀ (z : EuclideanSpace ℝ (Fin 2)) (r : ℝ), ρ ≤ r → r ≤ 1 → ((P.filter (fun x => dist x z ≤ r)).card : ℝ) ≤ ρ ^ (-η₀) * r ^ d * P.card) → ∀ (M : ℝ) (T : EuclideanSpace ℝ (Fin 2) → Finset (EuclideanSpace ℝ (Fin 2))), (∀ x ∈ P, M ≤ ((T x).card : ℝ) ∧ ((T x).card : ℝ) ≤ 2 * M ∧ (∀ l ∈ T x, |l 0| ≤ 1 ∧ |l 1| ≤ 1) ∧ (∀ l ∈ T x, ∀ l' ∈ T x, l ≠ l' → ρ ≤ dist l l') ∧ (∀ (z : EuclideanSpace ℝ (Fin 2)) (r : ℝ), ρ ≤ r → r ≤ 1 → (((T x).filter (fun l => dist l z ≤ r)).card : ℝ) ≤ ρ ^ (-η₀) * r ^ s * (T x).card) ∧ (∀ l ∈ T x, |x 1 - l 0 * x 0 - l 1| ≤ ρ)) → c * ρ ^ (-(min 1 (min d ((d + s) / 2))) + α) * M ≤ ((P.biUnion T).card : ℝ)) → ∀ (Kv Kx : Set (EuclideanSpace ℝ (Fin 2))), Bornology.IsBounded Kv → Bornology.IsBounded Kx → ∀ (a₀ a₁ A : ℝ), 0 < a₀ → 1 ≤ A → ∀ Mb : ℕ → ℝ, ∀ ν : ℝ, 0 < ν → ∃ C : ℝ, ∀ lam : ℝ, 2 ≤ lam → ∀ σ : ℝ, (σ = 1 ∨ σ = -1) → ∀ (ζ : EuclideanSpace ℝ (Fin 2) → EuclideanSpace ℝ (Fin 2) → EuclideanSpace ℝ (Fin 2)) (Φ : ℝ → EuclideanSpace ℝ (Fin 2) → EuclideanSpace ℝ (Fin 2) → ℝ), Measurable (fun q : ℝ × EuclideanSpace ℝ (Fin 2) × EuclideanSpace ℝ (Fin 2) => Φ q.1 q.2.1 q.2.2) → ContDiff ℝ ((⊤ : ℕ∞) : WithTop ℕ∞) (fun q : EuclideanSpace ℝ (Fin 2) × EuclideanSpace ℝ (Fin 2) => ζ q.1 q.2) → (∀ (v p u w : EuclideanSpace ℝ (Fin 2)), inner ℝ (fderiv ℝ (ζ v) p u) w = inner ℝ u (fderiv ℝ (ζ v) p w)) → (∀ (v p u : EuclideanSpace ℝ (Fin 2)), a₀ * ‖u‖ ^ 2 ≤ σ * inner ℝ (fderiv ℝ (ζ v) p u) u ∧ σ * inner ℝ (fderiv ℝ (ζ v) p u) u ≤ a₁ * ‖u‖ ^ 2) → (∀ (j : ℕ) (q : EuclideanSpace ℝ (Fin 2) × EuclideanSpace ℝ (Fin 2)), ‖iteratedFDeriv ℝ j (fun r : EuclideanSpace ℝ (Fin 2) × EuclideanSpace ℝ (Fin 2) => fderiv ℝ (ζ r.1) r.2) q‖ ≤ A ^ (j + 1) * (Nat.factorial j : ℝ) ^ 3) → (∀ c ∈ Set.Icc (0 : ℝ) 1, ∀ (x v : EuclideanSpace ℝ (Fin 2)), HasGradientAt (Φ c x) (ζ v (x - c • v)) v) → ∀ B : ℝ × EuclideanSpace ℝ (Fin 2) × EuclideanSpace ℝ (Fin 2) → ℂ, ContDiff ℝ ((⊤ : ℕ∞) : WithTop ℕ∞) B → (∀ q : ℝ × EuclideanSpace ℝ (Fin 2) × EuclideanSpace ℝ (Fin 2), B q ≠ 0 → q.1 ∈ Set.Icc (0 : ℝ) 1 ∧ q.2.1 ∈ Kx ∧ q.2.2 ∈ Kv) → (∀ (k : ℕ) (q : ℝ × EuclideanSpace ℝ (Fin 2) × EuclideanSpace ℝ (Fin 2)), ‖iteratedFDeriv ℝ k B q‖ ≤ Mb k) → ∀ f : EuclideanSpace ℝ (Fin 2) → ℂ, MeasureTheory.MemLp f 3 MeasureTheory.volume → (∀ v, v ∉ Kv → f v = 0) → MeasureTheory.eLpNorm (fun q : ℝ × EuclideanSpace ℝ (Fin 2) => ∫ v, Complex.exp (Complex.I * ((lam * Φ q.1 q.2 v : ℝ) : ℂ)) * B (q.1, q.2, v) * f v) 3 MeasureTheory.volume ≤ ENNReal.ofReal (C * lam ^ (-1 + ν)) * MeasureTheory.eLpNorm f 3 MeasureTheory.volume

import ChallengeDeps

open MeasureTheory

/-- Theorem 1.1: for every `δ > 0` there is a finite constant `C_δ` with
`‖T_δ f‖_{L³(ℝ³)} ≤ C_δ ‖f‖_{L³(ℝ³)}` for all Schwartz functions `f`. (By interpolation and
duality this gives boundedness on `L^p(ℝ³)` for all `δ > max{3|1/p - 1/2| - 1/2, 0}`.) -/
theorem bochner_riesz_three (δ : ℝ) (hδ : 0 < δ) :
    ∃ C : ℝ, ∀ f : SchwartzMap (EuclideanSpace ℝ (Fin 3)) ℂ,
      eLpNorm (bochnerRiesz δ f) 3 volume ≤ ENNReal.ofReal C * eLpNorm (⇑f) 3 volume := by
  sorry

Other configurations measured其他实测配置

Conditions: each run alone on 8 whole physical cores (16 CPUs, both hyperthreads) and 64 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，含超线程）和 64 GiB 内存，运行期间独占锁定，其他进程用不了这些 CPU；断网，所有工具和库只读挂载；Lean leanprover/lean4:v4.35.0-rc3。原始流程是未经改动的官方检查器^[3,4]，每层运行一次；两条泳道都不计排队等待和层与层之间调度器的停顿。测于 2026-10-24。