PrincipalResponseComposeAssembly #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
Provider: the assembly of e.lower.bound.principal.one #
Target display, e.lower.bound.principal.one, in ABK26 (block):
avsum_{z in 3^n Zd cap cu_K} E[ P_z . bfA_m(z+cu_n) P_z ]
<= (1 + C E^2 |log cgamma|^2 cgamma)
avsum_z E[ G_{-(h)_{z+cu_n}} P_z . bfAhom_{m-h} G_{-(h)_{z+cu_n}} P_z ]
+ cgamma^6 .
The manuscript derives it in one sentence: "Combining the above two displays
with e.lower.bound.principal.one.pre leads to e.lower.bound.principal.one."
The three inputs of that sentence are
e.lower.bound.principal.one.pre, the good-event half, which readsavsum_z E[ P_z. bfA_m(z+cu_n) P_z 1_{Q_z} ] <= (1 + cgamma^6) avsum_z E[ G P_z. bfAhom_{m-h}(z+cu_n) G P_z ] + cgamma^6/2;e.use.also.for.the.upper.bound, the passage from the finite-cube annealed matrixbfAhom_{m-h}(cu_n)to the infinite-volumebfAhom_{m-h}, at the factor1 +^2 |log cgamma|^2 cgamma.
This module performs exactly that combination.
What is supplied and what is assumed #
- The indicator split
E[X] = E[X 1_{Q}] + E[X 1_{not Q}]at the grid (integral_indicator_split,descendantsAverage_add_real). The two integrability side conditions are its only cost. - The cube-to-limit step is not assumed. It is produced from the proved
leg (v):
annealedCubeBlockQuadratic_le_annealedLimitBlockQuadratic(e.use.also.for.the.upper.boundin Loewner form) integrated and grid-averaged indescendantsAverage_integral_annealedCubeBlockQuadratic_le, together withcubeAnnealedProbeDefect_le_logSq_budget, which is the manuscript's own budget att = |log cgamma|^{-1}. So the printed factorC E^2 |log cgamma|^2 cgammaappears here as the named quantityprincipalResponseSwitchBudget, withCthe provedprincipalResponseBudgetConstand the scale-gap factor3^{2K}visible. - The good-event half
hgoodis a named binder: it is the source displaye.lower.bound.principal.one.pre, whose proof combines thel.J.sensitivitygauge switch of sub-step (i), the ellipticity budget of sub-step (ii) and the independence step of sub-step (iii). It is a conclusion of the manuscript at a\labeled display, not a step of the combination performed here. - The bad-event half
hbadis likewise a named binder. Its analytic content is the bad-event leg at the grid average,PrincipalComplementEnergy.exists_const_descendantsAverage_integral_switchCubeEnergy_badEvent_le; bringing that estimate's exponential tail below the half-budget shape used here is the caller's step, not one performed in this module.
Other divergences #
- The scale gap is free. It enters only through the free real
KofcubeAnnealedProbeDefect_le_logSq_budget's own gate|log cgamma|^{-1}(L - n) <= K. The printed buffer16ofe.recurrence.paramsis not used and the localization depthjis free.
Binders #
Every theorem below is conditional except descendantsAverage_add_real, which
is an unconditional identity. None of them is a frozen declaration. What the
caller must supply, plainly:
integral_indicator_splitasks for integrability of the two halves;descendantsAverage_integral_annealedCubeBlockQuadratic_leasks for the unit normalizationhEvof the probe direction and integrability of the two quadratic forms;
hgood and hbad are \labeled displays of the manuscript, supplied
elsewhere; every step between them and the target display is performed here
rather than assumed.
Module boundary #
This module does not import or consume
Provider.BadEvents.BadEventLemmaUmbrella. The bad-event half enters only as
the abstract binder hbad, so the transitional umbrella consumption described
in PrincipalResponseComposeBadEvent is confined to that single file and does
not leak here.
References #
- ABK26,
l.approximate.recurrence.formula, Step 3;e.lower.bound.principal.one,e.lower.bound.principal.one.pre,e.use.also.for.the.upper.bound, the budget chain;e.good.local.events;e.cgamma.constraints;e.recurrence.params.
Grid arithmetic #
A uniform per-cube bound with a constant factor passes to the grid average.
: this statement holds only under the propositions supplied by its binders; it is a provider A, not a source-facing frozen declaration.
The grid average is additive.
Unconditional: no caller-supplied proposition enters.
The fold, with its excess pinned #
The combination, with the product left exact.
Splitting the energy over the good and bad events, applying the good-event
display at factor 1 + delta, the bad-event budget, and the cube-to-limit step
at factor 1 + kappa, one gets the target with the exact product (1 + delta)(1 + kappa). Nothing is absorbed: a formalization must name its
constants, and this statement names them.
: this statement holds only under the propositions supplied by its binders; it is a provider A, not a source-facing frozen declaration.
The rename, at the visible price C -> 3C. If the good-event excess
delta is below the cube-to-limit budget kappa and below 1, the exact
product collapses into a single factor with the constant tripled.
: this statement holds only under the propositions supplied by its binders; it is a provider A, not a source-facing frozen declaration.
The combination in the manuscript's printed shape, with the constant renamed rather than silently reused.
: this statement holds only under the propositions supplied by its binders; it is a provider A, not a source-facing frozen declaration.
The indicator split #
The good/bad split of the energy under the expectation, against.
: this statement holds only under the propositions supplied by its binders; it is a provider A, not a source-facing frozen declaration.
Leg (v) at the grid #
e.use.also.for.the.upper.bound integrated and grid-averaged. The proved
Loewner domination of the finite-cube annealed matrix by (1 + delta) times
the infinite-volume one, with delta the defect, passes through the
expectation and the grid average.
: this statement holds only under the propositions supplied by its binders; it is a provider A, not a source-facing frozen declaration.
The target display #
The printed switch budget^{2K} E^2 |log cgamma|^2 cgamma, with the proved absolute constant and the scale-gap factor both visible. This is the quantity the manuscript writes as^2 |log cgamma|^2 cgamma.
Equations
- One or more equations did not get rendered due to their size.
Instances For
e.lower.bound.principal.one, assembled.
At the field index L (the manuscript's m - h), the cube scale n, the
localization cube Q and depth j, for every energy observable energy and
every gauged doubled load W:
avsum_R E[ energy_R ]
<= (1 + 3 principalResponseSwitchBudget)
avsum_R E[ W_R . bfAhom_L W_R ]
+ cgamma^6 ,
given the good-event display e.lower.bound.principal.one.pre (hgood), the
bad-event budget (hbad), and the rename gate hrename. The passage from
bfAhom_L(cu_n) to bfAhom_L -- the manuscript's third input,
e.use.also.for.the.upper.bound -- is not assumed: it is produced from the
proved leg (v) and its budget.
The bad event is indexed by the grid cube, Ebad : TriadicCube d → Set Omega,
as the manuscript's own Q_z are: each cube of the depth-j grid carries its
own event, and the split below is performed cube by cube. Taking Ebad
constant recovers the single-event reading, so nothing is lost by the indexing.
hgood and hbad are named binders: they are the manuscript's own two
\labeled displays, and this theorem asserts nothing about their
satisfiability.
The statement therefore holds only under the propositions supplied by its binders; it is a conditional result, not a frozen declaration.