HomSeamProviderFinal

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

The datum instantiation: the budgeted sup-clause producer, UNCONDITIONAL

What this file does

HomSeamCompositionCcg.generatorRenormalizationShape_of_supClauseProducerAtBudgeted reduces the generator-renormalization root's shape — the sup clause for the coarse-grained flux over the whole depth band, at the budgeted clause constant — to ONE object, SupClauseProducerAtBudgeted. This file PRODUCES that object, with no hypothesis at all (supClauseProducerAtBudgeted_holds), by instantiating the unconditional band-input producer at the lane's own data:

• the clause constant is CcgF M:= max (recutPinnedCcgFlux d p) (produced M) with produced M = (√d · CA(M) · C(p,d)).toReal the displayed constant of HomSpineSupFormClauseAt, at the pin x₀ = homS M · p'; the max raise is CoarseGrainingSupMultiscale.mono_ccg, and it discharges the duality pin via the cgDualBoundConstFlux_le_ofReal_of_pinned_le;
• the budget CcgF M · GEOM ≤ C_bud · |log γ| holds at C_bud = 2·recutPinnedCcgFlux d p + √d·K(d,p)·C(p,d)·2: the produced leg is the seamProducedCcg_le_budget, the pinned leg is the recut_geomFactor_le_absLog (GEOM ≤ 2|log γ|);
• the supply is produced PER SAMPLE, deterministically (ae_of_all shape): the Dirichlet pair gives the forced-equation/scalar/H¹₀ triple at the printed coefficient ã (isDirichletSolutionOn_fluxCorrected_of_cutoff + the HomCGDischargeInstantiation bridges), the Hölder binder gives 𝐠 ∈ W^{s₂,p} (memCubeEuclideanFullWsp_of_holderHalf), the 𝓔/D_g slots self-dominate at their own toReal pins, the two-sided band pin is recutDepthBandPin, and the produced clause is transported to the lane's slots by mono_s1 (error order s/8, clause slot s/4), mono_ccg, and congr_grad_of_eqOn.

generator_renormalization_provider_final is the endpoint: the frozen root's SHAPE at every dimension and every cstar > 0, from {d, cstar, hcstar} and nothing else. The theorem statement itself is neither imported nor claimed here; its discharge is a separate, audited step.

1. THE ONE OBJECT, PRODUCED

theorem Algsuperdiff.Section4.Provider.Homogenization.supClauseProducerAtBudgeted_holds (d : ℕ) (cstar : ℝ) : SupClauseProducerAtBudgeted d cstar

THE BUDGETED SUP-CLAUSE PRODUCER HOLDS. No hypothesis: the band-input producer, instantiated at the lane's own data and transported to the lane's slots.

2. THE ENDPOINT

theorem Algsuperdiff.Section4.Provider.Homogenization.generator_renormalization_provider_final (d : ℕ) (cstar : ℝ) (hcstar : 0 < cstar) : GeneratorRenormalizationShape d cstar

THE PROVIDER, FINAL. The frozen root's shape at every dimension and every cstar > 0, from {d, cstar, hcstar} and NOTHING else. The theorem statement is neither imported nor claimed here.