Canonical.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Small semantic steps used by the generated canonicalization traces. Each step preserves the actual averaged injective moment. The finite side conditions (state dimensions, permutation inverses, and zero entries) are checked separately.

theorem OAI.MUB6.Certificate.moment_delete_zero_row line 14

Source documentation

Move a zero row to the front and delete it.

theorem moment_delete_zero_row {p q : ℕ} (hp : p < 6) (H : CMatrix)
    (A : Matrix (Fin (p + 1)) (Fin q) ℤ) (σ : Equiv.Perm (Fin (p + 1)))
    (hzero : ∀ j, A (σ 0) j = 0) :
    injectiveMoment H A = injectiveMoment H (fun i j => A (σ i.succ) j) := by
…

Mentions: OAI.MUB6.CMatrix, OAI.MUB6.injectiveMoment

theorem OAI.MUB6.Certificate.moment_delete_zero_column line 26

Source documentation

The column version uses the transpose symmetry already present in the manuscript's normalization.

theorem moment_delete_zero_column {p q : ℕ} (hq : q < 6) (H : CMatrix)
    (A : Matrix (Fin p) (Fin (q + 1)) ℤ) (σ : Equiv.Perm (Fin (q + 1)))
    (hzero : ∀ i, A i (σ 0) = 0) :
    injectiveMoment H A = injectiveMoment H (fun i j => A i (σ j.succ)) := by
…

Mentions: OAI.MUB6.CMatrix, OAI.MUB6.injectiveMoment

theorem OAI.MUB6.Certificate.moment_permute line 39

Source documentation

Simultaneous row and column relabeling.

theorem moment_permute {p q : ℕ} (H : CMatrix)
    (A : Matrix (Fin p) (Fin q) ℤ)
    (σ : Equiv.Perm (Fin p)) (τ : Equiv.Perm (Fin q)) :
    injectiveMoment H A = injectiveMoment H (fun i j => A (σ i) (τ j)) := by
…

Mentions: OAI.MUB6.CMatrix, OAI.MUB6.injectiveMoment