Lax Lean Archive

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

Table contractions on effective profiles and their full extensions

Lax342547.TableContractions · concepts/Lax342547/TableContractions.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 starred contraction is a linear functional on the actual effective cut profiles. It uses both cross orientations of the table. Every full nominal cross form extending the whole table has that same contraction on effective profiles; admissibility alone is not asserted to suffice.

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

    Each proof establishes this claim relative to its assumptions.

    Lean source view on GitHub

    1import Lax342547.SmallTables
    2import Lax342547.TensorContractions
    3
    4/-!
    5---
    6title: Table contractions on effective profiles and their full extensions
    7type: lemma
    8---
    9The starred contraction is a linear functional on the actual effective
    10cut profiles. It uses both cross orientations of the table. Every full
    11nominal cross form extending the whole table has that same contraction
    12on effective profiles; admissibility alone is not asserted to suffice.
    13-/
    14
    15namespace Lax342547.TableContractions
    16
    17open Lax342547.MomentSpace Lax342547.ExactPins Lax342547.ProjectedPins
    18open Lax342547.TableSpaces Lax342547.SmallTables
    19
    20structure CrossForms (Comp B H : Type) where
    21 forward : Comp → LinearMap.BilinForm Binary ((Fin 2 × (B ⊕ H)) → Binary)
    22 reverse : Comp → LinearMap.BilinForm Binary ((Fin 2 × (B ⊕ H)) → Binary)
    23
    24def CrossForms.flip {Comp B H : Type} (F : CrossForms Comp B H) : CrossForms Comp B H :=
    25 ⟨F.reverse, F.forward⟩
    26
    27def flipTable {Comp B H N : Type} {P Q : Pin (Comp × Bool) (Fin 2 × (B ⊕ H)) N}
    28 (T : Table P Q) : Table Q P := ⟨T.reverse, T.forward⟩
    29
    30def Extends {Comp B H N : Type} {P Q : Pin (Comp × Bool) (Fin 2 × (B ⊕ H)) N}
    31 (F : CrossForms Comp B H) (T : Table P Q) : Prop :=
    32 (∀ e (v : tableSpace P (e, true)) (w : tableSpace Q (e, false)),
    33 F.forward e v.val w.val = T.forward e v w) ∧
    34 (∀ e (v : tableSpace Q (e, true)) (w : tableSpace P (e, false)),
    35 F.reverse e v.val w.val = T.reverse e v w)
    36
    37def primalToTable {Comp B H N : Type}
    38 (P : Pin (Comp × Bool) (Fin 2 × (B ⊕ H)) N) (a : Comp × Bool) (i : Fin 2) :
    39 projected P i a →ₗ[Binary] tableSpace P a where
    40 toFun v := ⟨primalEmbedding i v.val, by
    41 intro j
    42 by_cases hji : j = i
    43 · subst j
    44 simp [primalProjection, primalEmbedding]
    45 · have hz : primalProjection j (primalEmbedding (H := H) i v.val) = 0 := by
    46 ext b
    47 simp [primalProjection, primalEmbedding, hji]
    48 rw [hz]
    49 exact (projected P j a).zero_mem⟩
    50 map_add' v w := Subtype.ext ((primalEmbedding i).map_add v.val w.val)
    51 map_smul' c v := Subtype.ext ((primalEmbedding i).map_smul c v.val)
    52
    53noncomputable def plus {Comp B H N : Type} {P Q : Pin (Comp × Bool) (Fin 2 × (B ⊕ H)) N}
    54 (T : Table P Q) (e : Comp) (i z : Fin 2) : projected P i (e, true) →ₗ[Binary] (H → Binary) := by
    55 classical
    56 exact
    57 { toFun := fun v h => T.forward e (primalToTable P (e, true) i v)
    58 (tableChannel Q (e, false) z (Pi.single h 1))
    59 map_add' := by intro v w; ext h; simp
    60 map_smul' := by intro c v; ext h; simp }
    61
    62noncomputable def minus {Comp B H N : Type} {P Q : Pin (Comp × Bool) (Fin 2 × (B ⊕ H)) N}
    63 (T : Table P Q) (e : Comp) (i z : Fin 2) : projected P i (e, false) →ₗ[Binary] (H → Binary) := by
    64 classical
    65 exact
    66 { toFun := fun v h => T.reverse e (tableChannel Q (e, true) z (Pi.single h 1))
    67 (primalToTable P (e, false) i v)
    68 map_add' := by intro v w; ext h; simp
    69 map_smul' := by intro c v; ext h; simp }
    70
    71noncomputable def fullPlus {Comp B H : Type} (F : CrossForms Comp B H) (e : Comp) (i z : Fin 2) :
    72 (B → Binary) →ₗ[Binary] (H → Binary) := by
    73 classical
    74 exact
    75 { toFun := fun v h => F.forward e (primalEmbedding i v) (channelEmbedding z (Pi.single h 1))
    76 map_add' := by intro v w; ext h; simp
    77 map_smul' := by intro c v; ext h; simp }
    78
    79noncomputable def fullMinus {Comp B H : Type} (F : CrossForms Comp B H) (e : Comp) (i z : Fin 2) :
    80 (B → Binary) →ₗ[Binary] (H → Binary) := by
    81 classical
    82 exact
    83 { toFun := fun v h => F.reverse e (channelEmbedding z (Pi.single h 1)) (primalEmbedding i v)
    84 map_add' := by intro v w; ext h; simp
    85 map_smul' := by intro c v; ext h; simp }
    86
    87def component {Comp B H N : Type} (X : Submodule Binary (Comp → Matrix B B Binary))
    88 (P : Pin (Comp × Bool) (Fin 2 × (B ⊕ H)) N) (i : Fin 2) (e : Comp) :
    89 effective X P i →ₗ[Binary] tensorSpace (projected P i (e, true)) (projected P i (e, false)) where
    90 toFun x := ⟨x.val.val e, x.property e⟩
    91 map_add' _ _ := rfl
    92 map_smul' _ _ := rfl
    93
    94noncomputable def starContraction {Comp B H N : Type} [Fintype Comp] [Fintype B] [Fintype H]
    95 {P Q : Pin (Comp × Bool) (Fin 2 × (B ⊕ H)) N} (T : Table P Q)
    96 (X : Submodule Binary (Comp → Matrix B B Binary)) (i z : Fin 2) :
    97 effective X P i →ₗ[Binary] Binary :=
    98 ∑ e, (TensorContractions.contraction (plus T e i z) (minus T e i z)).comp (component X P i e)
    99
    100noncomputable def fullContraction {Comp B H : Type} [Fintype Comp] [Fintype B] [Fintype H]
    101 (F : CrossForms Comp B H) (X : Submodule Binary (Comp → Matrix B B Binary)) (i z : Fin 2) :
    102 X →ₗ[Binary] Binary :=
    103 ∑ e, (TensorContractions.ambient (fullPlus F e i z) (fullMinus F e i z)).comp
    104 ((LinearMap.proj e).comp X.subtype)
    105
    106axiom star_extension {Comp B H N : Type} [Fintype Comp] [Fintype B] [Fintype H]
    107 {P Q : Pin (Comp × Bool) (Fin 2 × (B ⊕ H)) N} (T : Table P Q)
    108 (F : CrossForms Comp B H) (hF : Extends F T)
    109 (X : Submodule Binary (Comp → Matrix B B Binary)) (i z : Fin 2) (x : effective X P i) :
    110 starContraction T X i z x = fullContraction F X i z x.val
    111
    112end Lax342547.TableContractions
    113
    Show 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…