Coarse-graining support: Support.Book.Ch04.Internal.ScalarizationWitnesses

Imported from the Apache-2.0 CoarseGraining development at commit c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.

Scalarization witness internals

This file contains the route-specific witness and primitive-data machinery used to prove the public Chapter 4 scalarization theorems. The note-facing API should prefer direct theorem endpoints over these objects.

structure HCPolySupport.Book.Ch04.Internal.AnnealedScalarizationWitness {d : ℕ} (P : RestrictionCoeffLaw d) (n : ℤ) : Type

Witness data for scalarization of annealed matrices at scale n.

• sigma : ℝ

  The scalar multiplying the identity in the annealed σ matrix at scale n.

• sigmaStar : ℝ

  The scalar multiplying the identity in the annealed σ* matrix at scale n.

• sigma_eq : annealedSigmaAtScale P n = self.sigma • 1
• sigmaStar_eq : annealedSigmaStarAtScale P n = self.sigmaStar • 1
• kappa_eq_zero : annealedKappaAtScale P n = 0

def HCPolySupport.Book.Ch04.Internal.HasAnnealedScalarizationAtScale {d : ℕ} (P : RestrictionCoeffLaw d) (n : ℤ) : Prop

Scalarization at scale n, packaged as a witness.

Equations

• HCPolySupport.Book.Ch04.Internal.HasAnnealedScalarizationAtScale P n = Nonempty (HCPolySupport.Book.Ch04.Internal.AnnealedScalarizationWitness P n)

structure HCPolySupport.Book.Ch04.Internal.AnnealedScalarizationInvarianceData {d : ℕ} [NeZero d] (P : RestrictionCoeffLaw d) (n : ℤ) : Prop

Abstract invariance data sufficient to build a scalarization witness.

• sigmaFlip : IsSignFlipInvariant (annealedSigmaAtScale P n)
• sigmaSwap : IsSwapInvariant (annealedSigmaAtScale P n)
• sigmaStarFlip : IsSignFlipInvariant (annealedSigmaStarAtScale P n)
• sigmaStarSwap : IsSwapInvariant (annealedSigmaStarAtScale P n)
• kappa_eq_zero : annealedKappaAtScale P n = 0

structure HCPolySupport.Book.Ch04.Internal.AnnealedScalarizationPrimitiveData {d : ℕ} [NeZero d] (P : RestrictionCoeffLaw d) (n : ℤ) : Prop

Primitive scalarization data for the annealed b and \sigma_*^{-1} blocks.

• sigmaStarInvFlip : IsSignFlipInvariant (annealedSigmaStarInvAtScale P n)
• sigmaStarInvSwap : IsSwapInvariant (annealedSigmaStarInvAtScale P n)
• bFlip : IsSignFlipInvariant (annealedBAtScale P n)
• bSwap : IsSwapInvariant (annealedBAtScale P n)
• sigmaStarInvKappaMean_eq_zero : annealedSigmaStarInvKappaMeanAtScale P n = 0

noncomputable def HCPolySupport.Book.Ch04.Internal.annealedContrastAtScale {d : ℕ} {P : RestrictionCoeffLaw d} {n : ℤ} (w : AnnealedScalarizationWitness P n) : ℝ

The scalar contrast ratio attached to a chosen scalarization witness.

Equations

• HCPolySupport.Book.Ch04.Internal.annealedContrastAtScale w = w.sigma * w.sigmaStar⁻¹

theorem HCPolySupport.Book.Ch04.Internal.annealedSigmaAtScale_isScalarMatrix_of_invariant {d : ℕ} [NeZero d] (P : RestrictionCoeffLaw d) (n : ℤ) (hFlip : IsSignFlipInvariant (annealedSigmaAtScale P n)) (hSwap : IsSwapInvariant (annealedSigmaAtScale P n)) : IsScalarMatrix (annealedSigmaAtScale P n)

