StepSevenWireChain #

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

`t.regularity` Step 7d: the narrowed chain #

What this module does #

The Step-7d end chain is the entry point for Step 7d. It takes four named conditional inputs across its three displays: hcg, hlambda, hembed, hbridge. Three of them are discharged here:

hcg — StepSevenWireCgMatching.exists_stepSevenCgPoincareInput_pinned (CoarseGraining's coarsePoincareRHSTheory, at the pin s₀ = 1/4);
hembed — StepSevenWireEmbedding.stepSevenEmbedding (the Section-3 mean-zero multiscale Poincaré, with the coordinate aggregation and the off-grid recovery);
hbridge — StepSevenWireBridge.stepSevenBesovBridge (the summability conversion).

The narrowed entry point keeps hlambda alone. Its remaining conditional inputs are exactly

  { hlambda ,  the Step-7c hgrad display (which carries hcacc / hlambda / hosc) } ,

plus the caller's own geometry (hmean, hcomp, the three transports and the two Ktr dominations) and the printed nonnegativity/window data. Nothing else.

The carriers of the composition #

Everything is stated at the scale normalization of the cube Q, which under the translate-the-sample convention is originCube d (m'-1) carrying the sample translated by z':

  oscLoc  = 3^{-Q.scale}‖u - (u)_Q‖_{L²(Q)}                     (the embedding LHS)
  besovP1 = cubeBesovNegativeVectorSeminorm Q 1 (∇u)             (B^{-1}_{2,1})
  besov   = scaleNormalizedNegativeBesovVectorNorm Q s₀ (.finite 2) (∇u)
  gradLoc = forcedSolutionEnergyNorm Q a u ,  dataLoc = [𝐠]_{B^{s₀}_{2,2}(Q)}

with s₀ = stepSevenCgS = 1/4. Neither Besov membership is a hypothesis: the B^{-s₀}_{2,2} side is CoarseGraining's proved forcedSolutionGradientField_negativeBesovPartialSeminormTwo_bddAbove (automatic for every ForcedCubeSolution), and the B^{-1}_{2,1} side is derived from it through the conversion (bddAbove_partialOne_of_partialTwo).