High-contrast homogenization: Provider.Quenched.CoupledWitnessAssembly

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

Assembly of the coupled mixing-scale witness

The finite-range engine fixes its stretched-exponential tail constant before the exponent and before the coefficient law. This file records the remaining outer composition: a normalized reference-family package supplies the decay, row-series and polynomial-cost data for each law, while the unit-range renormalization theorem constructs the coupled witness.

structure HCPolySupport.HighContrast.Quenched.CoupledWitnessEngineData {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) (gamma : ℝ) (E : BlockMat d) (Psi : ℝ → ℝ) (K : ℝ) (S : CoeffSpace d → ℝ) (Abar : BlockMat d) (Nann : ℕ) (theta deltaOut Cmix : ℝ) : Type

The lawwise data left after selecting the exponent and the uniform polynomial cost. It contains no coupled witness: that witness is constructed by the finite-range renormalization engine.

• mu : ℝ

  Positive exponent d / 2 - gamma used in the radius-tail bounds.

• nstar : ℕ

  Starting generation for the radius-tail and quenched row-decay estimates.

• qfb : ℕ

  Generation offset supplied to the stopping-generation construction.

• b : ℕ

  Additional generation offset in the radius-tail threshold.

• N0 : ℕ

  Absolute generation threshold satisfying the stopping and tail-gain conditions.

• radius : ℕ → CoeffSpace d → ℝ

  Generation-dependent random radius with the prescribed finite-range tail estimate.

• F : ℕ → CoeffSpace d → ℝ

  Measurable weighted row-tail sum, with weight 3 ^ (theta / 2 * j).

• Cblk : ℝ

  Positive prefactor in the quenched physical block-row decay estimate.

• Bconst : ℝ

  Normalizer bounded below by one and controlled by the polynomial cost.

• C1 : ℝ

  Polynomial cost exponent controlling 3 ^ N0.

• C2 : ℝ

  Polynomial cost exponent controlling the normalizer Bconst.

• C3 : ℝ

  Polynomial cost exponent whose base power absorbs the factor three.

• Cstop : ℝ

  Total stopping cost bounding the sum C1 + C2 + C3.

• Cround : ℝ

  Rounding cost exponent whose base power absorbs the factor three.

• mu_eq : self.mu = ↑d / 2 - gamma
• mu_pos : 0 < self.mu
• radius_tail (n q : ℕ) : self.nstar ≤ n → P.real {a : CoeffSpace d | 3 ^ (n + q + self.b) < self.radius n a} ≤ Real.exp (-(frGaugeConst d * 3 ^ (2 * self.mu * ↑q)))
• Cblk_pos : 0 < self.Cblk
• F_measurable (n : ℕ) : Measurable (self.F n)
• row_decay : ∀ᵐ (a : CoeffSpace d) ∂P, ∀ (m : ℕ), self.nstar ≤ m → quenchedBlockRow ((1 + 3 * gamma) / 4) Abar (max 1 (S a / 3 ^ Nann)) (physicalScaleCoefficient Nann a) m ≤ self.Cblk * deltaOut * 3 ^ (-theta * (↑m - ↑(stoppingGeneration self.nstar self.qfb self.radius m a) - ↑self.nstar))
• row_nonnegative (m : ℕ) (a : CoeffSpace d) : 0 ≤ quenchedBlockRow ((1 + 3 * gamma) / 4) Abar (max 1 (S a / 3 ^ Nann)) (physicalScaleCoefficient Nann a) m
• row_hasSum : ∀ᵐ (a : CoeffSpace d) ∂P, ∀ (k : ℕ), HasSum (fun (j : ℕ) => 3 ^ (theta / 2 * ↑j) * quenchedBlockRow ((1 + 3 * gamma) / 4) Abar (max 1 (S a / 3 ^ Nann)) (physicalScaleCoefficient Nann a) (k + j)) (self.F k a)
• nstar_le_N0 : self.nstar ≤ self.N0
• one_le_Bconst : 1 ≤ self.Bconst
• threshold_low : ↑self.qfb + ↑self.b + 1 + rowSplitOffset theta self.Cblk ≤ ↑self.N0 - ↑self.nstar
• threshold_gain : Real.log 2 ≤ frGaugeConst d * 3 ^ (2 * self.mu * (↑self.N0 - ↑self.nstar - badTailOffset theta self.Cblk self.qfb self.b)) * (3 ^ (self.mu / 2) - 1)
• threshold_absolute : 2 * Real.log 4 ≤ frGaugeConst d * 3 ^ (2 * self.mu * (↑self.N0 - ↑self.nstar - badTailOffset theta self.Cblk self.qfb self.b))
• normalizer_relation : 3 ^ (2 * self.mu * (↑self.nstar + badTailOffset theta self.Cblk self.qfb self.b - ↑self.N0)) ≤ frGaugeConst d / 2 * self.Bconst ^ (2 * self.mu)
• one_le_base : 1 ≤ 2 + aspectRatio E * K
• three_le_base_pow : 3 ≤ (2 + aspectRatio E * K) ^ self.C3
• generation_cost : 3 ^ self.N0 ≤ (2 + aspectRatio E * K) ^ self.C1
• normalizer_cost : self.Bconst ≤ (2 + aspectRatio E * K) ^ self.C2
• raw_cost : self.C1 + self.C2 + self.C3 ≤ self.Cstop
• rounding_cost : 3 ≤ (2 + aspectRatio E * K) ^ self.Cround
• final_cost : self.Cround + self.Cstop ≤ Cmix

