Lax Lean Archive

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

Numerical cross tables, injection flags, and unary admissibility

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

    A table records both cross orientations on the actual projected table spaces. Its injection quotients use the protected channel of the same sign as the pinned primal input, as in Definition 6.1. Admissibility on exact-pin events separates into two filters on individual orientations.

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

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

    1 admissible_iff_filters proven

    2 raw_admissible_iff_filters proven

    Lean source view on GitHub

    1import Lax342547.TableSpaces
    2import Lax342547.ReferencePins
    3
    4/-!
    5---
    6title: Numerical cross tables, injection flags, and unary admissibility
    7type: lemma
    8---
    9A table records both cross orientations on the actual projected table
    10spaces. Its injection quotients use the protected channel of the same
    11sign as the pinned primal input, as in Definition 6.1. Admissibility on
    12exact-pin events separates into two filters on individual orientations.
    13-/
    14
    15namespace Lax342547.SmallTables
    16
    17open Lax342547.MomentSpace Lax342547.ExactPins Lax342547.ProjectedPins Lax342547.TableSpaces
    18
    19variable {Comp B H N : Type}
    20
    21structure Table (P Q : Pin (Comp × Bool) (Fin 2 × (B ⊕ H)) N) where
    22 forward : ∀ e, tableSpace P (e, true) →ₗ[Binary] tableSpace Q (e, false) →ₗ[Binary] Binary
    23 reverse : ∀ e, tableSpace Q (e, true) →ₗ[Binary] tableSpace P (e, false) →ₗ[Binary] Binary
    24
    25def tableChannel (P : Pin (Comp × Bool) (Fin 2 × (B ⊕ H)) N) (a : Comp × Bool) (i : Fin 2) :
    26 (H → Binary) →ₗ[Binary] tableSpace P a where
    27 toFun v := ⟨channelEmbedding i v, by
    28 intro j
    29 have hz : primalProjection j (channelEmbedding (B := B) i v) = 0 := by
    30 ext b
    31 simp [primalProjection, channelEmbedding]
    32 rw [hz]
    33 exact (projected P j a).zero_mem⟩
    34 map_add' v w := Subtype.ext ((channelEmbedding i).map_add v w)
    35 map_smul' c v := Subtype.ext ((channelEmbedding i).map_smul c v)
    36
    37def tablePinnedPrimal (P : Pin (Comp × Bool) (Fin 2 × (B ⊕ H)) N)
    38 (a : Comp × Bool) (i : Fin 2) : pinnedPrimal P i a →ₗ[Binary] tableSpace P a where
    39 toFun v := ⟨primalEmbedding i v.val, fun _j => ⟨primalEmbedding i v.val, v.property, rfl⟩⟩
    40 map_add' v w := Subtype.ext ((primalEmbedding i).map_add v.val w.val)
    41 map_smul' c v := Subtype.ext ((primalEmbedding i).map_smul c v.val)
    42
    43noncomputable def rowChannels (P Q : Pin (Comp × Bool) (Fin 2 × (B ⊕ H)) N)
    44 (a b : Comp × Bool)
    45 (T : tableSpace P a →ₗ[Binary] tableSpace Q b →ₗ[Binary] Binary) (i z : Fin 2) :
    46 pinnedPrimal P i a →ₗ[Binary] (H → Binary) := by
    47 classical
    48 exact
    49 { toFun := fun d h => T (tablePinnedPrimal P a i d) (tableChannel Q b z (Pi.single h 1))
    50 map_add' := by intro d d'; ext h; simp
    51 map_smul' := by intro c d; ext h; simp }
    52
    53noncomputable def columnChannels (P Q : Pin (Comp × Bool) (Fin 2 × (B ⊕ H)) N)
    54 (a b : Comp × Bool)
    55 (T : tableSpace P a →ₗ[Binary] tableSpace Q b →ₗ[Binary] Binary) (z i : Fin 2) :
    56 pinnedPrimal Q i b →ₗ[Binary] (H → Binary) := by
    57 classical
    58 exact
    59 { toFun := fun d h => T (tableChannel P a z (Pi.single h 1)) (tablePinnedPrimal Q b i d)
    60 map_add' := by intro d d'; ext h; simp
    61 map_smul' := by intro c d; ext h; simp }
    62
    63def Injecting {P Q : Pin (Comp × Bool) (Fin 2 × (B ⊕ H)) N} (T : Table P Q) : Prop :=
    64 ∀ e i z,
    65 Function.Injective (((protectedChannel Q z (e, true)).mkQ).comp
    66 (rowChannels P Q (e, true) (e, false) (T.forward e) i z)) ∧
    67 Function.Injective (((protectedChannel Q z (e, false)).mkQ).comp
    68 (columnChannels Q P (e, true) (e, false) (T.reverse e) z i)) ∧
    69 Function.Injective (((protectedChannel P z (e, true)).mkQ).comp
    70 (rowChannels Q P (e, true) (e, false) (T.reverse e) i z)) ∧
    71 Function.Injective (((protectedChannel P z (e, false)).mkQ).comp
    72 (columnChannels P Q (e, true) (e, false) (T.forward e) z i))
    73
    74variable [Fintype N] {ΩA ΩB : Type}
    75
    76def Admissible {P Q : Pin (Comp × Bool) (Fin 2 × (B ⊕ H)) N} (T : Table P Q)
    77 (A : ΩA → (Comp × Bool) → ((Fin 2 × (B ⊕ H)) → Binary) →ₗ[Binary] (N → Binary))
    78 (Bmap : ΩB → (Comp × Bool) → ((Fin 2 × (B ⊕ H)) → Binary) →ₗ[Binary] (N → Binary))
    79 (oA : ΩA) (oB : ΩB) : Prop :=
    80 (∀ e (v : tableSpace P (e, true)) (w : tableSpace Q (e, false)),
    81 v.val ∈ P.space (e, true) ∨ w.val ∈ Q.space (e, false) →
    82 T.forward e v w = dotProduct (A oA (e, true) v.val) (Bmap oB (e, false) w.val)) ∧
    83 (∀ e (v : tableSpace Q (e, true)) (w : tableSpace P (e, false)),
    84 v.val ∈ Q.space (e, true) ∨ w.val ∈ P.space (e, false) →
    85 T.reverse e v w = dotProduct (Bmap oB (e, true) v.val) (A oA (e, false) w.val))
    86
    87def leftFilter {P Q : Pin (Comp × Bool) (Fin 2 × (B ⊕ H)) N} (T : Table P Q)
    88 (A : ΩA → (Comp × Bool) → ((Fin 2 × (B ⊕ H)) → Binary) →ₗ[Binary] (N → Binary)) : Set ΩA :=
    89 {oA | (∀ e (v : tableSpace P (e, true)) (w : tableSpace Q (e, false))
    90 (hw : w.val ∈ Q.space (e, false)),
    91 T.forward e v w = dotProduct (A oA (e, true) v.val) (Q.value (e, false) ⟨w.val, hw⟩)) ∧
    92 (∀ e (v : tableSpace Q (e, true)) (w : tableSpace P (e, false))
    93 (hv : v.val ∈ Q.space (e, true)),
    94 T.reverse e v w = dotProduct (Q.value (e, true) ⟨v.val, hv⟩) (A oA (e, false) w.val))}
    95
    96def rightFilter {P Q : Pin (Comp × Bool) (Fin 2 × (B ⊕ H)) N} (T : Table P Q)
    97 (Bmap : ΩB → (Comp × Bool) → ((Fin 2 × (B ⊕ H)) → Binary) →ₗ[Binary] (N → Binary)) : Set ΩB :=
    98 {oB | (∀ e (v : tableSpace P (e, true)) (w : tableSpace Q (e, false))
    99 (hv : v.val ∈ P.space (e, true)),
    100 T.forward e v w = dotProduct (P.value (e, true) ⟨v.val, hv⟩) (Bmap oB (e, false) w.val)) ∧
    101 (∀ e (v : tableSpace Q (e, true)) (w : tableSpace P (e, false))
    102 (hw : w.val ∈ P.space (e, false)),
    103 T.reverse e v w = dotProduct (Bmap oB (e, true) v.val) (P.value (e, false) ⟨w.val, hw⟩))}
    104
    105axiom admissible_iff_filters {P Q : Pin (Comp × Bool) (Fin 2 × (B ⊕ H)) N} (T : Table P Q)
    106 (A : ΩA → (Comp × Bool) → ((Fin 2 × (B ⊕ H)) → Binary) →ₗ[Binary] (N → Binary))
    107 (Bmap : ΩB → (Comp × Bool) → ((Fin 2 × (B ⊕ H)) → Binary) →ₗ[Binary] (N → Binary))
    108 (oA : ΩA) (oB : ΩB) (hA : oA ∈ P.event A) (hB : oB ∈ Q.event Bmap) :
    109 Admissible T A Bmap oA oB ↔ oA ∈ leftFilter T A ∧ oB ∈ rightFilter T Bmap
    110
    111axiom raw_admissible_iff_filters [Fintype B] [Fintype H] {E : Matrix B B Binary}
    112 {P Q : Pin (Comp × Bool) (Fin 2 × (B ⊕ H)) N} (T : Table P Q)
    113 (oA oB : Fin 2 → Comp → Lax342547.RawFrames.Frame B H N E)
    114 (hA : oA ∈ P.event Lax342547.ReferencePins.observation)
    115 (hB : oB ∈ Q.event Lax342547.ReferencePins.observation) :
    116 Admissible T Lax342547.ReferencePins.observation Lax342547.ReferencePins.observation oA oB ↔
    117 oA ∈ leftFilter T Lax342547.ReferencePins.observation ∧
    118 oB ∈ rightFilter T Lax342547.ReferencePins.observation
    119
    120end Lax342547.SmallTables
    121
    Show 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…