SplitProducerFold

Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.

ClosureSplitInput reduced to three named residual obligations

ABK26, l.approximate.recurrence.formula, Steps 1--3, e.lower.bound.basic.split, e.lower.bound.localization.terms.

What this module does

Closure.ClosureFinal.ClosureSplitInput is the finite-grid half of Steps 1--3 at the cgamma^10 endpoint, read at the closure's own corrector families. The proved structural endpoint integral_blockVecDot_recurrenceP_le_principalSwitchEnergyAverage_add already delivers

  E[ P . bfA_{n+h}(cu_K) P ]  <=  principalSwitchEnergyAverage + fluctuationEnergyAverage ,

and principalSwitchEnergyAverage is definitionally the closure's own Closure.principalEnergyAverage (checked: the rfl below). This module performs the whole remaining assembly --- the eventual large-cube gate, the eventual depth-naming identity, the weak-solution properties of the closure families, the hintLHS producer, and both direction pairs --- and isolates exactly what is not proved anywhere in the repository as of writing:

SplitScaleObligations, three propositions at one localization scale and one direction pair.

obligation	content	status
(1)	per-cell sample integrability of the switch energy at P_z	produced (see the audit
correction below):
exists_const_eventually_integrable_switchCubeEnergy_closureFamilies;
its measurability half is Closure.SplitProducerLoad.measurable_principalPz_cutoffSample
(2)	per-cell sample integrability of the background energy mu(a_omega; P_z + bfF_z)
produced (see the audit correction below):
Closure.SplitObligationsBackground.integrable_doubledMuValue_meshCellBackground_of_cellMoments,
fed by the cell moments of Closure.SplitFoldCellMoments; its measurability half is
LocalizationFluctuationBackgroundClass.measurable_doubledMuValue_meshCellBackground
(3)	fluctuationEnergyAverage <= cgamma^10	open: Step 2 itself

Both are obsolete: the two dominations have since proved, and the two obligations are now produced unconditionally at the closure's own families and inside the closure's own regime by Closure.SplitObligationsRegime and Closure.SplitObligationsBackground, assembled in Closure.SplitObligations.splitScaleObligations_integrability_of_regime and (with the cell moments discharged) in Closure.SplitFoldIntegrability.splitScaleObligations_integrability_closureFamilies. Closure.SplitFoldIntegrability.closureSplitInput_of_gammaTenBound consumes exactly that, leaving conjunct (3) --- Step 2 --- as the sole residual obligation of Closure.ClosureFinal.ClosureSplitInput. Nothing in this file changed; only the status column was stale.

Everything else the split input needs is discharged below. In particular the two typing binders hpot, hflux and the whole hcomp front are supplied by LocalizationFluctuationBackgroundClass, so no measurability proposition survives in SplitScaleObligations.

Scope

There is no sorry, no admit, no custom axiom and no set_option maxHeartbeats.

References

• ABK26, l.approximate.recurrence.formula, e.lower.bound.basic.split, Step 2, e.lower.bound.localization.terms, e.recurrence.params.

The closure's corrector families, named

noncomputable def Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.closureDirichletAlong {d : ℕ} [NeZero d] (M : ABKModel d) (n : ℤ) (h K : ℕ) (e : HCPolySupport.Vec d) : Cutoff.ShellSeq d → HCPolySupport.H10Function (HCPolySupport.openCubeSet (HCPolySupport.originCube d ↑K))

