Lax Lean Archive

While this submission is a draft, it cannot be used by other submissions.

Uniform positive Gram mass from bounded tester prescriptions

Lax342547.FixedSelectorGram · concepts/Lax342547/FixedSelectorGram.lean · lax-342547

proven

Loading review…

Community review

Flags

Each flag is tied to a public ORCID identity and explains why this concept may be incorrect.

No flags have been submitted.

    Community review

    Flag this concept

    State precisely what appears incorrect. This explanation will be public under your ORCID name.

    No source line selected.

    Natural Language Statement

    Lemma

    At a fixed selector the sharp mixer contribution vanishes. Prescribing only retained tester pairs has mass independent of the growing free dimension. Routing across all retained tester pairs realizes every target slice Gram.

    Concept map
    47 concepts; 3 descendants hidden
    100%
    Exact-image bounds for independent affinecolumnsIndependent nominal affine slices from thefree blockConditioned affine-slice variance under theactual raw lawPoint atoms and finite flavor distributionsWalsh operator bounds with explicit bilinearrankConcrete cut-space testers and the orderedmixer formConcrete coordinates, quadratic testers, andthe self-Gram formActual conditioned affine coefficientdependence boundsExact finite conditioning of separated FouriertestsExact conditioning costs and recovery offinite probability massesEntropy progress for residual pair lawsQuantitative comparison after cross-batchGram conditioningIndependent characters of actual mutualGram entriesCut profiles and the constant kernelFinite empirical variance from atwo-coefficient comparisonEntropy along feasible mixture lines,including new supportFull feasible support and finite informationprojectionFinite linear images and their uniform-lawdensity boundsFinite independent sampling and vertexexception tailsUniform positive Gram mass from boundedtester prescriptionsAffine-slice comparison for every actual atomflavorFinite scalar agreement from binarycharacter boundsAmbient symmetries and frame marginalsUniform tuple images on prescribed GramorbitsThe symmetric binary gradient formGram-conditioned columns and theirrank-failure probabilityTwo-sided Gram normalization forindividually injective framesActual reference-batch laws for mutual GramtestsTwo-batch comparison across independentcomponent groupsThe binary hole relationExact joining of two prescribed Gram orbitsJoint-injectivity loss for two actual referencebatchesBoolean point moments with restricted basecoordinatesSquared restriction cost for independent uniteventsWalsh bounds for independent image lawsand separated phasesBounded tests under the actual two-batchGram lawActual raw frame observations with uniformtwo-batch decayRaw matrix frames and their tensorrealizationActual grouped raw observations witharbitrary common testsThe finite uniform raw-vertex lawOriginal retained-cell laws from finite PMFsFinite relative entropy and support costsImage caps inside original retained cellsBit rank and Walsh bounds for globalvector-slot pairingsMajority intersections in the cyclic taggeometryAdmissible pair lawsOrthogonality and finite Walsh correlationbounds
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A
    Evidence

    This concept declares 9 statements. Each proof establishes one of them relative to its assumptions.

    1 gram_cell_mass proven

    2 gram_mass_bound proven

    3 gram_restriction proven

    4 massFloor_pos proven

    5 positive_gram_mass proven

    6 prescription_mass proven

    7 restriction_uniform proven

    8 routed_gram proven

    9 same_selector_gram proven

    Lean source view on GitHub

    1import Lax342547.FlavorAffineSlices
    2
    3/-!
    4---
    5title: Uniform positive Gram mass from bounded tester prescriptions
    6type: lemma
    7---
    8At a fixed selector the sharp mixer contribution vanishes. Prescribing only
    9retained tester pairs has mass independent of the growing free dimension.
    10Routing across all retained tester pairs realizes every target slice Gram.
    11-/
    12
    13namespace Lax342547.FixedSelectorGram
    14noncomputable section
    15open Lax342547.MomentSpace Lax342547.TagGeometry Lax342547.ConcreteGeometry
    16open Lax342547.AffineSliceIndependence Lax342547.FlavorAffineSlices Lax342547.Atoms
    17open scoped BigOperators ENNReal
    18set_option backward.isDefEq.respectTransparency false
    19
    20abbrev TesterBlock (k : ℕ) := Option (Tag k × Tag k)
    21
    22def testerCoordinate {k n r : ℕ} (hr : 2*r ≤ n)
    23 (u : TesterBlock k × Fin r × Bool) : Base k n :=
    24 let i := if u.2.2 then pairRight hr u.2.1 else pairLeft hr u.2.1
    25 match u.1 with
    26 | none => shared i
    27 | some (d,t) => ordinary d t i
    28
    29def blockRetained {k : ℕ} (l : Tag k) (f : Flavor k) : TesterBlock k → Prop
    30 | none => match f with | .pure _ => False | _ => True
    31 | some (d,t) => l ∈ interval k d ∧ match f with
    32 | .generic => True | .sharedOnly => False | .pure blocks => (d,t) ∈ blocks
    33
    34abbrev Slots {k : ℕ} (l : Tag k) (f : Flavor k) (r : ℕ) :=
    35 {q : TesterBlock k // blockRetained l f q} × Fin r × Bool
    36
    37noncomputable instance {k : ℕ} (l : Tag k) (f : Flavor k) :
    38 Fintype {q : TesterBlock k // blockRetained l f q} := Fintype.ofFinite _
    39
    40noncomputable instance {k r : ℕ} (l : Tag k) (f : Flavor k) : Fintype (Slots l f r) :=
    41 Fintype.ofFinite _
    42
    43noncomputable instance {k r : ℕ} {D : Type} [Fintype D]
    44 (l : Tag k) (f : Flavor k) : Fintype (Matrix (Slots l f r) (Option D) Binary) := Fintype.ofFinite _
    45
    46def slotIndex {k n r : ℕ} (hr : 2*r ≤ n) (l : Tag k) (f : Flavor k)
    47 (u : Slots l f r) : {a : Base k n // a ∈ retained l f} :=
    48 ⟨testerCoordinate hr (u.1.val,u.2), (show testerCoordinate hr (u.1.val,u.2) ∈ retained (n := n) l f ↔ blockRetained l f u.1.val from by
    49 change retained l f (testerCoordinate hr (u.1.val,u.2)) ↔ _
    50 cases u.1.val with
    51 | none => cases f <;> simp [testerCoordinate,shared,retained,blockRetained]
    52 | some q => cases f <;> simp [testerCoordinate,ordinary,retained,blockRetained]).mpr u.1.property⟩
    53
    54def restrictTesters {k n r : ℕ} {D : Type} (hr : 2*r ≤ n) (l : Tag k) (f : Flavor k) :
    55 Coefficients n l f D →ₗ[Binary] Matrix (Slots l f r) (Option D) Binary where
    56 toFun V := fun u j => V (slotIndex hr l f u) j
    57 map_add' _ _ := rfl
    58 map_smul' _ _ := rfl
    59
    60def restrictedGram {k r : ℕ} {l : Tag k} {f : Flavor k} {D : Type}
    61 (X : Matrix (Slots l f r) (Option D) Binary) : Matrix (Option D) (Option D) Binary :=
    62 fun i j => ∑ q : {q : TesterBlock k // blockRetained l f q},∑ ρ : Fin r,
    63 X (q,ρ,false) i*X (q,ρ,true) j
    64
    65abbrev Pairs {k : ℕ} (l : Tag k) (f : Flavor k) (r : ℕ) :=
    66 {q : TesterBlock k // blockRetained l f q} × Fin r
    67
    68def routing {k r : ℕ} {l : Tag k} {f : Flavor k} {D : Type}
    69 (c : Option D → Pairs l f r) (G : Matrix (Option D) (Option D) Binary) :
    70 Matrix (Slots l f r) (Option D) Binary := by
    71 classical
    72 exact fun u j => if u.2.2 then Function.extend c (fun i => G i j) 0 (u.1,u.2.1)
    73 else if (u.1,u.2.1) = c j then 1 else 0
    74
    75def massFloor {k : ℕ} (l : Tag k) (f : Flavor k) (r : ℕ) (D : Type) [Fintype D] : ℝ :=
    76 1/(2 : ℝ)^(Fintype.card (Slots l f r)*Fintype.card (Option D))
    77
    78axiom same_selector_gram {k n b degree r : ℕ} {D : Type}
    79 (hr : 2*r ≤ n) (hd : 1 ≤ degree)
    80 (M : Fin b → Matrix (Fin n) (Fin n) Binary) (s : Fin b → Binary)
    81 (V W : Matrix (Base k n) (Option D) Binary) :
    82 (pointColumns s V).transpose*selfGram hr hd M*pointColumns s W =
    83 fun i j => (∑ d : Tag k,∑ t : Tag k,∑ ρ : Fin r,
    84 V (ordinary d t (pairLeft hr ρ)) i*W (ordinary d t (pairRight hr ρ)) j)+
    85 ∑ ρ : Fin r,V (shared (pairLeft hr ρ)) i*W (shared (pairRight hr ρ)) j
    86
    87axiom restriction_uniform {k n r : ℕ} {D : Type} [Fintype D]
    88 (hr : 2*r ≤ n) (l : Tag k) (f : Flavor k) :
    89 (PMF.uniformOfFintype (Coefficients n l f D)).map (restrictTesters hr l f) =
    90 PMF.uniformOfFintype (Matrix (Slots l f r) (Option D) Binary)
    91
    92axiom prescription_mass {k n r : ℕ} {D : Type} [Fintype D]
    93 (hr : 2*r ≤ n) (l : Tag k) (f : Flavor k)
    94 (X : Matrix (Slots l f r) (Option D) Binary) :
    95 (PMF.uniformOfFintype (Coefficients n l f D)).toOuterMeasure
    96 {V | restrictTesters hr l f V = X} =
    97 1/(2 : ℝ≥0∞)^(Fintype.card (Slots l f r)*Fintype.card (Option D))
    98
    99axiom gram_restriction {k n b degree r : ℕ} {D : Type}
    100 (hr : 2*r ≤ n) (hd : 1 ≤ degree)
    101 (M : Fin b → Matrix (Fin n) (Fin n) Binary) (s : Fin b → Binary)
    102 (l : Tag k) (f : Flavor k) (V : Coefficients n l f D) :
    103 (pointColumns s (value V)).transpose*selfGram hr hd M*pointColumns s (value V) =
    104 restrictedGram (restrictTesters hr l f V)
    105
    106axiom routed_gram {k r : ℕ} {l : Tag k} {f : Flavor k} {D : Type}
    107 [Fintype D]
    108 (c : Option D → Pairs l f r) (hc : Function.Injective c)
    109 (G : Matrix (Option D) (Option D) Binary) : restrictedGram (routing c G) = G
    110
    111axiom gram_mass_bound {k n b degree r : ℕ} {D : Type} [Fintype D]
    112 (hr : 2*r ≤ n) (hd : 1 ≤ degree)
    113 (M : Fin b → Matrix (Fin n) (Fin n) Binary) (s : Fin b → Binary)
    114 (l : Tag k) (f : Flavor k)
    115 (c : Option D → Pairs l f r) (hc : Function.Injective c)
    116 (G : Matrix (Option D) (Option D) Binary) :
    117 1/(2 : ℝ≥0∞)^(Fintype.card (Slots l f r)*Fintype.card (Option D)) ≤
    118 (PMF.uniformOfFintype (Coefficients n l f D)).toOuterMeasure
    119 {V | (pointColumns s (value V)).transpose*selfGram hr hd M*pointColumns s (value V) = G}
    120
    121axiom positive_gram_mass {k n b degree r : ℕ} {D : Type} [Fintype D]
    122 (hr : 2*r ≤ n) (hd : 1 ≤ degree)
    123 (M : Fin b → Matrix (Fin n) (Fin n) Binary) (s : Fin b → Binary)
    124 (l : Tag k) (f : Flavor k)
    125 (hroom : Fintype.card (Option D) ≤ Fintype.card (Pairs l f r))
    126 (G : Matrix (Option D) (Option D) Binary) :
    127 1/(2 : ℝ≥0∞)^(Fintype.card (Slots l f r)*Fintype.card (Option D)) ≤
    128 (PMF.uniformOfFintype (Coefficients n l f D)).toOuterMeasure
    129 {V | (pointColumns s (value V)).transpose*selfGram hr hd M*pointColumns s (value V) = G}
    130
    131axiom massFloor_pos {k : ℕ} (l : Tag k) (f : Flavor k) (r : ℕ) (D : Type) [Fintype D] :
    132 0 < massFloor l f r D
    133
    134axiom gram_cell_mass {k n b degree r : ℕ} {D : Type} [Fintype D]
    135 (hr : 2*r ≤ n) (hd : 1 ≤ degree)
    136 (M : Fin b → Matrix (Fin n) (Fin n) Binary) (s : Fin b → Binary)
    137 (l : Tag k) (f : Flavor k)
    138 (hroom : Fintype.card (Option D) ≤ Fintype.card (Pairs l f r))
    139 (G : Matrix (Option D) (Option D) Binary) :
    140 massFloor l f r D ≤ Lax342547.RetainedImages.cellMass
    141 (Lax342547.RealCellLaws.weights (PMF.uniformOfFintype (Coefficients n l f D)))
    142 (fun V => (pointColumns s (value V)).transpose*selfGram hr hd M*pointColumns s (value V) = G)
    143
    144end
    145end Lax342547.FixedSelectorGram
    146
    Show ProofShow ProofShow ProofShow ProofShow ProofShow ProofShow ProofShow ProofShow Proof
    Builds on
    Used by
    From Mathlib

    none

    Discussion

    Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

    Loading discussion…