High-contrast homogenization: Provider.Quenched.SmallContrastCorrectedCadenceDesign #
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
The hcore body from the one-step family, through the corrected descent #
The cadence assembly re-aimed at the corrected three-channel descent
(the strengthened free-threshold estimate): the clauses are discharged exactly as
the cadence design discharges them, but the entry-slot source
is kept explicit through the _src line chain and priced by the
corrected three-channel hypothesis hsrc3 — an absolutely decaying
channel at the anchor, the lag channel, and an absolutely decaying channel
at the generation — and the descent core is
hcore_body_of_corrected_family: the linear level schedule with law-free rate and
linear threshold.
theorem
HCPolySupport.HighContrast.Quenched.hcore_body_of_corrected_design
{d : ℕ}
[NeZero d]
(hd : 2 ≤ d)
{P : MeasureTheory.Measure (CoeffSpace d)}
[MeasureTheory.IsProbabilityMeasure P]
(hstat : IsStationaryLaw P)
{lAl : ℤ}
{E : BlockMat d}
(hgrid : IsRoundedGrid lAl (roundedGrid lAl (canonicalMetric E)))
(hfin : ∀ (k : ℤ), HasFiniteAdaptedMean P (roundedGrid lAl (canonicalMetric E)) k)
{N₀ : ℕ}
(hlN : lAl ≤ ↑N₀)
{g : ℝ}
(hg0 : 0 ≤ g)
(hg1 : g < 1)
{Cpre eta : ℝ}
{H : ℕ}
(hCpre : 0 ≤ Cpre)
(heta : 0 < eta)
(hE : IsSymmetricBlockMat E)
(hEpd : Book.Ch02.BlockPosDef E)
(hsharp : BlockMatLoewnerLE (blockSharp E) E)
(hrecE : canonicalShear E = 0)
{cIso : ℝ}
(hcIso : 0 ≤ cIso)
(hcsmall : cIso < 1)
{cDeep : ℝ}
(hcDeep0 : 0 ≤ cDeep)
{S0 SStar0 K0 : ℕ → Mat d}
(hS0 : ∀ (n : ℕ), Matrix.PosDef (S0 n))
(hStar0 : ∀ (n : ℕ), Matrix.PosDef (SStar0 n))
(hform :
∀ (n : ℕ),
toFullBlockMat (adaptedMean P (roundedGrid lAl (canonicalMetric E)) (↑N₀ + ↑n)) = schurBlock (S0 n) (SStar0 n) (K0 n))
(henvC :
∀ (n : ℕ),
BlockMatLoewnerLE (adaptedMean P (roundedGrid lAl (canonicalMetric E)) (↑N₀ + ↑n)) (isotropyReference cIso E))
(hcompC :
∀ (n : ℕ),
BlockMatLoewnerLE E
(blockScale (isotropyKap2 cIso) (adaptedMean P (roundedGrid lAl (canonicalMetric E)) (↑N₀ + ↑n))))
{Csub Msc delta0 conv deltaDrop : ℝ}
(hCsub : 0 ≤ Csub)
(hMsc : 0 ≤ Msc)
(hdelta0pos : 0 < delta0)
(hconv0 : 0 ≤ conv)
(hdeltaDrop0 : 0 ≤ deltaDrop)
(hbS : 0 ≤ blockSize E (isotropyReference cIso E))
(hfloor : ∀ (m : ℕ), hatExcess P (roundedGrid lAl (canonicalMetric E)) N₀ m ≤ delta0)
(hdropchoice : dropConstantIsotropy (1 + cIso) E (isotropyReference cIso E) * delta0 ≤ deltaDrop)
{M₀ : ℝ}
(hM₀ : metricFactorValue E (1 + cIso) (isotropyKap2 cIso) ≤ M₀)
{K R : ℝ}
{Gacc : ℕ}
{sKw : ℤ}
(hR : 1 ≤ R)
{ns : ℕ}
(hns : H + 1 ≤ ns)
{A : ℝ}
(hAdef :
A = fusionRecursionConstantIsotropySharp d Cpre eta H (absorbedNormalizer 16 16 (designNormalizer R M₀))
(isotropyLoadScale cIso (isotropyKap2 cIso)) g (rowSplitConstant cIso cDeep) (isotropyKap2 cIso)
(dropConstantIsotropy (1 + cIso) E (isotropyReference cIso E)) deltaDrop (slotCVsum d) (cVmConstant d conv))
(hA1 : 1 ≤ A)
{Ssrc0 Ssrc1 Ssrc2 b0 bA b2 : ℝ}
(hSsrc0 : 1 ≤ Ssrc0)
(hSsrc1 : 1 ≤ Ssrc1)
(hSsrc2 : 1 ≤ Ssrc2)
(hb0 : 0 < b0)
(hbA : 0 < bA)
(hb2 : 0 < b2)
{cA : ℕ}
(hgs3 : (128 * A ^ 2) ^ 3 * delta0 ≤ 1 / 3)
(hcA24 : 24 * A ≤ 3 ^ (recursionAlpha g * ↑cA))
(hfam :
∀ (m : ℕ),
ns ≤ m →
∀ (n : ℕ),
ns ≤ n →
adaptedHattedContrast P (roundedGrid lAl (canonicalMetric E)) (↑N₀ + ↑n) - 1 ≤ 4 * Cpre * ((3 / 2 + 1 / (4 * eta)) * (16 * ↑d * (adaptedHattedContrast P (roundedGrid lAl (canonicalMetric E)) (↑N₀ + ↑(n - H)) - adaptedHattedContrast P (roundedGrid lAl (canonicalMetric E)) (↑N₀ + ↑n))) + rowValue2Isotropy d (rowSplitConstant cIso cDeep) (isotropyKap2 cIso)
(hatExcessAt P (roundedGrid lAl (canonicalMetric E)) (↑N₀ + ↑n)) + weakValueBoundSharpIsotropyAt (Response.recentConstantAtLevel R) (Response.maxGroupConstantAtLevel R)
(Response.energyGoodConstantAtLevel R) P (canonicalMetric E) (Response.responseSkew (K0 n))
(isotropyReference cIso E) (loadScaleOfScalar (1 + cIso) (isotropyKap2 cIso)) (canonicalMetric E)
(contrastRho g) (n - ns) (R ^ 4 * badMomentMajorant K (↑N₀ + ↑n + ↑(Gacc + 1) - 1 - sKw)) (R / 2) R
(↑N₀ + ↑n) lAl
(fun (j : ℕ) =>
slotFamilyValue d Csub Msc delta0 (hatExcess P (roundedGrid lAl (canonicalMetric E)) N₀ (min n m))
(n - min n m) j)
(slotFamilyValue d Csub Msc delta0 (hatExcess P (roundedGrid lAl (canonicalMetric E)) N₀ (min n m))
(n - min n m) 0)
(meanDrop2ValueIsotropy P lAl (1 + cIso) (canonicalMetric E) E (isotropyReference cIso E)
(↑N₀ + ↑n))
(conv * slotFamilyValue d Csub Msc delta0 (hatExcess P (roundedGrid lAl (canonicalMetric E)) N₀ (min n m))
(n - min n m) 0)) + 2 * ((3 * ↑d + 4) * hatExcessAt P (roundedGrid lAl (canonicalMetric E)) (↑N₀ + ↑n) ^ 2))
(hsrc3 :
∀ (n m : ℕ),
ns ≤ m →
m ≤ n →
3 * weakCoefficient d Cpre * weakSourceGroupSummed (absorbedNormalizer 16 16 (designNormalizer R M₀))
(isotropyLoadScale cIso (isotropyKap2 cIso)) (contrastRho g)
(slotVsumSharp d Csub Msc delta0 (n - min n m)) (conv * slotSourceSeq d Csub Msc delta0 (n - min n m) 0)
(√2 * √(isotropyLoadScale cIso (isotropyKap2 cIso) + 1) * Response.profileBadMajorantAt 4 (R ^ 4 * badMomentMajorant K (↑N₀ + ↑n + ↑(Gacc + 1) - 1 - sKw))
(R / 2) R + √2 * 3 ^ (-((1 - contrastRho g) / 2) * ↑(n - ns)) * √(isotropyLoadScale cIso (isotropyKap2 cIso) + 1)) ^ 2 ≤ Ssrc1 * 3 ^ (-(bA * ↑m)) + Ssrc0 * 3 ^ (-(b0 * ↑(n - m))) + Ssrc2 * 3 ^ (-(b2 * ↑n)))
{base Centry Cpref : ℝ}
(hbase : 3 ≤ base)
(hCpref : 0 ≤ Cpref)
(hentry : 3 ^ (2 * N₀) ≤ base.rpow Centry)
(hpref :
9 / 2 * ((1 + hatExcess P (roundedGrid lAl (canonicalMetric E)) N₀ 0) * 3 ^ (linRate A (recursionAlpha g) b0 bA b2 cA Ssrc0 * ↑(linR ns cA A (recursionAlpha g) b0 bA b2 Ssrc0 Ssrc1 Ssrc2 delta0 0))) * (Real.rpow 3 (linRate A (recursionAlpha g) b0 bA b2 cA Ssrc0 / 2) + 1) ≤ base.rpow Cpref)
(htransfer :
∀ (m : ℕ),
2 * N₀ ≤ m →
annealedContrast P ↑m - 1 ≤ 9 / 2 * (↑d * (adaptedHattedContrast P (roundedGrid lAl (canonicalMetric E)) ↑(Prop42Scalar.correctedTiltScale N₀ m) - 1)) + 9 / 2 * ((1 + hatExcess P (roundedGrid lAl (canonicalMetric E)) N₀ 0) * 3 ^ (linRate A (recursionAlpha g) b0 bA b2 cA Ssrc0 * ↑(linR ns cA A (recursionAlpha g) b0 bA b2 Ssrc0 Ssrc1 Ssrc2 delta0 0))) * Real.rpow 3 (-↑(m - Prop42Scalar.correctedTiltScale N₀ m)))
:
The hcore body through the corrected descent.