Lax Lean Archive

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

Pure bilinear responses detect quotient tensors

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

    Vanishing against every bilinear form on two quotient spaces implies the component-rank bound used in §6. The selected affine-ray case gives exactly a scalar point moment, rather than an arbitrary low-rank block.

    Concept map
    11 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 pure_rank proven

    2 pure_sandwich proven

    3 selected_block proven

    Lean source view on GitHub

    1import Lax342547.QuotientRank
    2import Lax342547.SelectedMoments
    3import Lax342547.ConcreteGeometry
    4
    5/-!
    6---
    7title: Pure bilinear responses detect quotient tensors
    8type: lemma
    9---
    10Vanishing against every bilinear form on two quotient spaces implies the
    11component-rank bound used in §6. The selected affine-ray case gives
    12exactly a scalar point moment, rather than an arbitrary low-rank block.
    13-/
    14
    15namespace Lax342547.TensorAnnihilators
    16
    17open Lax342547.MomentSpace Lax342547.ConcreteGeometry
    18open Lax342547.BaseMoments Lax342547.SelectedMoments
    19
    20def dualCoordinates {I : Type} [DecidableEq I] :
    21 Module.Dual Binary (I → Binary) →ₗ[Binary] (I → Binary) where
    22 toFun φ i := φ (Pi.single i 1)
    23 map_add' _ _ := rfl
    24 map_smul' _ _ := rfl
    25
    26noncomputable def pureContraction {I : Type} [Fintype I]
    27 (S T : Submodule Binary (I → Binary))
    28 (β : ((I → Binary) ⧸ S) →ₗ[Binary] ((I → Binary) ⧸ T) →ₗ[Binary] Binary) :
    29 Matrix I I Binary →ₗ[Binary] Binary := by
    30 classical
    31 exact matrixPair (LinearMap.BilinForm.toMatrix' (β.compl₁₂ S.mkQ T.mkQ))
    32
    33def PureAnnihilates {I : Type} [Fintype I] (M : Matrix I I Binary)
    34 (S T : Submodule Binary (I → Binary)) : Prop :=
    35 ∀ β, pureContraction S T β M = 0
    36
    37axiom pure_rank {I : Type} [Fintype I] [DecidableEq I]
    38 (M : Matrix I I Binary) (S T : Submodule Binary (I → Binary))
    39 (h : PureAnnihilates M S T) :
    40 M.rank ≤ Module.finrank Binary S + Module.finrank Binary T
    41
    42axiom pure_sandwich {I P Q : Type} [Fintype I] [Fintype P] [Fintype Q]
    43 [DecidableEq I] (M : Matrix I I Binary) (S T : Submodule Binary (I → Binary))
    44 (h : PureAnnihilates M S T) (A : Matrix P I Binary) (B : Matrix Q I Binary)
    45 (hA : S ≤ LinearMap.ker A.mulVecLin) (hB : T ≤ LinearMap.ker B.mulVecLin) :
    46 A * M * B.transpose = 0
    47
    48axiom selected_block {Base : Type} [Fintype Base] [DecidableEq Base]
    49 (z : Base → Binary) (Z : Matrix (Option Base) (Option Base) Binary)
    50 (hZ : IsBaseMoment Z)
    51 (h : PureAnnihilates Z (Submodule.span Binary {baseEval z})
    52 (Submodule.span Binary {baseEval z})) :
    53 Z = Z none none • baseMoment z
    54
    55end Lax342547.TensorAnnihilators
    56
    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…