Uniform finite-layer / hat-layer bridge for Σ₁₁

At κ = κ̂ = 1, Suzuki's (9.6) is finiteSourceLayer 1 2 M x. The finite statement (13.13) in the proof of Lemma 13.2 is

x * T_M(x) ≤ C * x^2 * T̂^(parity M)(x)

with one C = C(κ) for every depth M ≥ 1 and every x ∈ I_M. The proposition below freezes exactly that still-missing source edge. In particular, it does not manufacture a coefficient by dividing one target value by another.

def MathlibNt.SieveTheory.Section13FiniteLayerHatUniform (H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers) : Prop

Exact κ = 1, β = 2 specialization of Suzuki (13.13). The single constant is outside both the depth and coordinate quantifiers.

Equations

• MathlibNt.SieveTheory.Section13FiniteLayerHatUniform H = ∃ (C : ℝ), 1 ≤ C ∧ ∀ (M : ℕ) (x : ℝ), 1 ≤ M → x ∈ MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.KappaOneModel.parityDomain 2 M → x * MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.finiteSourceLayer 1 2 M x ≤ C * x ^ 2 * H.T (MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.ErrorSign.ofDepth M) x

theorem MathlibNt.SieveTheory.finiteSourceLayer_le_uniform_mul_hat {H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers} (hbridge : Section13FiniteLayerHatUniform H) : ∃ (C : ℝ), 1 ≤ C ∧ ∀ (M : ℕ) (x : ℝ), 1 ≤ M → 0 < x → x ∈ SuzukiFiniteContinuousLayers.KappaOneModel.parityDomain 2 M → SuzukiFiniteContinuousLayers.finiteSourceLayer 1 2 M x ≤ C * (x * H.T (SwitchingPrinciple.SuzukiLemma144KappaOne.ErrorSign.ofDepth M) x)

Cancellation of the positive source coordinate converts source (13.13) into the unweighted form consumed by the Σ₁₁ endpoint. The same C remains uniform in M and x.

theorem MathlibNt.SieveTheory.finiteSourceLayer_pred_le_uniform_oppositeHat {H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers} (hbridge : Section13FiniteLayerHatUniform H) : ∃ (C : ℝ), 1 ≤ C ∧ ∀ (N : ℕ) (s : ℝ), 2 ≤ N → 2 ≤ s → s - 1 ∈ SuzukiFiniteContinuousLayers.KappaOneModel.parityDomain 2 (N - 1) → SuzukiFiniteContinuousLayers.finiteSourceLayer 1 2 (N - 1) (s - 1) ≤ C * ((s - 1) * H.T (SwitchingPrinciple.SuzukiLemma144KappaOne.ErrorSign.ofDepth N).opposite (s - 1))

The literal predecessor/sign form required in Case I: depth N-1 has the sign opposite to depth N. One constant works simultaneously for every N ≥ 2 and every legal moving coordinate s.

theorem MathlibNt.SieveTheory.finiteSourceLayer_pred_le_uniform_oppositeHat_on_window {H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers} (hbridge : Section13FiniteLayerHatUniform H) : ∃ (C : ℝ), 1 ≤ C ∧ ∀ (N : ℕ) (s σ : ℝ), 2 ≤ N → 2 ≤ s → s ≤ σ → s - 1 ∈ SuzukiFiniteContinuousLayers.KappaOneModel.parityDomain 2 (N - 1) → SuzukiFiniteContinuousLayers.finiteSourceLayer 1 2 (N - 1) (s - 1) ≤ C * ((s - 1) * H.T (SwitchingPrinciple.SuzukiLemma144KappaOne.ErrorSign.ofDepth N).opposite (s - 1))

Explicit moving-window packaging. The bound does not acquire a new coefficient when s or the outer endpoint σ moves.