GammaTenDepthOscillation #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
e.lower.bound.oscillations at every depth below the recurrence mesh #
ABK26, e.lower.bound.oscillations, e.nablaw.oscillations,
e.recurrence.params.
What this module adds #
LocalizationOscillationEndpointSixteen reads the interior-mesh endpoint of
e.lower.bound.oscillations at the one mesh scale
nmesh = recurrenceMesoScale a cgamma m h of e.recurrence.params. The Besov
tower of Step 2 needs it at every scale nmesh - i, i : ℕ, with a
geometric gain in i; that is what
Closure.GammaTenEnvelopeInputGrid.exists_besovEnvelope_of_grid_depth_oscillation
consumes as its per-depth input D i.
The route is a re-instantiation, at no new analytic cost: the free-buffer
display
LocalizationOscillationDisplay.exists_freshShell*_gradient_oscillation_lower_bound_display
is run at inner scale nmesh - i and buffer N_i = Ngap + i, so that the outer
scale n + N = m - h --- the corrector's own fresh-shell scale --- does not
move. Consequently
- the coarse-energy envelope
LocalizationEnvelopeWire.exists_freshShell_gridFourthMoment_mesoWindowEnergy_le_wiredapplies at(n, N) = (nmesh - i, Ngap + i)with its buffer-independent right-hand side3^d freshShellFourthEnergyConst Chead (cgamma^{100}), so the amplitudeWis one constant for all depths; - the cell integrability
exists_gamma0_integrable_freshShell*_meshEnergyCell_rpow_fourapplies verbatim, its containment hypothesis being supplied on the finer grid byopenCubeAtScale_subset_openCubeSet_of_mem_interiorMesoCubeGrid; - the two
cgamma-facing gaugesS * P <= shellNormalizationConstandCtot cgamma^{15} <= 1are untouched, sincen + Nis unchanged.
The one new piece of arithmetic, and the polynomial factor it leaves #
Only the display's first factor moves with the depth: 3^{-N} becomes
3^{-(Ngap + i)} = 3^{-Ngap} 3^{-i}, and the middle term's linear factor N
becomes Ngap + i. The proved collapse
LocalizationOscillationEndpointSixteen.three_term_budget_le_sixteen absorbs
the linear factor through Ngap cgamma <= 96; at depth i the same step needs
(Ngap + i) 3^{-(Ngap+i)}, and the sharp elementary bound is Ngap + i <= Ngap (1 + i), i.e.
(Ngap + i) 3^{-(Ngap+i)} <= 96 cgamma^{31} * ((1 + i) 3^{-i}) .
The conclusion therefore carries the decay factor (1 + i) 3^{-i}, not the
bare 3^{-i}: the linear factor is genuinely there and is not silently dropped.
It is harmless downstream --- at the fourth power the depth input is
cgamma^{64} (1+i)^4 3^{-4i} <= 25 cgamma^{64} 36^{-i}, and 36^{-1} is the
exact ratio gate of
Closure.GammaTenEnvelopeInputGrid.sum_two_pow_mul_rpow_pow_four_geometric_le
at the closure's exponent gammaTenBesovExponent = 1/2 --- but it is recorded
in the statement.
What is proved #
three_term_budget_le_sixteen_decay--- the three-term collapse ofLocalizationOscillationEndpointSixteen.three_term_budget_le_sixteencarrying an arbitrary nonnegative decay factordeltathrough both the first factorGand the productNr * G.rpow_three_neg_add_split,depth_natCast_add_le,depth_geometric_le,depth_linear_geometric_le--- the depth arithmetic, isolated so that the two endpoints below stay inside the default heartbeat budget.exists_gamma0_freshShellDirichlet_meshOscillationDepth_le_gamma_pow_sixteenand its Neumann mirror --- the depth-indexed interior endpoints: statement, binders and threshold are those of the proved..._meshOscillation_le_gamma_pow_sixteenpair, with the mesh scale relaxed tonmesh - iand the conclusion multiplied by(1 + i) 3^{-i}. Ati = 0they are the proved statements.
Binders #
Verbatim those of LocalizationOscillationEndpointSixteen: hd, the model gate
M.gamma <= gamma0, the induction state, the four source gates 0 < h,
m - h <= m0, h <= 6 cstar gamma^{-1}, 10^10 gamma^{-1} <= K - m, the two
direction bounds, the base point z0, and the corrector family with the weak
formulation of e.def.w. The depth i : ℕ is universally quantified after the
corrector, so one threshold serves every depth. No sample-space binder and
no smallness gate beyond the produced threshold occurs.
Declared divergence: the carrier is the interior mesh #
The statements are on interiorMesoCubeGrid d K (nmesh - i) (m - h - 1), the
carrier. The transfer to the full mesh performed by
LocalizationOscillationFullMesh for the single scale nmesh does not
survive the depth index: the remainder of
LocalizationFluctuationGammaFold.gridFourthMoment_mesoCubeGrid_le_interior_add_of_eighthMoment
is sqrt (d 3^g / 3^p) sqrt E with K = n + p and outer + 1 = n + g, i.e.
3^{g-p} = 3^{(outer+1) - K} = 3^{(m-h) - K}, which does not move with the
mesh scale n. The boundary strip is the same fixed fraction at every depth,
so no 3^{-i} is available for it. This is recorded, not closed, here.
Scope #
There is no sorry, no admit, no custom axiom and no set_option maxHeartbeats.
References #
- ABK26,
e.lower.bound.oscillations,e.nablaw.oscillations,e.recurrence.params,e.def.w.
The three-term collapse, with a depth decay factor #
The two depth arithmetic facts #
The four gradient-integrability facts used by both corrector estimates.
A uniform depth budget for any gradient satisfying the cell and envelope estimates. The boundary condition enters only through the three supplied lower-level estimates.
The shared depth budget for the Dirichlet corrector.
The shared depth budget for the Neumann corrector.