The Dirichlet corrector of e.def.w the closure reads at direction e, on cu_K, along the increment path. A name for the term ClosureSplitInput prints.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.closureNeumannAlong {d : ℕ} (M : ABKModel d) (n : ℤ) (h K : ℕ) (e' : HCPolySupport.Vec d) : Cutoff.ShellSeq d → HCPolySupport.H1MeanZeroFunction (HCPolySupport.openCubeSet (HCPolySupport.originCube d ↑K))

The mean-zero Neumann mirror.

Equations

• One or more equations did not get rendered due to their size.

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.isZeroTraceDirichletRhsWeakSolution_closureDirichletAlong {d : ℕ} [NeZero d] (M : ABKModel d) (n : ℤ) (h K : ℕ) (e : HCPolySupport.Vec d) (omega : Cutoff.ShellSeq d) : HCPolySupport.IsZeroTraceDirichletRhsWeakSolution (fun (x : HCPolySupport.Vec d) => 1) (HCPolySupport.openCubeSet (HCPolySupport.originCube d ↑K)) (closureDirichletAlong M n h K e omega) fun (x : HCPolySupport.Vec d) => -Corrector.streamForcing (↑(Annealed.sigmaBar M n))⁻¹ omega n (n + ↑h) e x

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.isMeanZeroNeumannRhsWeakSolution_closureNeumannAlong {d : ℕ} (M : ABKModel d) (n : ℤ) (h K : ℕ) (e' : HCPolySupport.Vec d) (omega : Cutoff.ShellSeq d) : HCPolySupport.IsMeanZeroNeumannRhsWeakSolution (fun (x : HCPolySupport.Vec d) => 1) (HCPolySupport.openCubeSet (HCPolySupport.originCube d ↑K)) (closureNeumannAlong M n h K e' omega) fun (x : HCPolySupport.Vec d) => -Corrector.streamForcing (↑(Annealed.sigmaBar M n))⁻¹ omega n (n + ↑h) e' x

The residual obligations

def Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.SplitScaleObligations {d : ℕ} [NeZero d] (M : ABKModel d) (n : ℤ) (h K : ℕ) (e e' : HCPolySupport.Vec d) : Prop

The three residual obligations of the finite-grid half of Steps 1--3, at one localization scale K and one direction pair.

Two integrability statements in the sample, per mesoscopic cell, and the Step-2 estimate itself. No measurability proposition occurs: the measurability halves of the first two are proved (Closure.SplitProducerLoad.measurable_principalPz_cutoffSample and LocalizationFluctuationBackgroundClass.measurable_doubledMuValue_meshCellBackground), and the whole hcomp front is proved as well.

Equations

• One or more equations did not get rendered due to their size.

The reduction at one direction pair

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.eventually_integral_le_principalEnergyAverage_add {d : ℕ} [NeZero d] (M : ABKModel d) (n : ℤ) (h : ℕ) (e e' : HCPolySupport.Vec d) (hobl : ∀ᶠ (K : ℕ) in Filter.atTop, SplitScaleObligations M n h K e e') : ∀ᶠ (K : ℕ) in Filter.atTop, ∫ (omega : Cutoff.CutoffSample d), HCPolySupport.blockVecDot (recurrenceP (Annealed.sigmaBar M n) e e') (HCPolySupport.blockMatVecMul (HCPolySupport.Book.Ch02.coarseBlockMatrix (HCPolySupport.Book.Ch02.cubeDomain (HCPolySupport.originCube d ↑K)) ((Cutoff.coefficientCutoffTriadicCoeffFamily M (n + ↑h) omega).coeffOn (HCPolySupport.originCube d ↑K))) (recurrenceP (Annealed.sigmaBar M n) e e')) ∂↑(Cutoff.cutoffSampleLaw M) ≤ principalEnergyAverage M n h (↑K) (closureMeshDepth M n h K) e e' (alongIncrementPath n h (closureDirichletFamily (↑(Annealed.sigmaBar M n))⁻¹ e K)) (alongIncrementPath n h (closureNeumannFamily (↑(Annealed.sigmaBar M n))⁻¹ e' K)) + M.gamma ^ 10

The Step-1--3 display at one direction pair, from the three residual obligations.

exactly on SplitScaleObligations holding for all sufficiently large localization cubes. Everything else --- the large-cube gate, the depth-naming identity, the weak-solution properties of the closure families, the unconditional hintLHS producer, the typing binders and the whole hcomp measurability front --- is discharged here.

The split input

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.closureSplitInput_of_obligations (d : ℕ) [NeZero d] {Csplit : ℝ} (hCsplit : 0 < Csplit) (hobl : ∀ (M : ABKModel d) (n : ℤ) (h : ℕ) (Ec : { E : ℝ // 1 ≤ E }) (e : HCPolySupport.Vec d), HCPolySupport.vecNormSq e = 1 → ClosureRegime Csplit M n h Ec → (∀ᶠ (K : ℕ) in Filter.atTop, SplitScaleObligations M n h K 0 e) ∧ ∀ᶠ (K : ℕ) in Filter.atTop, SplitScaleObligations M n h K e 0) : ClosureSplitInput d

Closure.ClosureSplitInput from the residual obligations at both gauge branches.

on hobl; nothing else is assumed. This module does not prove ClosureSplitInput.