High-contrast homogenization: Provider.Quenched.SmallContrastFusionStep #
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
The fusion's ∀ n binder body #
the corresponding argument step 3. Inside the fusion's ∀ n ≥ n_s binder, the account's hatted
one-step conclusion at the generation t = N₀ + n has to become one line of
the drop-history recursion for the sequence F j = hatExcess P q N₀ j. This
file is that line, isolated as a lemma so the outer assembly can apply it
without carrying the algebra.
The identifications are definitional: hatExcess P q N₀ n is
d(Θ̂_{N₀+n} − 1), and the account's lagged scale s = t − H is
N₀ + (n − H), so one_step_to_scalar_step_isotropy (the scalar conversion) yields directly in the
shape per_generation_hrec_at_recursionAlpha_sharp_at_jb_src consumes. Nothing else happens
here; the three coefficients are dropCoefficient, quadCoefficient and
weakCoefficient of the corresponding argument.