ClosureFinal

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

The two-sided closure, reduced to its named endpoints

Closure.ClosureAssembly carries the node as far as conditional displays: two statements of the form "given the four junctions at the chosen corrector families, plus two typing binders and three parameter-regime facts, the printed display holds". This module removes everything from that list that is not a mathematical endpoint of the manuscript:

• the two AEStronglyMeasurable typing binders hDm, hNm are discharged by Closure.ClosureFinalMeasurability;
• the three parameter-regime facts hgamma, hcap, hsmall are derived from the contract's own antecedents by Closure.ClosureFinalArithmetic and Closure.shellDrift_le_cap, at an enlarged absolute constant;
• Junction 4 is discharged at the chosen families by Closure.eventually_principalSwitchEndpoint_closureFamilies;
• the induction state is moved from the contract's scale m0 - 1 to the producers' scale n + h - 1 by Closure.inductionState_mono;
• the degenerate shell h = 0 is discharged by Closure.recurrenceUpperDisplay_zero and Closure.recurrenceLowerDisplay_zero;
• the two displays' constants (closureConstant and max closureConstant (2 F)) are merged into one by Closure.recurrenceUpperDisplay_mono and Closure.recurrenceLowerDisplay_mono;
• the direction of the displays is chosen here (closureUnitVec), the printed lines being statements about shom ratios alone.

What is left is exactly three named endpoints, ClosureSplitInput, ClosureStep4Input and ClosureStep5Input below, each stated at the closure's own corrector families and in the shape its named producer delivers.

Each of the three carries, as its own leading antecedent, the manuscript's standing dimension hypothesis 2 <= d --- exactly the shape Closure.NodeContract.TwoSidedClosure itself has. twoSidedClosure_of_endpoints introduces hd before consuming any input.

The three inputs, and their status

input	content	producer
ClosureSplitInput	the finite-grid half of Steps 1--3 at the cgamma^10 endpoint, in the exact
antecedent shape of
Closure.AnnealedLimitJunction.annealedSplitEndpoint_of_integral_ch02CoarseBlockMatrix_le	IN,
lane gamma10-*
ClosureStep4Input	Junction 1, e.lower.bound.pre1 at the closure families
Closure.JunctionDischargeStepFour.step4GaugeEndpoint_of_correctors, whose four remaining binders
are analytic side conditions of the display
ClosureStep5Input	Junction 2, e.lower.bound.pre2 at the closure families, with the produced
Fend	Closure.JunctionDischargeStepFiveDisplay.step5GaugeEndpoint_of_correctors_gauge (per-cube
gauge), whose hosc binder is supplied by Closure.Step5DefectGauge's re-sited full-mesh producer

Nothing else is assumed. In particular no smallness, no normalization and no bound of the manuscript is carried as a hypothesis of twoSidedClosure_of_endpoints: the three inputs are the manuscript's own Step-1--3, Step-4 and Step-5 conclusions, and everything the assembly needs besides them is proved.

References

• ABK26, l.approximate.recurrence.formula.

A unit direction

Both printed lines of e.what.do.we.have are statements about the ratio shom_{n+h} shom_n^{-1} alone; the direction enters only through the junctions, which hold at every unit direction. The closure therefore chooses one.

def Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.closureUnitVec (d : ℕ) [NeZero d] : HCPolySupport.Vec d

The first coordinate direction, a unit vector of Vec d whenever d /= 0.

Equations

• Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.closureUnitVec d = Pi.single ⟨0, ⋯⟩ 1

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.vecNormSq_closureUnitVec (d : ℕ) [NeZero d] : HCPolySupport.vecNormSq (closureUnitVec d) = 1

The regime under which the three inputs are read

Each input is read exactly where the manuscript reads Steps 1--5: inside l.approximate.recurrence.formula's standing hypotheses. ClosureRegime records that antecedent block once, in the shape the proved principal-response producer Closure.eventually_principalSwitchEndpoint_closureFamilies already uses, so that an input is never asked for outside the regime in which the manuscript proves it.

def Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.ClosureRegime {d : ℕ} (C : ℝ) (M : ABKModel d) (n : ℤ) (h : ℕ) (Ec : { E : ℝ // 1 ≤ E }) : Prop

The manuscript's standing hypotheses at one admissible pair (n, n+h) and one threshold C.

Equations

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

The three inputs

def Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.ClosureSplitInput (d : ℕ) [NeZero d] : Prop

Input 1 (Steps 1--3, the cgamma^10 endpoint).

The finite-grid half of e.lower.bound.basic.split together with e.lower.bound.localization.terms, stated verbatim in the antecedent shape of Closure.AnnealedLimitJunction.annealedSplitEndpoint_of_integral_ch02CoarseBlockMatrix_le and at the closure's own corrector families, for all sufficiently large localization cubes. Both gauge branches are required: the upper display reads it at (e, e') = (0, e), the lower display at (e, 0). The producer names its own threshold Csplit, exactly as the proved principal-response terminal does.

Equations

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

def Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.ClosureStep4Input (d : ℕ) [NeZero d] : Prop

Input 2 (Step 4). Closure.Step4GaugeEndpoint at the closure's own corrector families, in the manuscript's regime, for all sufficiently large localization cubes.

Equations

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

def Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.ClosureStep5Input (d : ℕ) [NeZero d] : Prop

Input 3 (Step 5). Closure.Step5GaugeEndpoint at the closure's own corrector families, in the manuscript's regime, with the produced constant Fend uniform in the model, for all sufficiently large localization cubes.

Equations

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

Junction 3 at the closure families, from the finite-grid input

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.eventually_annealedSplitEndpoint_of_splitInput {d : ℕ} [NeZero d] {Csplit : ℝ} (hsplit : ∀ (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, ∫ (omega : Cutoff.CutoffSample d), HCPolySupport.blockVecDot (recurrenceP (Annealed.sigmaBar M n) 0 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) 0 e)) ∂↑(Cutoff.cutoffSampleLaw M) ≤ principalEnergyAverage M n h (↑K) (closureMeshDepth M n h K) 0 e (alongIncrementPath n h (closureDirichletFamily (↑(Annealed.sigmaBar M n))⁻¹ 0 K)) (alongIncrementPath n h (closureNeumannFamily (↑(Annealed.sigmaBar M n))⁻¹ e K)) + M.gamma ^ 10) ∧ ∀ᶠ (K : ℕ) in Filter.atTop, ∫ (omega : Cutoff.CutoffSample d), HCPolySupport.blockVecDot (recurrenceP (Annealed.sigmaBar M n) e 0) (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 0)) ∂↑(Cutoff.cutoffSampleLaw M) ≤ principalEnergyAverage M n h (↑K) (closureMeshDepth M n h K) e 0 (alongIncrementPath n h (closureDirichletFamily (↑(Annealed.sigmaBar M n))⁻¹ e K)) (alongIncrementPath n h (closureNeumannFamily (↑(Annealed.sigmaBar M n))⁻¹ 0 K)) + M.gamma ^ 10) (M : ABKModel d) (n : ℤ) (h : ℕ) (Ec : { E : ℝ // 1 ≤ E }) {e : HCPolySupport.Vec d} (he : HCPolySupport.vecNormSq e = 1) (hreg : ClosureRegime Csplit M n h Ec) : (∀ᶠ (K : ℕ) in Filter.atTop, AnnealedSplitEndpoint M n h (↑K) (closureMeshDepth M n h K) 0 e (alongIncrementPath n h (closureDirichletFamily (↑(Annealed.sigmaBar M n))⁻¹ 0 K)) (alongIncrementPath n h (closureNeumannFamily (↑(Annealed.sigmaBar M n))⁻¹ e K))) ∧ ∀ᶠ (K : ℕ) in Filter.atTop, AnnealedSplitEndpoint M n h (↑K) (closureMeshDepth M n h K) e 0 (alongIncrementPath n h (closureDirichletFamily (↑(Annealed.sigmaBar M n))⁻¹ e K)) (alongIncrementPath n h (closureNeumannFamily (↑(Annealed.sigmaBar M n))⁻¹ 0 K))

The contract

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.twoSidedClosure_of_endpoints (d : ℕ) [NeZero d] (hsplit : ClosureSplitInput d) (hstep4 : ClosureStep4Input d) (hstep5 : ClosureStep5Input d) : TwoSidedClosure d

The two-sided closure of l.approximate.recurrence.formula, from its three named endpoints.

Everything the assembly needs besides the three inputs is proved: the two AEStronglyMeasurable typing binders, the three parameter-regime facts, Junction 4, the induction-state transport, the degenerate shell h = 0 and the merge of the two displays' constants.

The switch endpoint enters through Closure.eventually_principalSwitchEndpoint_closureFamilies.