High-contrast homogenization: Entry.Response.Kernel.TerminalDefectDepthZeroBound

Imported from the Apache-2.0 HighContrastHomogenization development at commit 7a13dbcd8d6609264a713373f5c69ceeac870472.

The depth-zero bound on the terminal defect

This file proves the two-sided depth-0 bound on the normalized terminal defect of the recentred and adjoint coarse blocks against their own annealed blocks, and composes it with the analytic core of the recentring bound to obtain the estimate integral_respRecentre_sq_le_minus/_plus (p.response.transfer): the correction from the random cell average to the annealed centre, integrated over the coefficient law via response_allscale_abs and the integrability of respAllScaleAbs. A short leaf of purely real-number identities and inequalities - squares of scaled square roots, the reciprocal bound on 1 - 3^{-1/2}, and the rewriting of η^{1/(2Q)} powers - is carried alongside it for reuse when the weak-norm estimate is finally assembled.

The random-to-annealed recentring (p.response.transfer)

The recentring layer.

The two twins below rest on the observation that the available respAllScaleMax controls only the spectral positive part.

This is not a gap in the proof but a defect of the STATEMENT: the recentring vector c_a = M_0^{1/2} R (A_t(a) − Ehat_t^-) x^- needs a bound on the SIGNED difference, which the one-sided respAllScaleMax provably cannot give (the one-sided hypothesis is too weak for this bound, for every constant). Accordingly the two carrier premises of both twins are restated on the two-sided respAllScaleAbs, exactly as for the earlier twins. The restatement is free of new obligations: response_allscale_abs produces the moment bound and respAllScaleAbs_aestronglyMeasurable_integrable the integrability, and integral_recentDefect_sq_le_of_rawOutput_minus/_plus are the compiled proof that they compose from RawOutput alone.

The analytic core is the comparison profilePrimalCenterVariance_le_variance through centered_metric_quadratic_le; it lives in RandomToAnnealedRecentring.lean, imported above. What remains here is the three steps that need the earlier layer: the depth-0 comparison with respAllScaleAbs, measurability, and Jensen.

theorem HCPolySupport.HighContrast.Multiscale.integral_respRecentre_sq_le_minus (d : ℕ) (hd : 2 ≤ d) (γ : ℝ) (hγ : γ ∈ Set.Ico 0 1) (S : SelectionData) (hS : S.Selects d γ) (Cc Cm : ℝ) (hCc : 0 < Cc) (hCm : 0 < Cm) : ∃ (C : ℝ), 0 < C ∧ ∀ (ε σ Cglob Cprof Csrc Bresp : ℝ) (H : ℕ) (P : MeasureTheory.Measure (CoeffSpace d)) (E : BlockMat d) (Ψ : ℝ → ℝ) (Kg : ℝ) (Src : CoeffSpace d → ℝ) (B : ℝ) (jStar : ℕ) (F : BlockMat d) (s t : ℤ), RawOutput d γ S ε σ Cglob Cprof Csrc H Bresp P E Ψ Kg Src B jStar F s t → RespCalibrated Cc P jStar F s t → ∀ η ∈ Set.Ioo 0 (1 / 2), MeasureTheory.Integrable (fun (a : CoeffSpace d) => respAllScaleAbs P γ jStar F t a ^ bigQ d γ) P → ∫ (a : CoeffSpace d), respAllScaleAbs P γ jStar F t a ^ bigQ d γ ∂P ≤ Cm * η → ∀ (e : Vec d), vecDot e e = 1 → ∀ (u : (a : CoeffSpace d) → AHarmonicFunction (respCoeffMinus F a) (respCell jStar F t)), (∀ (a : CoeffSpace d), IsResponseMaximizer (respCell jStar F t) (respP (respMean P jStar F t) e) (respqMinus P jStar F t e) (respCoeffMinus F a) (u a)) → MeasureTheory.Integrable (fun (a : CoeffSpace d) => blockVecDot (respRecentreMinus P jStar F t e a (u a)) (respRecentreMinus P jStar F t e a (u a))) P ∧ ∫ (a : CoeffSpace d), blockVecDot (respRecentreMinus P jStar F t e a (u a)) (respRecentreMinus P jStar F t e a (u a)) ∂P ≤ C * (respK0SqMinus P jStar F t * respLsqMinus P jStar F t e) * η ^ (2 / ↑(bigQ d γ))

