Lax Lean Archive

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

Extracting fresh label coefficients through pin quotients

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

    Theorem

    The stronger sparse exclusion permits a selected coefficient to be read from the quotient by a projected pin. This is a first ingredient for isolating selected blocks in the §6 annihilator argument. The extractor also descends through selected key spans after quotienting its output by the corresponding base ray. Applying it to the actual label summands remains a separate step.

    Concept map
    13 concepts
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on ADescendants are omitted for concepts with more than 10 descendants.
    Evidence

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

    1 key_extractor proven

    2 pin_extractor proven

    3 quotient_factor proven

    Lean source view on GitHub

    1import Lax342547.PinLabelExclusions
    2import Mathlib.LinearAlgebra.Basis.VectorSpace
    3
    4/-!
    5---
    6title: Extracting fresh label coefficients through pin quotients
    7type: theorem
    8---
    9The stronger sparse exclusion permits a selected coefficient to be read
    10from the quotient by a projected pin. This is a first ingredient for
    11isolating selected blocks in the §6 annihilator argument. The extractor
    12also descends through selected key spans after quotienting its output
    13by the corresponding base ray. Applying it to the actual label summands
    14remains a separate step.
    15-/
    16
    17namespace Lax342547.QuotientExtractors
    18
    19open Lax342547.MomentSpace Lax342547.ExactPins Lax342547.ProjectedPins
    20open Lax342547.SparsePins Lax342547.PinLabelExclusions
    21
    22axiom quotient_factor {C V W : Type}
    23 [AddCommGroup C] [Module Binary C] [AddCommGroup V] [Module Binary V]
    24 [AddCommGroup W] [Module Binary W] (D : Submodule Binary V)
    25 (f : C →ₗ[Binary] V) (g : C →ₗ[Binary] W)
    26 (h : ∀ c, f c ∈ D → g c = 0) :
    27 ∃ q : (V ⧸ D) →ₗ[Binary] W, q.comp (D.mkQ.comp f) = g
    28
    29axiom pin_extractor {Base Comp H N : Type} {b degree R : ℕ}
    30 (P : Pin (Comp × Bool) (Fin 2 × ((SelectorCoordinates b degree × Option Base) ⊕ H)) N)
    31 (A : Fin 2 → Finset (Fin b → Binary)) (hA : Covers P A R)
    32 (i : Fin 2) (a : Comp × Bool) (L : Finset (Fin b → Binary))
    33 (hL : L.card ≤ R + 14) (s : Fin b → Binary) (hs : s ∈ L) (hfresh : s ∉ A i) :
    34 ∃ q : ((SelectorCoordinates b degree × Option Base → Binary) ⧸ projected P i a) →ₗ[Binary]
    35 (Option Base → Binary),
    36 ∀ t ∈ L, ∀ v : Option Base → Binary,
    37 q ((projected P i a).mkQ (labelTensor (selectorEval (degree := degree)) t v)) =
    38 if t = s then v else 0
    39
    40axiom key_extractor {Base Comp H N I : Type} {b degree R : ℕ}
    41 (P : Pin (Comp × Bool) (Fin 2 × ((SelectorCoordinates b degree × Option Base) ⊕ H)) N)
    42 (A : Fin 2 → Finset (Fin b → Binary)) (hA : Covers P A R)
    43 (i : Fin 2) (a : Comp × Bool) (L : Finset (Fin b → Binary))
    44 (hL : L.card ≤ R + 14) (s : Fin b → Binary) (hs : s ∈ L) (hfresh : s ∉ A i)
    45 (label : I → Fin b → Binary) (base : I → Option Base → Binary)
    46 (hlabels : ∀ j, label j ∈ L) (Ray : Submodule Binary (Option Base → Binary))
    47 (hmatch : ∀ j, label j = s → base j ∈ Ray) :
    48 ∃ q : ((SelectorCoordinates b degree × Option Base → Binary) ⧸
    49 (projected P i a ⊔ Submodule.span Binary
    50 (Set.range (fun j => labelTensor (selectorEval (degree := degree)) (label j) (base j))))) →ₗ[Binary]
    51 ((Option Base → Binary) ⧸ Ray),
    52 ∀ t ∈ L, ∀ v : Option Base → Binary,
    53 q (Submodule.Quotient.mk (labelTensor (selectorEval (degree := degree)) t v)) =
    54 if t = s then Ray.mkQ v else 0
    55
    56end Lax342547.QuotientExtractors
    57
    Show ProofShow ProofShow Proof
    Builds on
    Used by
    From Mathlib

    Discussion

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

    Loading discussion…