Lax Lean Archive

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

Table coordinates and private channel complements

Lax342547.TableSpaces · concepts/Lax342547/TableSpaces.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 table space contains the full channel blocks and the endpoint projections of the stored primal pins. Protected channels are projections of the pins, not intersections with the channel blocks.

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

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

    1 pin_le_table proven

    2 private_complement proven

    3 protected_rank proven

    4 table_dimension proven

    5 table_mono proven

    Lean source view on GitHub

    1import Lax342547.ProjectedPins
    2import Mathlib.LinearAlgebra.Basis.VectorSpace
    3import Mathlib.LinearAlgebra.Dimension.Constructions
    4
    5/-!
    6---
    7title: Table coordinates and private channel complements
    8type: lemma
    9---
    10The table space contains the full channel blocks and the endpoint
    11projections of the stored primal pins. Protected channels are projections
    12of the pins, not intersections with the channel blocks.
    13-/
    14
    15namespace Lax342547.TableSpaces
    16
    17open Lax342547.MomentSpace Lax342547.ExactPins Lax342547.ProjectedPins
    18
    19def primalEmbedding {B H : Type} (i : Fin 2) :
    20 (B → Binary) →ₗ[Binary] ((Fin 2 × (B ⊕ H)) → Binary) where
    21 toFun v x := if x.1 = i then Sum.elim v (fun _ => 0) x.2 else 0
    22 map_add' v w := by ext ⟨j, b | h⟩ <;> by_cases hj : j = i <;> simp [hj]
    23 map_smul' c v := by ext ⟨j, b | h⟩ <;> by_cases hj : j = i <;> simp [hj]
    24
    25def channelProjection {B H : Type} (i : Fin 2) :
    26 ((Fin 2 × (B ⊕ H)) → Binary) →ₗ[Binary] (H → Binary) where
    27 toFun v h := v (i, Sum.inr h)
    28 map_add' _ _ := rfl
    29 map_smul' _ _ := rfl
    30
    31def channelEmbedding {B H : Type} (i : Fin 2) :
    32 (H → Binary) →ₗ[Binary] ((Fin 2 × (B ⊕ H)) → Binary) where
    33 toFun v x := if x.1 = i then Sum.elim (fun _ => 0) v x.2 else 0
    34 map_add' v w := by ext ⟨j, b | h⟩ <;> by_cases hj : j = i <;> simp [hj]
    35 map_smul' c v := by ext ⟨j, b | h⟩ <;> by_cases hj : j = i <;> simp [hj]
    36
    37def protectedChannel {Comp B H N : Type}
    38 (P : Pin (Comp × Bool) (Fin 2 × (B ⊕ H)) N) (i : Fin 2) (a : Comp × Bool) :
    39 Submodule Binary (H → Binary) := (P.space a).map (channelProjection i)
    40
    41def tableSpace {Comp B H N : Type}
    42 (P : Pin (Comp × Bool) (Fin 2 × (B ⊕ H)) N) (a : Comp × Bool) :
    43 Submodule Binary ((Fin 2 × (B ⊕ H)) → Binary) where
    44 carrier := {v | ∀ i, primalProjection i v ∈ projected P i a}
    45 zero_mem' := fun i => (projected P i a).zero_mem
    46 add_mem' := fun hv hw i => (projected P i a).add_mem (hv i) (hw i)
    47 smul_mem' := fun c _ hv i => (projected P i a).smul_mem c (hv i)
    48
    49def pinnedPrimal {Comp B H N : Type}
    50 (P : Pin (Comp × Bool) (Fin 2 × (B ⊕ H)) N) (i : Fin 2) (a : Comp × Bool) :
    51 Submodule Binary (B → Binary) := (P.space a).comap (primalEmbedding i)
    52
    53axiom pin_le_table {Comp B H N : Type}
    54 (P : Pin (Comp × Bool) (Fin 2 × (B ⊕ H)) N) (a : Comp × Bool) :
    55 P.space a ≤ tableSpace P a
    56
    57axiom table_mono {Comp B H N : Type}
    58 (P Q : Pin (Comp × Bool) (Fin 2 × (B ⊕ H)) N) (h : P.Extends Q) (a : Comp × Bool) :
    59 tableSpace P a ≤ tableSpace Q a
    60
    61axiom protected_rank {Comp B H N : Type} [Fintype Comp] [Fintype B] [Fintype H]
    62 (P : Pin (Comp × Bool) (Fin 2 × (B ⊕ H)) N) (i : Fin 2) :
    63 (∑ a, Module.finrank Binary (protectedChannel P i a)) ≤ P.rank
    64
    65axiom private_complement {Comp B H N : Type}
    66 (P : Pin (Comp × Bool) (Fin 2 × (B ⊕ H)) N) (i : Fin 2) (a : Comp × Bool) :
    67 ∃ U : Submodule Binary (H → Binary), IsCompl (protectedChannel P i a) U
    68
    69axiom table_dimension {Comp B H N : Type} [Fintype Comp] [Fintype B] [Fintype H]
    70 (P : Pin (Comp × Bool) (Fin 2 × (B ⊕ H)) N) (a : Comp × Bool) :
    71 Module.finrank Binary (tableSpace P a) ≤ 2 * P.rank + 2 * Fintype.card H
    72
    73end Lax342547.TableSpaces
    74
    Show ProofShow ProofShow 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…