The recentring estimate, minus sign. ⟨X_a⟩_{U_t} = blockResponseMean (A^b_t(a)) x^- and Y^- = blockResponseMean (Ehat_t^-) x^- = ∫ ⟨X_a⟩_{U_t} dP (integral_blockResponseMean; its integrability binders come from RawOutput), so c_a = M_0^{1/2} R (A^b_t(a) - Ehat_t^-) x^- and |c_a| ≤ K_0 · ‖Ehat^{-1/2}(A_t(a)-Ehat)Ehat^{-1/2}‖ · L^- (‖M_0^{1/2} R Ehat^{1/2}‖^2 = K_0^2 since R = blockSwap and S M_0^{1/2} = M_0^{-1/2} S); the two-sided difference at depth 0 is bounded as in the earlier layer by M(a) (+ swap-conjugate lower side), and ∫ M^2 ≤ (∫ M^Q)^{2/Q}.

theorem HCPolySupport.HighContrast.Multiscale.integral_respRecentre_sq_le_plus (d : ℕ) (hd : 2 ≤ d) (γ : ℝ) (hγ : γ ∈ Set.Ico 0 1) (S : SelectionData) (hS : S.Selects d γ) (Cc Cm : ℝ) (hCc : 0 < Cc) (hCm : 0 < Cm) : ∃ (C : ℝ), 0 < C ∧ ∀ (ε σ Cglob Cprof Csrc Bresp : ℝ) (H : ℕ) (P : MeasureTheory.Measure (CoeffSpace d)) (E : BlockMat d) (Ψ : ℝ → ℝ) (Kg : ℝ) (Src : CoeffSpace d → ℝ) (B : ℝ) (jStar : ℕ) (F : BlockMat d) (s t : ℤ), RawOutput d γ S ε σ Cglob Cprof Csrc H Bresp P E Ψ Kg Src B jStar F s t → RespCalibrated Cc P jStar F s t → ∀ η ∈ Set.Ioo 0 (1 / 2), MeasureTheory.Integrable (fun (a : CoeffSpace d) => respAllScaleAbs P γ jStar F t a ^ bigQ d γ) P → ∫ (a : CoeffSpace d), respAllScaleAbs P γ jStar F t a ^ bigQ d γ ∂P ≤ Cm * η → ∀ (e : Vec d), vecDot e e = 1 → ∀ (u : (a : CoeffSpace d) → AHarmonicFunction (respCoeffPlus F a) (respCell jStar F t)), (∀ (a : CoeffSpace d), IsResponseMaximizer (respCell jStar F t) (respP (respMean P jStar F t) e) (respqPlus P jStar F t e) (respCoeffPlus F a) (u a)) → MeasureTheory.Integrable (fun (a : CoeffSpace d) => blockVecDot (respRecentrePlus P jStar F t e a (u a)) (respRecentrePlus P jStar F t e a (u a))) P ∧ ∫ (a : CoeffSpace d), blockVecDot (respRecentrePlus P jStar F t e a (u a)) (respRecentrePlus P jStar F t e a (u a)) ∂P ≤ C * (respK0SqPlus P jStar F t * respLsqPlus P jStar F t e) * η ^ (2 / ↑(bigQ d γ))

The recentring estimate, plus sign.

The constant chain K_0 L^± ≤ C κ_s^{1/2} (p.response.transfer)

The two scale-selection premises.

Can κ_t ≤ C κ_s and 1 ≤ κ be derived from what RawOutput / RespCalibrated ALREADY state? Yes, with one caveat. Both facts are already proved, with C = 1, by response_imbalance_comparison (HCPoly/Entry/Response/Core/ResponseImbalanceComparison.lean, sorry-free, in the import closure of this file through LoadMeanIdentity): 1 ≤ κ_t ∧ κ_t ≤ κ_s ∧ κ_s ≤ r² κ_t ∧ 1 ≤ r ∧ r < exp(d σ). CAVEAT: response_imbalance_comparison carries two premises that this statement -- and the statement in WeakEstimateAssembly.lean -- do NOT carry: hε : ε ∈ Set.Ioc 0 S.eps0 and hσ : σ ∈ Set.Ioc 0 ε. They are needed because without them S.one_le_B0 is unavailable, so 1 ≤ B fails, so raw.hs_lo does not give j_* < s, so Annealed.adaptedMean_antitone (HCPoly/Entry/Annealed/AnnealedBlockOrder.lean, which needs (jStar : ℤ) ≤ j ≤ k) does not give E_t ≤ E_s, which is what canonicalImbalance_mono consumes for κ_t ≤ κ_s. 1 ≤ κ_t alone does NOT need them. So the missing inequality is NOT one of RespCalibrated: it is a premise gap at the statement.

