High-contrast homogenization: Provider.Quenched.SmallContrastLineProducer #
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
hline: the per-generation producer at the sharp constant #
The per-generation analytic estimate.
hline is precisely hrec_line_of_slots_isotropy_sharp_at_jb_at_level_src's conclusion
quantified
over n ≥ ns (the cited theorem). the corresponding argument found no producer in
the construction: the account that would feed it was never built. This file builds
it, in the two stages the corresponding argument separated.
the corresponding step — the constants pack. Nine of the seventeen n-free hypotheses are
pure scalar side conditions on the slot constants. IsotropySlotConstants bundles
them so the producer's binder stays readable, and the isotropic slot constants
are supplied from the exponent pack's g-clauses plus the four positivity facts
a caller already has.
the corresponding step — the producer. hline_of_slots_sharp_var_at_jb_at_level_src takes
the n-free data once
and the n-dependent slots as families over n, and discharges ∀ n ≥ ns by
hrec_line_of_slots_isotropy_sharp_at_jb_at_level_src at each generation.
The carriers that must vary with the generation are exactly V, V0, Dr,
Vmean, bmaj, wv and jb; everything appearing in the recursion constant
or in the recursion tolerance — cD, delta, cVsum, cVm, vsum, vmsrc,
bsrc — is
n-free of necessity, since fusionRecursionConstantIsotropySharp and the geometric
term are fixed across the recursion. That split is forced by the statement, not
chosen.
the corresponding step: the constants pack #
The nine scalar side conditions of the isotropy slot line. Bundling them keeps the producer's binder to the data that actually varies.