theorem HCPolySupport.HighContrast.Quenched.exists_coupledWitnessAssembly (d : ℕ) (_hd : 2 ≤ d) (hdata : ∀ g ∈ Set.Ico 0 1, ∀ (alpha : ℝ), 0 < alpha → ∃ (Cmix : ℝ) (theta : ℝ) (deltaOut : ℝ), 0 < Cmix ∧ 0 < theta ∧ deltaOut ∈ Set.Ioo 0 1 ∧ ∀ (P : MeasureTheory.Measure (CoeffSpace d)) (E : BlockMat d) (Psi : ℝ → ℝ) (K : ℝ) (S : CoeffSpace d → ℝ) (Abar : BlockMat d) (Nann : ℕ), MeasureTheory.IsProbabilityMeasure P → IsStationaryLaw P → IsUnitRangeLaw P → CoarseEllipticityDagger P g E Psi K S → IsSymmetricBlockMat Abar → Book.Ch02.BlockPosDef Abar → (∀ (j : ℕ), annealedContrast P ↑(Nann + j) - 1 ≤ 3 ^ (-alpha * ↑j)) → (∀ (j : ℕ), BlockMatLoewnerLE Abar (annealedBlock P (centeredCube d ↑(Nann + j))) ∧ BlockMatLoewnerLE (annealedBlock P (centeredCube d ↑(Nann + j))) (blockScale (1 + 6 * 3 ^ (-alpha * ↑j)) Abar)) → Nonempty (CoupledWitnessEngineData P g E Psi K S Abar Nann theta deltaOut Cmix)) : ∃ (cd : ℝ), 0 < cd ∧ ∀ g ∈ Set.Ico 0 1, ∀ (alpha : ℝ), 0 < alpha → ∃ (Cmix : ℝ) (cMix : ℝ) (kappa : ℝ) (delta : ℝ), 0 < Cmix ∧ 0 < cMix ∧ 0 < kappa ∧ delta ∈ Set.Ioo 0 1 ∧ ∀ (P : MeasureTheory.Measure (CoeffSpace d)) (E : BlockMat d) (Psi : ℝ → ℝ) (K : ℝ) (S : CoeffSpace d → ℝ) (Abar : BlockMat d) (Nann : ℕ), MeasureTheory.IsProbabilityMeasure P → IsStationaryLaw P → IsUnitRangeLaw P → CoarseEllipticityDagger P g E Psi K S → IsSymmetricBlockMat Abar → Book.Ch02.BlockPosDef Abar → (∀ (j : ℕ), annealedContrast P ↑(Nann + j) - 1 ≤ 3 ^ (-alpha * ↑j)) → (∀ (j : ℕ), BlockMatLoewnerLE Abar (annealedBlock P (centeredCube d ↑(Nann + j))) ∧ BlockMatLoewnerLE (annealedBlock P (centeredCube d ↑(Nann + j))) (blockScale (1 + 6 * 3 ^ (-alpha * ↑j)) Abar)) → ∃ (W : CoupledMixingScaleWitness P (fun (m : ℕ) (a : CoeffSpace d) => quenchedBlockRow ((1 + 3 * g) / 4) Abar (max 1 (S a / 3 ^ Nann)) (physicalScaleCoefficient Nann a) m) cMix cd (↑d - 2 * g) kappa delta), W.normalization ≤ (2 + aspectRatio E * K) ^ Cmix

Assemble the coupled witness in the quantifier order used by the random homogenization root. In particular, the dimensional tail constant is selected before the exponent, and the four witness constants are selected before the law and all of its coefficient data.