respKappa_persistence_of_raw below is that derivation, compiled. respK0Sq_mul_Lsq_le_arith, respLsq_bounds_of_energyDefect, respK0Sq_nonneg and respK0Sq_mul_Lsq_le_kappa_of_calibration_step are the compiled constant chain on top of it: with the single remaining routine matrix step K_0² ≤ C_c √κ_t they close the chain with the explicit constant C = 2 C_c (1 + C_e).

theorem HCPolySupport.HighContrast.Multiscale.respKappa_persistence_of_raw (d : ℕ) (hd : 2 ≤ d) (γ : ℝ) (hγ : γ ∈ Set.Ico 0 1) (S : SelectionData) (hS : S.Selects d γ) (ε σ : ℝ) (hε : ε ∈ Set.Ioc 0 S.eps0) (hσ : σ ∈ Set.Ioc 0 ε) (Cglob Cprof Csrc Bresp : ℝ) (H : ℕ) (P : MeasureTheory.Measure (CoeffSpace d)) (E : BlockMat d) (Ψ : ℝ → ℝ) (Kg : ℝ) (Src : CoeffSpace d → ℝ) (B : ℝ) (jStar : ℕ) (F : BlockMat d) (s t : ℤ) (raw : RawOutput d γ S ε σ Cglob Cprof Csrc H Bresp P E Ψ Kg Src B jStar F s t) : 1 ≤ respKappa P jStar F t ∧ respKappa P jStar F t ≤ respKappa P jStar F s

The persistence inequality (a), compiled. 1 ≤ κ_t and κ_t ≤ κ_s from RawOutput alone, ONCE the two scale-selection premises hε, hσ of response_imbalance_comparison are available. A pure re-export of the first two conjuncts of response_imbalance_comparison; it records, in compiled form, exactly which premises the inequality turns on.

theorem HCPolySupport.HighContrast.Multiscale.respK0Sq_mul_Lsq_le_arith {Cc Ce k0sq lsq kt ks : ℝ} (hCc : 0 < Cc) (_hCe : 0 < Ce) (hkt1 : 1 ≤ kt) (hkts : kt ≤ ks) (_hk0nn : 0 ≤ k0sq) (hk0 : k0sq ≤ Cc * √kt) (hlnn : 0 ≤ lsq) (hl : lsq ≤ 2 + 2 * Ce * √ks) : k0sq * lsq ≤ (2 * Cc + 2 * Cc * Ce) * ks

The constant chain as pure real arithmetic: K_0² ≤ C_c √κ_t, L² ≤ 2 + 2 C_e √κ_s and 1 ≤ κ_t ≤ κ_s give K_0² L² ≤ 2 C_c (1 + C_e) κ_s. The step that consumes 1 ≤ κ_s is √κ_s ≤ κ_s.

theorem HCPolySupport.HighContrast.Multiscale.respLsq_bounds_of_energyDefect {d : ℕ} (Ce : ℝ) (P : MeasureTheory.Measure (CoeffSpace d)) (jStar : ℕ) (F : BlockMat d) (s t : ℤ) (e : Vec d) (hE : RespEnergyDefect Ce P jStar F s t e) : 0 ≤ respLsqMinus P jStar F t e ∧ 0 ≤ respLsqPlus P jStar F t e ∧ respLsqMinus P jStar F t e ≤ 2 + 2 * Ce * √(respKappa P jStar F s) ∧ respLsqPlus P jStar F t e ≤ 2 + 2 * Ce * √(respKappa P jStar F s)

The L² side of the constant chain, compiled. RespEnergyDefect alone gives both 0 ≤ (L^±)² (in fact 2 ≤ (L^±)²) and (L^±)² ≤ 2 + 2 C_e √κ_s, through (L^±)² = 2(E[J^±] + 1) and 0 ≤ E[J^±] ≤ C_e √κ_s. No extra premise is needed.

theorem HCPolySupport.HighContrast.Multiscale.respK0Sq_nonneg {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) (jStar : ℕ) (F : BlockMat d) (t : ℤ) : 0 ≤ respK0SqMinus P jStar F t ∧ 0 ≤ respK0SqPlus P jStar F t

The constant chain: 0 ≤ K_0^±. blockSpecBound is an sInf over a set of nonnegative reals, so it is nonnegative whether or not that infimum is attained.

