ClosureAssembly #

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

The closure assembly: the two displays at one explicit pair of correctors #

Closure.Junctions names the four junctions of the closure node and proves two private assembly skeletons from them. This module carries the assembly as far as the proved producers allow: it chooses the corrector families, discharges Junction 4 at them for every large localization cube, reduces the drift limit to two typing binders, and states the two printed displays conditionally on what is genuinely still in flight.

Two shape deltas against `Closure.Junctions`' skeletons, and what replaces #

them

The skeletons upperDisplay_of_junctions / lowerDisplay_of_junctions of Closure.Junctions cannot be used here, for two independent reasons.

They are private. A private declaration is visible only inside its own module, so no other file can instantiate them. They are therefore re-proved here, from the public Closure.StepSixClosure.upperDisplay_of_annealedBlockBound and ..._lowerDisplay_of_annealedBlockBound, with the same proof.
Their quantification over the localization cube does not match the producers. The skeletons consume the junctions as
```
  {j : ℕ}   and   (hswitch : ∀ K : ℕ, PrincipalSwitchEndpoint M n h (K : ℤ) j ...)
```
i.e. at one fixed descendant depth j and at every cube scale K. Both producers of hswitch and hsplit --- the proved principal-response terminal exists_const_descendantsAverage_integral_principalEnergy_le_annealedLimit and the proved structural split LocalizationRecurrenceMesh.exists_localizationRecurrenceMeshSplit_le_descendantsAverage_expanded --- carry the depth-naming identity
```
  ((originCube d Kc).scale : ℤ) - (j : ℤ)
    = recurrenceMesoScale recurrenceGapMultiplier M.gamma m (hgap : ℤ)
```
and (originCube d Kc).scale = Kc, so at a fixed j that identity pins Kc to the single value j + recurrenceMesoScale .... Both producers also carry the localization gap 10^10 cgamma^{-1} <= Kc - m, which fails for small Kc. A ∀ K premise at fixed j is therefore not obtainable from them. Exactly two changes are needed, both harmless for the limit passage: the depth becomes a family jf : ℕ → ℕ (one depth per cube scale), and the junctions are consumed eventually in K rather than for all K (ge_of_tendsto in place of ge_of_tendsto'). upperDisplay_of_junctionFamilies and lowerDisplay_of_junctionFamilies below are the skeletons in that shape; closureMeshDepth is the depth family the producers name.

What is supplied #

upperDisplay_of_junctionFamilies, lowerDisplay_of_junctionFamilies --- the two assembly skeletons in the corrected shape.
closureDirichletFamily, closureNeumannFamily --- the two corrector families of e.def.w, indexed by the increment path exactly as Closure.alongIncrementPath and the fresh-shell energy display require, built from Corrector.exists_isZeroTraceDirichletRhsWeakSolution_openCubeSet_of_continuous and its Neumann mirror. Their two weak formulations are proved at every (K, f), and transported to the streamForcing shape the terminal, Step 4 and Step 5 read, by Corrector.toVec_realize_valuePathForcing_shellSumValuePath.
closureMeshDepth, eventually_closureMeshDepth_scale --- the depth family and its depth-naming identity, valid for every large cube scale.
eventually_principalSwitchEndpoint_closureFamilies --- Junction 4 at the chosen families, for every large cube scale, from Closure.JunctionDischargePrincipalSwitch.principalSwitchEndpoint_of_terminal.
tendsto_neumannCubeEnergy_closureNeumannFamily, tendsto_dirichletCubeEnergy_closureDirichletFamily --- the drift limit hlimit of both skeletons, reduced to the two AEStronglyMeasurable typing binders the proved display Corrector.ShellSumEnergyDisplay.tendsto_integral_cutoffSample_cubeAverage_display already carries; the two weak formulations it asks for are discharged by the construction, and the limit value is matched to Closure.shellDrift through Closure.shellDrift_eq_shellSum.
exists_const_recurrenceUpperDisplay_of_inflight, exists_const_recurrenceLowerDisplay_of_inflight --- the two printed displays of e.what.do.we.have, conditional on the premises listed below and on nothing else.

The premises that remain, and their producers #

Neither conditional assembly assumes any estimate of the manuscript beyond the following, each of which is a named producer's output:

premise	content	producer
`hsplit`	Junction 3, `e.lower.bound.basic.split` + `e.lower.bound.localization.terms` at the
`cgamma^10` endpoint	IN, lane `gamma10-fold`; reduce to one finite grid first with
`Closure.AnnealedLimitJunction.annealedSplitEndpoint_of_integral_ch02CoarseBlockMatrix_le`
`hstep4`	Junction 1 at the chosen families
`Closure.JunctionDischargeStepFour.step4GaugeEndpoint_of_correctors`, whose `hD` binder is
`isZeroTraceDirichletRhsWeakSolution_alongIncrementPath` below and whose four remaining binders are
the analytic side conditions its own docstring table charges to
`Corrector.CorrectorMeasurableGradient` and `Corrector.CorrectorLimitNode`
`hstep5`	Junction 2 at the chosen families
`Closure.JunctionDischargeStepFiveDisplay.step5GaugeEndpoint_of_correctors_gauge` (per-cube gauge),
whose `hosc` binder is supplied by `Closure.Step5DefectGauge`'s re-sited full-mesh producer and
whose remaining binders are that module's own table
`hDm`, `hNm`	`AEStronglyMeasurable` of the two cube energies along the increment path	the
path-carrier analogue of `Corrector.CorrectorMeasurableForcing.continuous_contMatrixFieldL2`
composed with `Corrector.MeasurablePrereqSolutionOperator`'s continuous solution operators; not
built here

hgamma, hcap, hsmall are the parameter-regime facts the manuscript grants (e.cgamma.constraints, Closure.shellDrift_le_cap); they are carried as binders, not assumed away.

References #

ABK26, l.approximate.recurrence.formula, Steps 4--6.
ABK26, e.def.w; e.perturb.assumption.

ClosureAssembly #

The closure assembly: the two displays at one explicit pair of correctors #

Two shape deltas against Closure.Junctions' skeletons, and what replaces #

What is supplied #

The premises that remain, and their producers #

References #

The corrector families #

The mesh depth attached to a localization scale #

The drift limit at the constructed families #

Junction 4 at the constructed families, for every large localization cube #

The conditional assembly #

Two shape deltas against `Closure.Junctions`' skeletons, and what replaces #