PrincipalResponseGoodEnergy #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
The principal good-event energy display, consumer-closed up to the Ccg gate #
Conditional Provider module: the direct successor of
PrincipalResponseBudgetWire.exists_smallCoupling_principalEnergy_bound_of_centering,
with thirteen previously caller-supplied inputs internalized (n, highScale,
hle, wD, wN, hwD, hwN, hmeasR, hintR, hgoodInt, hcubeInt,
hindep, hbudget). The correctors are produced existentially on the
conclusion side together with their e.def.w (label) weak-solution properties
-- never assumed. The scales are instantiated at `n = ((originCube d K).scale)
- j
andhighScale = m`; no uniqueness is claimed for that scale bridge.
The complement leg's per-cube integrability -- the integrability of
switchCubeEnergy against the complement indicator of the per-cube bad event --
is produced on the conclusion side too, at the very correctors and event
constant the inequality is stated at. It is an internal consequence of the
almost-sure good-event domination used to prove the display, not a new
hypothesis, and a direct consumer needs it to recombine the two legs.
The ONE non-standing conditional gate is hccg : 2 * d ^ 6 ≤ Ccg * sensitivityConstMax d ^ 2, quantified over the event constant Ccg. The
planned internal discharge (same-constant route, supervisor-ruled) selects a
floor-normalized coarse-ellipticity constant Cbase ≥ d ^ 6 B the bad-event
application and consumes the bad-event companion at event constant 2 * Cbase,
matching how the frozen bad_event_estimate on current main states its event
at twice its coarse constant. No event monotonicity is used or assumed
anywhere.
Besides the display endpoint
exists_smallCoupling_principalEnergy_bound_of_gate,
the fourth-order load integrability
exists_gamma0_integrable_switchEllipLoad_principalPz_sq and the energy's
sample measurability aestronglyMeasurable_switchCubeEnergy are exposed,
because the same-witness recombination in PrincipalResponseTerminal has to
rebuild the bad-event half's well-definedness binders at the very correctors
this module produces. Everything else below is private.
Frozen.Section3.stream_increment_lp_large_cube_bound is reached too but is
proved here, so it contributes nothing either.
aestronglyMeasurable_switchCubeEnergy reaches neither. All internal helpers
below are otherwise sorry-free, and none of the five forbidden circular anchors
is reached.
The measurable-proxy integrability device #
Measurability of the ellipticity load in the sample #
The L^8 membership of the two corrector gradients #
The fourth-order integrability of the ellipticity load #
The integrability of the conjugated quadratic form #
Sample measurability of the coarse matrix and of the good-event energy #
The shell-a.e. per-cube switch estimate is supplied by PrincipalResponseLamWire.