Lax Lean Archive

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

Primal blocks of the nominal spaces and their bounded table part

Lax342547.NominalPrimal · concepts/Lax342547/NominalPrimal.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 combined primal space has zero channel coordinates. Its intersection with a table space has dimension at most twice the total pin rank, while the table together with the primal space spans every nominal coordinate. A family of at most twenty-eight key directions costs at most twenty-eight more dimensions, independently of the ambient channel dimension.

    Concept map
    8 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_space_bound proven

    2 table_primal_dimension proven

    3 table_spans proven

    Lean source view on GitHub

    1import Lax342547.TableSpaces
    2import Lax342547.BaselineRank
    3
    4/-!
    5---
    6title: Primal blocks of the nominal spaces and their bounded table part
    7type: lemma
    8---
    9The combined primal space has zero channel coordinates. Its intersection
    10with a table space has dimension at most twice the total pin rank, while
    11the table together with the primal space spans every nominal coordinate.
    12A family of at most twenty-eight key directions costs at most twenty-eight
    13more dimensions, independently of the ambient channel dimension.
    14-/
    15
    16namespace Lax342547.NominalPrimal
    17
    18open Lax342547.MomentSpace Lax342547.ExactPins Lax342547.ProjectedPins Lax342547.TableSpaces
    19
    20variable {Comp B H N : Type}
    21
    22def primal : Submodule Binary ((Fin 2 × (B ⊕ H)) → Binary) where
    23 carrier := {v | ∀ i h, v (i, Sum.inr h) = 0}
    24 zero_mem' := by intro i h; rfl
    25 add_mem' := by intro v w hv hw i h; change v (i, Sum.inr h) + w (i, Sum.inr h) = 0; rw [hv, hw, add_zero]
    26 smul_mem' := by intro c v hv i h; change c * v (i, Sum.inr h) = 0; rw [hv, mul_zero]
    27
    28def keySpace {I : Type} (endpoint : I → Fin 2) (ray : I → B → Binary) :
    29 Submodule Binary ((Fin 2 × (B ⊕ H)) → Binary) :=
    30 Submodule.span Binary (Set.range (fun x => primalEmbedding (endpoint x) (ray x)))
    31
    32axiom table_spans (P : Pin (Comp × Bool) (Fin 2 × (B ⊕ H)) N) (a : Comp × Bool) :
    33 tableSpace P a ⊔ primal = ⊤
    34
    35axiom table_primal_dimension [Fintype Comp] [Fintype B] [Fintype H]
    36 (P : Pin (Comp × Bool) (Fin 2 × (B ⊕ H)) N) (a : Comp × Bool) :
    37 Module.finrank Binary ↥(tableSpace P a ⊓ primal) ≤ 2 * P.rank
    38
    39axiom key_space_bound {I : Type} [Fintype I] [Fintype B] [Fintype H]
    40 (endpoint : I → Fin 2) (ray : I → B → Binary) :
    41 keySpace (H := H) endpoint ray ≤ primal ∧
    42 Module.finrank Binary (keySpace (H := H) endpoint ray) ≤ Fintype.card I
    43
    44end Lax342547.NominalPrimal
    45
    Show 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…