High-contrast homogenization: Entry.Response.Core.ResponseCalibrationBundles #
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
Calibration and source smallness from the raw output #
This file derives two of the hypothesis bundles that adapted_response_core is assembled from,
directly from the raw multiscale output RawOutput: response_calibrated_blocks
(e.response.calibrated.blocks) produces the calibration bundle RespCalibrated from the Riccati
identity and the response-imbalance comparison, and response_source_smallness
(e.response.source.smallness) produces a source-smallness constant Bresp from the two-grid
source normalization and the scale-decay estimate. It also carries the load-quadratic identities —
respLsqMinus/Plus, respEJMinus/Plus, respTauMinus, and the pairings of the response load
vectors against respP — that later files in the chain need.
e.response.calibrated.blocks. The constant
depends only on (d, γ), never on the law, F, E, Pi or σ.
Route: the Riccati identity GeometricMean.geoMean_riccati gives M(E) <= E <= d(E)^{1/2} M(E)
(p.response.transfer); then raw.calib_lo/raw.calib_hi at s, the comparison E_t <= E_s <= r E_t
of response_imbalance_comparison, and GeometricMean.geoMean_mono. The congruence cost is
sqrt(r(1+xi)/(1-xi)) <= C(d) because xi <= 1/2 and r < e^{d/2}; D
commutes with M_0.
The premises _hε, _hσ are carried: without them 1 ≤ B and jStar ≤ s
are unavailable. The binder names are underscore-prefixed because they do not
occur in the statement's own type; the hypotheses are unchanged and the proof uses them
(with no linter suppression).
The source smallness estimate #
e.response.source.smallness:
C Pi e(m)^2 3^{-rho_max(t-j_*)} <= eta^{1/Q} and C Pi e(m)^2 3^{-3(s-j_*)/2} <= 1, once
B_resp is large enough. B_resp is chosen after H, eta, sigma and C_glob, exactly
the printed order (e.response.source.smallness).
Route: raw.hsrc and Annealed.adaptedMean_refBlock_normalization
(e.two.grid.source.normalization, e.two.grid.source.normalization) supply Csrc and the
envelope constant; raw.ecc
(e.global.selection.eccentricity, e.global.selection.eccentricity) bounds e(m)^2 by
(2+Pi)^{2 Cglob}; raw.hs_lo
and raw.ht_hi (e.global.selection.scales, e.global.selection.scales) with
scale_decay_of_hs_lo turn
3^{-rho(u-j_*)} into (2+Pi)^{-rho B}, and exists_Bresp_of_decay then produces
Bresp. raw.hB gives Bresp <= B, and 1 <= aspectRatio E comes from
Analysis.one_le_aspectRatio.
(L^-)^2 = (-p, q - h_t p). E_t (-p, q - h_t p).
(L^+)^2 = (-p, -(q + h_t p)). E_t (-p, -(q + h_t p)).
The reciprocal normalizations: p. q^- = 1 (the skew part cancels).
The reciprocal normalizations: p. q^+ = 1.
Congruence is monotone for the Loewner order.
The third conjunct of the response energy and defect estimate, conditional on the three bridge
inputs hpath, hint, hann
(p.response.transfer).
The fourth conjunct of the response energy and defect estimate, conditional on the three bridge inputs.
The annealed response at one adapted cell, from the pathwise identity, entrywise integrability, and the annealed-block identification.
The defect at the minus load, conditional on the bridge inputs at both scales
(e.response.energy.and.defect, p.response.transfer).
The defect is nonnegative once Ehat_t <= Ehat_s (Annealed.adaptedMean_antitone).