theorem HCPolySupport.Book.Ch04.Internal.annealedSigmaStarInvAtScale_isScalarMatrix_of_invariant {d : ℕ} [NeZero d] (P : RestrictionCoeffLaw d) (n : ℤ) (hFlip : IsSignFlipInvariant (annealedSigmaStarInvAtScale P n)) (hSwap : IsSwapInvariant (annealedSigmaStarInvAtScale P n)) : IsScalarMatrix (annealedSigmaStarInvAtScale P n)

theorem HCPolySupport.Book.Ch04.Internal.annealedBAtScale_isScalarMatrix_of_invariant {d : ℕ} [NeZero d] (P : RestrictionCoeffLaw d) (n : ℤ) (hFlip : IsSignFlipInvariant (annealedBAtScale P n)) (hSwap : IsSwapInvariant (annealedBAtScale P n)) : IsScalarMatrix (annealedBAtScale P n)

theorem HCPolySupport.Book.Ch04.Internal.annealedSigmaStarAtScale_isScalarMatrix_of_invariant {d : ℕ} [NeZero d] (P : RestrictionCoeffLaw d) (n : ℤ) (hFlip : IsSignFlipInvariant (annealedSigmaStarAtScale P n)) (hSwap : IsSwapInvariant (annealedSigmaStarAtScale P n)) : IsScalarMatrix (annealedSigmaStarAtScale P n)

theorem HCPolySupport.Book.Ch04.Internal.annealedSigmaStarAtScale_isScalarMatrix_of_sigmaStarInv {d : ℕ} (P : RestrictionCoeffLaw d) (n : ℤ) (hScalar : IsScalarMatrix (annealedSigmaStarInvAtScale P n)) : IsScalarMatrix (annealedSigmaStarAtScale P n)

theorem HCPolySupport.Book.Ch04.Internal.annealedKappaAtScale_eq_zero_of_sigmaStarInvKappaMean_eq_zero {d : ℕ} (P : RestrictionCoeffLaw d) (n : ℤ) (hMean : annealedSigmaStarInvKappaMeanAtScale P n = 0) : annealedKappaAtScale P n = 0

theorem HCPolySupport.Book.Ch04.Internal.annealedSigmaAtScale_eq_annealedBAtScale_of_sigmaStarInvKappaMean_eq_zero {d : ℕ} (P : RestrictionCoeffLaw d) (n : ℤ) (hMean : annealedSigmaStarInvKappaMeanAtScale P n = 0) : annealedSigmaAtScale P n = annealedBAtScale P n

theorem HCPolySupport.Book.Ch04.Internal.annealedSigmaAtScale_isScalarMatrix_of_bInvariant_of_sigmaStarInvKappaMean_eq_zero {d : ℕ} [NeZero d] (P : RestrictionCoeffLaw d) (n : ℤ) (hBFlip : IsSignFlipInvariant (annealedBAtScale P n)) (hBSwap : IsSwapInvariant (annealedBAtScale P n)) (hMean : annealedSigmaStarInvKappaMeanAtScale P n = 0) : IsScalarMatrix (annealedSigmaAtScale P n)

noncomputable def HCPolySupport.Book.Ch04.Internal.annealedScalarizationWitnessOfInvariant {d : ℕ} [NeZero d] (P : RestrictionCoeffLaw d) (n : ℤ) (hSigmaFlip : IsSignFlipInvariant (annealedSigmaAtScale P n)) (hSigmaSwap : IsSwapInvariant (annealedSigmaAtScale P n)) (hSigmaStarFlip : IsSignFlipInvariant (annealedSigmaStarAtScale P n)) (hSigmaStarSwap : IsSwapInvariant (annealedSigmaStarAtScale P n)) (hKappa : annealedKappaAtScale P n = 0) : AnnealedScalarizationWitness P n

Build scalarization from invariant annealed \sigma, \sigma_*, and zero coupling.

Equations

• One or more equations did not get rendered due to their size.

