Direct N = 1 base for Suzuki Lemma 13.2 #
At κ = 1, β = 2, the first finite source layer is explicit. On its
legal odd-parity domain x > 1, its weighted value is 3 - x for x ≤ 3
and is zero for x ≥ 3. The Section-13 initial condition says that the
weighted positive hat layer is exactly one on 0 < x ≤ 3. Thus the fixed
constant 2 proves the whole N = 1 layer, including the zero-support tail.
theorem
MathlibNt.SieveTheory.lemma132_base_one_direct_two
{H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers}
(hH : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatSourceContract H)
(x : ℝ)
:
Pointwise fixed-witness form of the direct base case.
theorem
MathlibNt.SieveTheory.lemma132_base_one_direct
{H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers}
(hH : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatSourceContract H)
:
∃ (C : ℝ),
1 ≤ C ∧ ∀ x ∈ SuzukiFiniteContinuousLayers.KappaOneModel.parityDomain 2 1,
x * SuzukiFiniteContinuousLayers.finiteSourceLayer 1 2 1 x ≤ C * x ^ 2 * H.T (SwitchingPrinciple.SuzukiLemma144KappaOne.ErrorSign.ofDepth 1) x
Uniform direct base case for (13.13), with the compact constant C = 2.
The quantifier order is ∃ C, ∀ x; the constant does not depend on x or on
H.