theorem HCPolySupport.HighContrast.Multiscale.respK0Sq_mul_Lsq_le_kappa_of_calibration_step (d : ℕ) (hd : 2 ≤ d) (γ : ℝ) (hγ : γ ∈ Set.Ico 0 1) (S : SelectionData) (hS : S.Selects d γ) (Cc Ce : ℝ) (hCc : 0 < Cc) (hCe : 0 < Ce) (ε σ Cglob Cprof Csrc Bresp : ℝ) (H : ℕ) (P : MeasureTheory.Measure (CoeffSpace d)) (E : BlockMat d) (Ψ : ℝ → ℝ) (Kg : ℝ) (Src : CoeffSpace d → ℝ) (B : ℝ) (jStar : ℕ) (F : BlockMat d) (s t : ℤ) : ε ∈ Set.Ioc 0 S.eps0 → σ ∈ Set.Ioc 0 ε → RawOutput d γ S ε σ Cglob Cprof Csrc H Bresp P E Ψ Kg Src B jStar F s t → ∀ (e : Vec d), RespEnergyDefect Ce P jStar F s t e → respK0SqMinus P jStar F t ≤ Cc * √(respKappa P jStar F t) → respK0SqPlus P jStar F t ≤ Cc * √(respKappa P jStar F t) → respK0SqMinus P jStar F t * respLsqMinus P jStar F t e ≤ (2 * Cc + 2 * Cc * Ce) * respKappa P jStar F s ∧ respK0SqPlus P jStar F t * respLsqPlus P jStar F t e ≤ (2 * Cc + 2 * Cc * Ce) * respKappa P jStar F s

The constant chain, conditional witness. The two inequalities, with the explicit constant C = 2 C_c (1 + C_e), from exactly two things beyond RawOutput/RespEnergyDefect:

• the two scale-selection premises hε, hσ that this statement and the statement in WeakEstimateAssembly.lean do not carry, and
• the single remaining routine matrix step K_0^± ≤ C_c √κ_t (hypotheses hKm, hKp), which is RespCalibrated's Ehat_t^± ≤ C_c √κ_t M_0 normalized by M_0 and read off by csInf_le: normalizedBlock_le_scale followed by blockSpecBound_le_of_loewner -- both currently private, hence restated rather than cited here.

This shows that the chain closes, with a concrete constant, as soon as hε/hσ are restored; no new inequality has to be added to RespCalibrated.

theorem HCPolySupport.HighContrast.Multiscale.respK0Sq_mul_Lsq_le_kappa (d : ℕ) (hd : 2 ≤ d) (γ : ℝ) (hγ : γ ∈ Set.Ico 0 1) (S : SelectionData) (hS : S.Selects d γ) (Cc Ce Cl : ℝ) (hCc : 0 < Cc) (hCe : 0 < Ce) (_hCl : 0 < Cl) : ∃ (C : ℝ), 0 < C ∧ ∀ (ε σ Cglob Cprof Csrc Bresp : ℝ) (H : ℕ) (P : MeasureTheory.Measure (CoeffSpace d)) (E : BlockMat d) (Ψ : ℝ → ℝ) (Kg : ℝ) (Src : CoeffSpace d → ℝ) (B : ℝ) (jStar : ℕ) (F : BlockMat d) (s t : ℤ), ε ∈ Set.Ioc 0 S.eps0 → σ ∈ Set.Ioc 0 ε → RawOutput d γ S ε σ Cglob Cprof Csrc H Bresp P E Ψ Kg Src B jStar F s t → RespCalibrated Cc P jStar F s t → ∀ (e : Vec d), vecDot e e = 1 → RespEnergyDefect Ce P jStar F s t e → RespLoadMean Cl P jStar F s t e → 0 ≤ respK0SqMinus P jStar F t ∧ 0 ≤ respLsqMinus P jStar F t e ∧ 0 ≤ respK0SqPlus P jStar F t ∧ 0 ≤ respLsqPlus P jStar F t e ∧ respK0SqMinus P jStar F t * respLsqMinus P jStar F t e ≤ C * respKappa P jStar F s ∧ respK0SqPlus P jStar F t * respLsqPlus P jStar F t e ≤ C * respKappa P jStar F s

The constant chain. K_0^2 ≤ C_c √κ_t (RespCalibrated, Ehat_t^± ≤ C_c √κ_t M_0, via blockSpecBound of the normalized block), (L^±)^2 = 2(respEJ± + 1) ≤ 2 + 2C_e √κ_s (RespEnergyDefect), alternatively (L^±)^2 ≤ C_c √κ_t · C_l √κ_s (RespLoadMean). Closing to C κ_s needs κ ≥ 1 (canonicalImbalance is the operator norm of a block whose product with its swap-inverse is I, so ≥ 1) and κ_t ≤ C κ_s from RawOutput (persistence, adaptedMean_persistence EccentricityScaleDecay:134 + adaptedMean_antitone, t = s + H). If κ_t ≤ C κ_s is NOT derivable from RawOutput, then the paper's K_0 ≤ C κ_s^{1/4} (p.response.transfer) would be a statement-level gap.

