StepSevenLambdaSlots #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
t.regularity Step 7b: the derived-slot table #
The target #
The derived-slot table: from clause (A) (StepSevenLambdaStability.lean) and
clause (B) (StepSevenLambdaGoodEvent.lean) alone, every §4.4 λ/Λ slot follows
by index monotonicity and λ ≤ Λ. The four slots, all on the inner cube
□_{k-1} (the Step-7a sandwich's y' + □_{k'-1} in the lattice-aligned
reading) against the outer □_k (z + □_{k'}), are:
| # | slot | consumer | constant proved here |
|---|---|---|---|
| 1 | λ_{1/8,2}^{-1}(□_{k-1}) ≤ Clam σ^{-1} | 's hlambda | Clam = (32/7)·CB |
| 2 | λ_{1/8,1}(□_{k-1}) ≤ Clam σ | 's Cacc. L² leg | (256/63)·CB |
| 3 | λ_{1/8,1}^{-1}(□_{k-1}) ≤ C σ^{-1} | 's Cacc. data leg | (64/7)·CB |
| 4 | Θ_{1/4,1/8}(□_{k-1}) ≤ C | the Theta0 cap | (16384/441)·² |
(row 1's consumer is stepSevenCgLamInv; row 4's is the Theta0 binder of
StepSevenCaccMatching.stepSevenCaccPrefactor_le.)
Row 4 is the one that matters structurally: the comparators cancel. The
Λ leg carries σ and the λ^{-1} leg carries σ^{-1}, so their product
is σ·σ^{-1} = 1 and Θ_{1/4,1/8} is a pure dimensional constant. That cancellation is
machine-verified below (stepSevenThetaRatio_le_of_caps), not asserted.
The prefactor arithmetic (all three values machine-checked) #
At s* = 1/16 and C = 2 the printed prefactor C(1-2s*)^{-1}(t/(t-s*))^{2/q}
has coefficient 2/(1-1/8) = 16/7 and takes the values
t = 1/8, q = 2 : (16/7)·(2)^1 = 32/7 (row 1)
t = 1/4, q = 1 : (16/7)·(4/3)^2 = 256/63 (rows 2 and 4's Λ leg)
t = 1/8, q = 1 : (16/7)·(2)^2 = 64/7 (rows 3 and 4's λ leg)
and row 4's constant is (256/63)·(64/7)·² = (16384/441)·².
References #
- ABK26,
e.lambda.stability.applied.
2. The three prefactor values #
The printed prefactor at (t, q) = (1/8, 2) — row 1's constant.
The printed prefactor at (t, q) = (1/4, 1) — the Λ leg of rows 2 and 4.
The printed prefactor at (t, q) = (1/8, 1) — the λ leg of rows 3 and 4.
3. The naming trap: stepSevenCgLamInv IS the inverse #
stepSevenCgLamInv Q a s = λ_{s/2,2}^{-1}(Q; a), with the rpow (-1) of
the definition read as an honest inverse.
4. The index inequalities of the table #
Row 1 of the derived-slot table. From clause (A) at (t,q) = (1/8,2)
and clause (B),
λ_{1/8,2}^{-1}(□_{k-1}; a) ≤ (32/7)·CB · σ^{-1} ,
which is the hlambda slot at Clam := (32/7)·CB and shomMp := σ^{-1}.
6. Rows 2 and 3: the Caccioppoli slots #
The Λ leg at (t,q) = (1/4,1): Λ_{1/4,1}(□_{k-1}; a) ≤ (256/63)··σ.
Row 2 of the derived-slot table. λ ≤ Λ at the two indices then gives
λ_{1/8,1}(□_{k-1}; a) ≤ (256/63)·CB · σ .
Row 3 of the derived-slot table. From clause (A) at (t,q) = (1/8,1)
and clause (B),
λ_{1/8,1}^{-1}(□_{k-1}; a) ≤ (64/7)·CB · σ^{-1} .
7. Row 4: the Θ cap, and the cancellation of the comparators #
Row 4 of the derived-slot table — the Θ cap is a pure dimensional
constant.
Θ_{1/4,1/8}(□_{k-1}; a) ≤ (16384/441)·CB² .
The σ of the Λ leg and the σ^{-1} of the λ leg cancel; the
cancellation is performed explicitly below. This is the Theta0 of
stepSevenCaccPrefactor_le.