Lax Lean Archive

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

Positive pure-flavor mass for the actual synthetic parity slice Grams

Lax342547.SyntheticGramSlices · concepts/Lax342547/SyntheticGramSlices.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

    The ordered Gram for synthetic parity on q selected coordinates in each half is a sum of q active products. Routing these products into retained pure tester pairs proves its positive mass and the full slice variance bound with an explicit mass floor independent of n and the unit law.

    Concept map
    50 concepts
    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 uniteventsExact pure-flavor tester room and alaw-uniform Gram mass floorWalsh 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 pairingsPositive pure-flavor mass for the actualsynthetic parity slice GramsMajority intersections in the cyclic taggeometryPrescribed Gram products routed intodistinct retained tester pairsAdmissible pair lawsOrthogonality and finite Walsh correlationbounds
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A
    Evidence

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

    1 pure_slice_gram_mass proven

    2 pure_slice_variance proven

    3 slice_gram_products proven

    Lean source view on GitHub

    1import Lax342547.PureTesterRoom
    2import Lax342547.TesterProductRouting
    3
    4/-!
    5---
    6title: Positive pure-flavor mass for the actual synthetic parity slice Grams
    7type: lemma
    8---
    9The ordered Gram for synthetic parity on q selected coordinates in each
    10half is a sum of q active products. Routing these products into retained
    11pure tester pairs proves its positive mass and the full slice variance
    12bound with an explicit mass floor independent of n and the unit law.
    13-/
    14
    15namespace Lax342547.SyntheticGramSlices
    16noncomputable section
    17open Lax342547.MomentSpace Lax342547.TagGeometry Lax342547.Atoms
    18open Lax342547.FixedSelectorGram Lax342547.FlavorAffineSlices Lax342547.AffineSliceIndependence
    19open Lax342547.ConcreteGeometry Lax342547.RetainedImages Lax342547.RealCellLaws
    20open Lax342547.PureTesterRoom
    21open Lax342547.AffineSliceVariance Lax342547.RawFrames Lax342547.FrameTuples Lax342547.GramOrbitDensity
    22open scoped BigOperators ENNReal
    23set_option backward.isDefEq.respectTransparency false
    24
    25
    26def sliceGram {q m : ℕ} (R C : Fin q → Fin m) :
    27 Matrix (Option (Fin q ⊕ Fin q)) (Option (Fin q ⊕ Fin q)) Binary
    28 | some (Sum.inl i),some (Sum.inr j) => if R i = C j then 1 else 0
    29 | _,_ => 0
    30
    31def leftFactor (q : ℕ) (p : Fin q) : Option (Fin q ⊕ Fin q) → Binary
    32 | some (Sum.inl i) => if p = i then 1 else 0
    33 | _ => 0
    34
    35def rightFactor {q m : ℕ} (R C : Fin q → Fin m) (p : Fin q) :
    36 Option (Fin q ⊕ Fin q) → Binary
    37 | some (Sum.inr j) => if R p = C j then 1 else 0
    38 | _ => 0
    39
    40axiom slice_gram_products {q m : ℕ} (R C : Fin q → Fin m) :
    41 sliceGram R C = fun i j => ∑ p : Fin q,leftFactor q p i*rightFactor R C p j
    42
    43axiom pure_slice_gram_mass {k n b degree r q m : ℕ}
    44 (hr : 2*r ≤ n) (hd : 1 ≤ degree)
    45 (M : Fin b → Matrix (Fin n) (Fin n) Binary) (sel : Fin b → Binary)
    46 (l : Tag k) (T₀ : Finset (Tag k))
    47 (hroom : q ≤ k*(2*k+1-T₀.card)*r) (R C : Fin q → Fin m) :
    48 uniformFloor k r (Fin q ⊕ Fin q) ≤ cellMass
    49 (weights (PMF.uniformOfFintype (Coefficients n l (pureOutside T₀) (Fin q ⊕ Fin q))))
    50 (fun V => (pointColumns sel (value V)).transpose*selfGram hr hd M*pointColumns sel (value V) = sliceGram R C)
    51
    52
    53axiom pure_slice_variance {S H : Type} [Fintype S] [DecidableEq S]
    54 [Fintype H] {k n b degree r q m : ℕ}
    55 (l : Tag k) (T₀ : Finset (Tag k))
    56 (N : ℕ) (sel : Fin b → Binary)
    57 (hr : 2*r ≤ n) (hd : 1 ≤ degree)
    58 (M : Fin b → Matrix (Fin n) (Fin n) Binary) (R C : Fin q → Fin m)
    59 (hroom : q ≤ k*(2*k+1-T₀.card)*r)
    60 (E : S → Matrix (Coordinate k n b degree) (Coordinate k n b degree) Binary)
    61 (G : S → Matrix (Option (Fin q ⊕ Fin q)) (Option (Fin q ⊕ Fin q)) Binary)
    62 [∀ i,Nonempty (Frame (Coordinate k n b degree) H (Fin N) (E i))]
    63 [∀ i,Nonempty (Orbit (Fin N) (G i))]
    64 (hE : ∀ i,E i = selfGram hr hd M) (hG : ∀ i,G i = sliceGram R C)
    65 (test : (S → (Fin N × (Option (Fin q ⊕ Fin q) ⊕ Option (Fin q ⊕ Fin q)) → Binary)) → ℝ) (htest : ∀ z,|test z| ≤ 1)
    66 (hN : Fintype.card (Option (Fin q ⊕ Fin q))+Fintype.card (Option (Fin q ⊕ Fin q))+1 ≤ N)
    67 (hsmall : ((2 : ℝ)^(Fintype.card (Option (Fin q ⊕ Fin q))*Fintype.card (Option (Fin q ⊕ Fin q))+2))*
    68 ((2 : ℝ)^(Fintype.card (Option (Fin q ⊕ Fin q))*Fintype.card (Option (Fin q ⊕ Fin q))+2))/Real.sqrt ((2 : ℝ)^N) ≤
    69 1/(2 : ℝ)^(Fintype.card (Lax342547.CrossGramBasis.Slots (Option (Fin q ⊕ Fin q)) (Option (Fin q ⊕ Fin q)) (Option (Fin q ⊕ Fin q)) (Option (Fin q ⊕ Fin q)))+1)) :
    70 (∑ o : ∀ i,Frame (Coordinate k n b degree) H (Fin N) (E i),weights (PMF.uniformOfFintype _) o*
    71 ((∑ V : Coefficients n l (pureOutside T₀) (Fin q ⊕ Fin q),
    72 conditionalLaw (weights (PMF.uniformOfFintype _)) (fun V : Coefficients n l (pureOutside T₀) (Fin q ⊕ Fin q) => GramEvent sel E G (value V)) V*
    73 test (fun i => batchEquiv ((o i).P*pointColumns (k := k) (n := n) (b := b) (degree := degree) sel (value V),(o i).Q*pointColumns (k := k) (n := n) (b := b) (degree := degree) sel (value V))))-
    74 referenceMean N G test)^2) ≤
    75 (Fintype.card S : ℝ)*Lax342547.RawFrameComparison.errorBound N (Option (Fin q ⊕ Fin q)) (Option (Fin q ⊕ Fin q)) (Option (Fin q ⊕ Fin q)) (Option (Fin q ⊕ Fin q))+
    76 4*(((2 : ℝ)^(2*Fintype.card (Fin q ⊕ Fin q)+1)/(2 : ℝ)^n)/(uniformFloor k r (Fin q ⊕ Fin q))^2)
    77
    78
    79end
    80end Lax342547.SyntheticGramSlices
    81
    Show ProofShow ProofShow Proof
    Builds on
    Used by

    none

    From Mathlib

    none

    Discussion

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

    Loading discussion…