theorem HCPolySupport.Book.Ch04.Internal.hasAnnealedScalarizationAtScale_of_invariant {d : ℕ} [NeZero d] (P : RestrictionCoeffLaw d) (n : ℤ) (hSigmaFlip : IsSignFlipInvariant (annealedSigmaAtScale P n)) (hSigmaSwap : IsSwapInvariant (annealedSigmaAtScale P n)) (hSigmaStarFlip : IsSignFlipInvariant (annealedSigmaStarAtScale P n)) (hSigmaStarSwap : IsSwapInvariant (annealedSigmaStarAtScale P n)) (hKappa : annealedKappaAtScale P n = 0) : HasAnnealedScalarizationAtScale P n

noncomputable def HCPolySupport.Book.Ch04.Internal.annealedScalarizationWitnessOfPrimitive {d : ℕ} [NeZero d] (P : RestrictionCoeffLaw d) (n : ℤ) (hSigmaStarInvFlip : IsSignFlipInvariant (annealedSigmaStarInvAtScale P n)) (hSigmaStarInvSwap : IsSwapInvariant (annealedSigmaStarInvAtScale P n)) (hBFlip : IsSignFlipInvariant (annealedBAtScale P n)) (hBSwap : IsSwapInvariant (annealedBAtScale P n)) (hMean : annealedSigmaStarInvKappaMeanAtScale P n = 0) : AnnealedScalarizationWitness P n

Build scalarization from primitive invariant data for b and \sigma_*^{-1}.

Equations

• One or more equations did not get rendered due to their size.

theorem HCPolySupport.Book.Ch04.Internal.hasAnnealedScalarizationAtScale_of_primitive {d : ℕ} [NeZero d] (P : RestrictionCoeffLaw d) (n : ℤ) (hSigmaStarInvFlip : IsSignFlipInvariant (annealedSigmaStarInvAtScale P n)) (hSigmaStarInvSwap : IsSwapInvariant (annealedSigmaStarInvAtScale P n)) (hBFlip : IsSignFlipInvariant (annealedBAtScale P n)) (hBSwap : IsSwapInvariant (annealedBAtScale P n)) (hMean : annealedSigmaStarInvKappaMeanAtScale P n = 0) : HasAnnealedScalarizationAtScale P n

noncomputable def HCPolySupport.Book.Ch04.Internal.AnnealedScalarizationInvarianceData.toWitness {d : ℕ} [NeZero d] {P : RestrictionCoeffLaw d} {n : ℤ} (h : AnnealedScalarizationInvarianceData P n) : AnnealedScalarizationWitness P n

A scalarization witness obtained from sign-flip and coordinate-swap invariance and vanishing annealed coupling.

Equations

• h.toWitness = HCPolySupport.Book.Ch04.Internal.annealedScalarizationWitnessOfInvariant P n ⋯ ⋯ ⋯ ⋯ ⋯

theorem HCPolySupport.Book.Ch04.Internal.AnnealedScalarizationInvarianceData.hasAnnealedScalarizationAtScale {d : ℕ} [NeZero d] {P : RestrictionCoeffLaw d} {n : ℤ} (h : AnnealedScalarizationInvarianceData P n) : HasAnnealedScalarizationAtScale P n

noncomputable def HCPolySupport.Book.Ch04.Internal.AnnealedScalarizationPrimitiveData.toWitness {d : ℕ} [NeZero d] {P : RestrictionCoeffLaw d} {n : ℤ} (h : AnnealedScalarizationPrimitiveData P n) : AnnealedScalarizationWitness P n

A scalarization witness obtained from invariance of the primitive inverse and energy matrices and vanishing mixed mean.

Equations

• h.toWitness = HCPolySupport.Book.Ch04.Internal.annealedScalarizationWitnessOfPrimitive P n ⋯ ⋯ ⋯ ⋯ ⋯

theorem HCPolySupport.Book.Ch04.Internal.AnnealedScalarizationPrimitiveData.hasAnnealedScalarizationAtScale {d : ℕ} [NeZero d] {P : RestrictionCoeffLaw d} {n : ℤ} (h : AnnealedScalarizationPrimitiveData P n) : HasAnnealedScalarizationAtScale P n