The two premises hε, hσ are binders of this theorem; the matrix step is normalizedBlock_le_scale followed by blockSpecBound_le_of_loewner, and the constant is C = 2 C_c (1 + C_e), exactly as (b) below predicts. A residual gap remains: the statement (WeakEstimateAssembly.lean) and the route assembly response_weak_estimate_of_route still do not carry hε/hσ, so the consumer of this theorem cannot discharge them. The points below record the derivation. (a) 1 ≤ κ_t and κ_t ≤ κ_s ARE derivable, with C = 1, from RawOutput alone -- they are conjuncts 1 and 2 of response_imbalance_comparison (HCPoly/Entry/Response/Core/ResponseImbalanceComparison.lean, sorry-free) -- BUT only once the two scale-selection premises hε : ε ∈ Set.Ioc 0 S.eps0 and hσ : σ ∈ Set.Ioc 0 ε are available. This statement and the statement (WeakEstimateAssembly.lean) do not carry them. See the note above this section and the compiled respKappa_persistence_of_raw. (b) NO new inequality has to be added to RespCalibrated. With hε/hσ restored, the chain closes with the explicit constant C = 2 C_c (1 + C_e); that is the compiled respK0Sq_mul_Lsq_le_kappa_of_calibration_step above, whose only further input is the routine matrix step K_0^± ≤ C_c √κ_t already contained in RespCalibrated. (c) The residual gap is therefore a PREMISE gap at the statement; it cannot be repaired inside this file, because its statement is fixed.

Real arithmetic for the weak-estimate assembly

This leaf module collects the purely real identities and inequalities that are used when the weak-norm estimate is assembled from its pieces. Nothing here mentions a measure, a matrix, a block or a function space: every statement is an identity or an inequality between real numbers.

theorem HCPolySupport.HighContrast.Multiscale.rpow_half_sq (t : ℝ) : (3 ^ (-(t / 2))) ^ 2 = 3 ^ (-t)

(3 ^ (-(t / 2))) ^ 2 = 3 ^ (-t) for the real power.

theorem HCPolySupport.HighContrast.Multiscale.sqrt_mul_sq (c x y s : ℝ) (hx : 0 ≤ x) (hy : 0 ≤ y) : (c * √x * √y * s) ^ 2 = c ^ 2 * (x * y) * s ^ 2

Square of a product of two square roots: (c * √x * √y * s) ^ 2 = c ^ 2 * (x * y) * s ^ 2.

theorem HCPolySupport.HighContrast.Multiscale.scaled_sqrt_sq (c v : ℝ) (hv : 0 ≤ v) : (c * √v) ^ 2 = c ^ 2 * v

Square of a scaled square root: (c * √v) ^ 2 = c ^ 2 * v.

theorem HCPolySupport.HighContrast.Multiscale.one_sub_rpow_pos : 0 < 1 - 3 ^ (-(1 / 2))

3 ^ (-(1 / 2)) < 1, hence 0 < 1 - 3 ^ (-(1 / 2)).

theorem HCPolySupport.HighContrast.Multiscale.rpow_sq_eq (η : ℝ) (hη : 0 ≤ η) (Q : ℝ) (hQ : 0 < Q) : (η ^ (1 / (2 * Q))) ^ 2 = η ^ (1 / Q)

(η ^ (1 / (2 * Q))) ^ 2 = η ^ (1 / Q) for η ≥ 0 and Q > 0.

theorem HCPolySupport.HighContrast.Multiscale.rpow_two_le_one (η : ℝ) (hη0 : 0 < η) (hη1 : η ≤ 1) (Q : ℝ) (hQ : 0 < Q) : η ^ (2 / Q) ≤ η ^ (1 / Q)

For 0 < η ≤ 1 the exponent map is antitone, so η ^ (2 / Q) ≤ η ^ (1 / Q).

theorem HCPolySupport.HighContrast.Multiscale.constant_arith (A B θ z κ X : ℝ) (hA : 0 ≤ A) (hB : 0 ≤ B) (hθ : 0 ≤ θ) (hz : 0 ≤ z) (hκ : 0 ≤ κ) (hX : X ≤ (A * z ^ 2 + B * θ ^ 2) * κ) : X ≤ (√(B + 1) * (θ + √(A + 1) * z) * √κ) ^ 2

Final constant bookkeeping for the weak estimate. If X ≤ (A * z ^ 2 + B * θ ^ 2) * κ and all of A, B, θ, z, κ are nonnegative, then X ≤ (√(B + 1) * (θ + √(A + 1) * z) * √κ) ^ 2.