OAI/RepresentationTheory/SignedTensor/Basic.lean

GitHub source file

70 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.CoordinateSweeps.SignedTensor.Letter line 15

   Source comment

   p even basis symbols followed by p odd ones, exactly E⊕O in05.

   abbrev Letter (p : ℕ) := Fin (2*p)

2. abbrev OAI.CoordinateSweeps.SignedTensor.Word line 16
3. def OAI.CoordinateSweeps.SignedTensor.odd line 18
4. def OAI.CoordinateSweeps.SignedTensor.koszulExponent line 22

   Source comment

   The sign from reordering the odd factors, with positions ordered as in ordinary tensor words. There is no choice of orientation hidden here.

   def koszulExponent {p l : ℕ} (σ : Equiv.Perm (Fin l)) (w : Word p l) : ℕ :=
   …

   Mentions: OAI.CoordinateSweeps.SignedTensor.Word

5. def OAI.CoordinateSweeps.SignedTensor.phase line 26
6. def OAI.CoordinateSweeps.SignedTensor.wordPerm line 30

   Source comment

   The underlying ordinary slot permutation; gh applies h first.

   def wordPerm {p l : ℕ} (σ : Equiv.Perm (Fin l)) : Equiv.Perm (Word p l) where
   …

   Mentions: OAI.CoordinateSweeps.SignedTensor.Word

7. def OAI.CoordinateSweeps.SignedTensor.matrix line 37

   Source comment

   Matrix of the exact parity-signed action in the tensor word basis.

   def matrix {p l : ℕ} (σ : Equiv.Perm (Fin l)) : Matrix (Word p l) (Word p l) ℂ :=
   …

   Mentions: OAI.CoordinateSweeps.SignedTensor.Word

8. lemma OAI.CoordinateSweeps.SignedTensor.phase_star_mul line 40
9. lemma OAI.CoordinateSweeps.SignedTensor.phase_prod line 46
10. lemma OAI.CoordinateSweeps.SignedTensor.wordPerm_mul line 52
11. theorem OAI.CoordinateSweeps.SignedTensor.phase_mul line 58

    Source comment

    The exact Koszul cocycle, proved from pair inversions, not an action axiom.

    theorem phase_mul {p l : ℕ} (σ τ : Equiv.Perm (Fin l)) (w : Word p l) :
        phase (σ*τ) w = phase σ (wordPerm τ w) * phase τ w := by
    …

    Mentions: OAI.CoordinateSweeps.SignedTensor.Word, OAI.CoordinateSweeps.SignedTensor.phase, OAI.CoordinateSweeps.SignedTensor.wordPerm

12. theorem OAI.CoordinateSweeps.SignedTensor.matrix_unitary line 96

    Source comment

    Unitarity follows directly, without assuming the Schur-Weyl or Pieri decomposition.

    theorem matrix_unitary {p l : ℕ} (σ : Equiv.Perm (Fin l)) :
        (matrix (p := p) σ).conjTranspose * matrix σ=1 := by
    …

    Mentions: OAI.CoordinateSweeps.SignedTensor.matrix

13. lemma OAI.CoordinateSweeps.SignedTensor.phase_one line 111
14. theorem OAI.CoordinateSweeps.SignedTensor.matrix_one line 118
15. theorem OAI.CoordinateSweeps.SignedTensor.matrix_mul line 122
16. def OAI.CoordinateSweeps.SignedTensor.action line 134

    Source comment

    Exact signed tensor representation of the symmetric group.

    def action (p l : ℕ) : Equiv.Perm (Fin l) →* Matrix (Word p l) (Word p l) ℂ where
    …

    Mentions: OAI.CoordinateSweeps.SignedTensor.Word

17. def OAI.CoordinateSweeps.SignedTensor.densityPower line 140

    Source comment

    Ordinary (not graded) tensor power of a one-site density, as in05.

    def densityPower {p : ℕ} (l : ℕ) (r : Matrix (Letter p) (Letter p) ℂ) :
        Matrix (Word p l) (Word p l) ℂ := fun u w => ∏ i, r (u i) (w i)

    Mentions: OAI.CoordinateSweeps.SignedTensor.Letter, OAI.CoordinateSweeps.SignedTensor.Word

18. lemma OAI.CoordinateSweeps.SignedTensor.densityPower_mul line 143
19. lemma OAI.CoordinateSweeps.SignedTensor.densityPower_star line 152
20. lemma OAI.CoordinateSweeps.SignedTensor.densityPower_trace line 157
21. lemma OAI.CoordinateSweeps.SignedTensor.densityPower_posSemidef line 163
22. def OAI.CoordinateSweeps.SignedTensor.EvenDensity line 170

    Source comment

    Even means positive trace-one and block diagonal for E,O, exactly as in05.

    def EvenDensity (p : ℕ) := {r : Matrix (Letter p) (Letter p) ℂ //
    …

    Mentions: OAI.CoordinateSweeps.SignedTensor.Letter

23. instance OAI.CoordinateSweeps.SignedTensor.(instance at line 174) line 174
24. lemma OAI.CoordinateSweeps.SignedTensor.phase_eq_of_parity line 177
25. lemma OAI.CoordinateSweeps.SignedTensor.densityPower_parity_of_ne_zero line 185
26. lemma OAI.CoordinateSweeps.SignedTensor.densityPower_permute line 196
27. theorem OAI.CoordinateSweeps.SignedTensor.densityPower_commute line 204

    Source comment

    Even densities commute with the signed action; omission of evenness here would be false. This is also the block-reordering claim at the end of05.

    theorem densityPower_commute {p l : ℕ} (r : EvenDensity p)
        (σ : Equiv.Perm (Fin l)) :
        matrix σ * densityPower l r.val=densityPower l r.val * matrix σ := by
    …

    Mentions: OAI.CoordinateSweeps.SignedTensor.EvenDensity, OAI.CoordinateSweeps.SignedTensor.matrix, OAI.CoordinateSweeps.SignedTensor.densityPower

28. lemma OAI.CoordinateSweeps.SignedTensor.evenDensityPower_trace line 230
29. def OAI.CoordinateSweeps.SignedTensor.isotypic line 236

    Source comment

    The standard central character formula for the isotypic projection. Its projection properties require the signed action laws (not assumed here).

    def isotypic {p l : ℕ} (ρ : UnitaryIrrep (Equiv.Perm (Fin l))) :
        Matrix (Word p l) (Word p l) ℂ :=
    …

    Mentions: OAI.CoordinateSweeps.UnitaryIrrep, OAI.CoordinateSweeps.SignedTensor.Word

30. def OAI.CoordinateSweeps.SignedTensor.Domination line 245

    Source comment

    Exact signed-density domination05 eq13, expressed for every irreducible (including absent ones whose projection is zero). The mixture is a genuine probability measure on the source's even density matrices, not an unproved positive operator supplied as a hypothesis.

    def Domination : Prop :=
    …

31. lemma OAI.CoordinateSweeps.SignedTensor.phase_ne_zero line 260
32. lemma OAI.CoordinateSweeps.SignedTensor.mul_signed_entry line 265
33. lemma OAI.CoordinateSweeps.SignedTensor.signed_mul_entry line 274
34. def OAI.CoordinateSweeps.SignedTensor.commutant line 287

    Source comment

    The actual signed-action commutant as a linear subspace of matrices.

    def commutant (p l : ℕ) : Submodule ℂ (Matrix (Word p l) (Word p l) ℂ) where
    …

    Mentions: OAI.CoordinateSweeps.SignedTensor.Word

35. lemma OAI.CoordinateSweeps.SignedTensor.commutant_zero_transport line 293
36. abbrev OAI.CoordinateSweeps.SignedTensor.Profile line 301
37. def OAI.CoordinateSweeps.SignedTensor.profile line 303
38. lemma OAI.CoordinateSweeps.SignedTensor.profile_fiber_card line 309
39. lemma OAI.CoordinateSweeps.SignedTensor.profile_eq_exists_perm line 315

    Source comment

    Two word pairs have the same histogram exactly when a position permutation carries one to the other. This supplies the finite orbit-counting parameter.

    lemma profile_eq_exists_perm {p l : ℕ} {u w u' w' : Word p l}
        (hh : profile u w=profile u' w') :
        ∃ σ : Equiv.Perm (Fin l), wordPerm σ u=u' ∧ wordPerm σ w=w' := by
    …

    Mentions: OAI.CoordinateSweeps.SignedTensor.Word, OAI.CoordinateSweeps.SignedTensor.profile, OAI.CoordinateSweeps.SignedTensor.wordPerm

40. abbrev OAI.CoordinateSweeps.SignedTensor.OccurringProfile line 333
41. def OAI.CoordinateSweeps.SignedTensor.profileRep line 336
42. lemma OAI.CoordinateSweeps.SignedTensor.profileRep_spec line 339
43. def OAI.CoordinateSweeps.SignedTensor.commutantEval line 342
44. lemma OAI.CoordinateSweeps.SignedTensor.commutantEval_injective line 347
45. theorem OAI.CoordinateSweeps.SignedTensor.commutant_finrank_le line 362

    Source comment

    Polynomial signed-commutant bound of exactly the O(p² log(s+1)) scale required by the main induction. No classification of partitions is used.

    theorem commutant_finrank_le (p l : ℕ) :
        Module.finrank ℂ (commutant p l) ≤ (l+1)^((2*p)*(2*p)) := by
    …

    Mentions: OAI.CoordinateSweeps.SignedTensor.commutant

46. lemma OAI.CoordinateSweeps.SignedTensor.matrix_inv line 375
47. abbrev OAI.CoordinateSweeps.SignedTensor.tensorRepresentation line 383
48. def OAI.CoordinateSweeps.SignedTensor.endomorphismMatrix line 387

    Source comment

    An actual intertwining endomorphism has its coefficient matrix in the signed commutant. This is not an assumed decomposition of the tensor action.

    def endomorphismMatrix (p l : ℕ) :
        (tensorRepresentation p l).IntertwiningMap (tensorRepresentation p l) →ₗ[ℂ]
          commutant p l where
    …

    Mentions: OAI.CoordinateSweeps.SignedTensor.tensorRepresentation, OAI.CoordinateSweeps.SignedTensor.commutant

49. lemma OAI.CoordinateSweeps.SignedTensor.endomorphismMatrix_injective line 402
50. theorem OAI.CoordinateSweeps.SignedTensor.tensor_endomorphisms_finrank_le line 408
51. theorem OAI.CoordinateSweeps.SignedTensor.multiplicity_le line 416

    Source comment

    The polynomial multiplicity clause of05 signed density lemma, proved without Young diagrams. Multiplicity is the actual space of equivariant embeddings.

    theorem multiplicity_le (p l : ℕ) (ρ : UnitaryIrrep (Equiv.Perm (Fin l))) :
        Module.finrank ℂ (ρ.asRepresentation.IntertwiningMap (tensorRepresentation p l)) ≤
          (l+1)^((2*p)*(2*p)) := by
    …

    Mentions: OAI.CoordinateSweeps.UnitaryIrrep, OAI.CoordinateSweeps.SignedTensor.tensorRepresentation

52. lemma OAI.CoordinateSweeps.SignedTensor.isotypic_eq_projector line 426
53. theorem OAI.CoordinateSweeps.SignedTensor.isotypic_posSemidef line 431
54. theorem OAI.CoordinateSweeps.SignedTensor.isotypic_trace line 436
55. lemma OAI.CoordinateSweeps.SignedTensor.swap01_inversion_iff line 461
56. lemma OAI.CoordinateSweeps.SignedTensor.phase_swap01 line 468
57. lemma OAI.CoordinateSweeps.SignedTensor.wordPerm_swap01_of_equal line 493
58. theorem OAI.CoordinateSweeps.SignedTensor.commutant_entry_zero_adjacent_mismatch line 501

    Source comment

    Two repeated, parity-mismatched pair symbols force a zero entry in every commuting matrix, hence in the canonical purification of an isotypic projector.

    theorem commutant_entry_zero_adjacent_mismatch {p n : ℕ} (A : commutant p (n+2))
        (u w : Word p (n+2)) (hu : u 0 = u 1) (hw : w 0 = w 1)
        (hm : odd (u 0) ↔ ¬ odd (w 0)) : A.val u w = 0 := by
    …

    Mentions: OAI.CoordinateSweeps.SignedTensor.commutant, OAI.CoordinateSweeps.SignedTensor.Word, OAI.CoordinateSweeps.SignedTensor.odd

59. lemma OAI.CoordinateSweeps.SignedTensor.exists_perm_pair line 521

    Source comment

    An explicit two-point transporter, avoiding any unproved transitivity principle or choice of ordering of the other positions.

    lemma exists_perm_pair {X : Type*} [DecidableEq X] (a b c d : X)
        (hab : a ≠ b) (hcd : c ≠ d) :
        ∃ g : Equiv.Perm X, g a = c ∧ g b = d := by
    …

    Mentions: OAI.CoordinateSweeps.a, OAI.CoordinateSweeps.c

60. theorem OAI.CoordinateSweeps.SignedTensor.commutant_entry_zero_repeated_mismatch line 538

    Source comment

    All repeated parity-mismatched pair symbols are impossible, at arbitrary positions. Distinct mismatched symbols will therefore account for every exceptional slot in the postselection argument.

    theorem commutant_entry_zero_repeated_mismatch {p l : ℕ} (A : commutant p l)
        (u w : Word p l) (i j : Fin l) (hij : i ≠ j) (hu : u i = u j) (hw : w i = w j)
        (hm : odd (u i) ↔ ¬ odd (w i)) : A.val u w = 0 := by
    …

    Mentions: OAI.CoordinateSweeps.SignedTensor.commutant, OAI.CoordinateSweeps.SignedTensor.Word, OAI.CoordinateSweeps.SignedTensor.odd

61. def OAI.CoordinateSweeps.SignedTensor.mismatchSlots line 567

    Source comment

    Exceptional slots of a vectorized commuting matrix.

    def mismatchSlots {p l : ℕ} (u w : Word p l) : Finset (Fin l) :=
    …

    Mentions: OAI.CoordinateSweeps.SignedTensor.Word

62. theorem OAI.CoordinateSweeps.SignedTensor.mismatchSlots_card_le line 572

    Source comment

    The exclusion bound needed for even-density postselection. The coarse constant four rather than two is harmless in the source's absolute Cp² error.

    theorem mismatchSlots_card_le {p l : ℕ} (A : commutant p l)
        (u w : Word p l) (hne : A.val u w ≠ 0) :
        (mismatchSlots u w).card ≤ (2*p)*(2*p) := by
    …

    Mentions: OAI.CoordinateSweeps.SignedTensor.commutant, OAI.CoordinateSweeps.SignedTensor.Word, OAI.CoordinateSweeps.SignedTensor.mismatchSlots

63. def OAI.CoordinateSweeps.SignedTensor.regroupPhase line 591

    Source comment

    The actual Koszul regrouping phase from (V⊗V̄)^⊗l to V^⊗l⊗V̄^⊗l. It will cancel, not be dropped, under partial trace.

    def regroupPhase {p l : ℕ} (u w : Word p l) : ℂ :=
    …

    Mentions: OAI.CoordinateSweeps.SignedTensor.Word

64. lemma OAI.CoordinateSweeps.SignedTensor.phase_square line 595
65. lemma OAI.CoordinateSweeps.SignedTensor.regroupPhase_square line 599
66. lemma OAI.CoordinateSweeps.SignedTensor.regroupPhase_star line 607
67. theorem OAI.CoordinateSweeps.SignedTensor.regroupPhase_permute line 617

    Source comment

    Permutations of the matched slots have no residual super-sign after literal Koszul regrouping; the positions of mismatched symbols are fixed.

    theorem regroupPhase_permute {p l : ℕ} (σ : Equiv.Perm (Fin l)) (u w : Word p l)
        (hfix : ∀ i, (odd (u i) ↔ ¬ odd (w i)) → σ i = i) :
        regroupPhase (wordPerm σ u) (wordPerm σ w) * phase σ u * phase σ w =
          regroupPhase u w := by
    …

    Mentions: OAI.CoordinateSweeps.SignedTensor.Word, OAI.CoordinateSweeps.SignedTensor.odd, OAI.CoordinateSweeps.SignedTensor.regroupPhase, OAI.CoordinateSweeps.SignedTensor.wordPerm, OAI.CoordinateSweeps.SignedTensor.phase

68. lemma OAI.CoordinateSweeps.SignedTensor.commutant_transport line 651
69. theorem OAI.CoordinateSweeps.SignedTensor.regrouped_commutant_invariant line 665

    Source comment

    Rephased purification components are ordinary symmetric on the free, matched-pair slots, a proved conclusion from the signed commutant relation.

    theorem regrouped_commutant_invariant {p l : ℕ} (A : commutant p l)
        (σ : Equiv.Perm (Fin l)) (u w : Word p l)
        (hfix : ∀ i, (odd (u i) ↔ ¬ odd (w i)) → σ i = i) :
        regroupPhase (wordPerm σ u) (wordPerm σ w) *
            A.val (wordPerm σ u) (wordPerm σ w) = regroupPhase u w * A.val u w := by
    …

    Mentions: OAI.CoordinateSweeps.SignedTensor.commutant, OAI.CoordinateSweeps.SignedTensor.Word, OAI.CoordinateSweeps.SignedTensor.odd, OAI.CoordinateSweeps.SignedTensor.regroupPhase, OAI.CoordinateSweeps.SignedTensor.wordPerm

70. lemma OAI.CoordinateSweeps.SignedTensor.regroupPhase_of_same_parity line 677

    Source comment

    Equal local parities in the system copies give equal regrouping signs. This is what justifies cancellation under the actual auxiliary partial trace.

    lemma regroupPhase_of_same_parity {p l : ℕ} (u u' w : Word p l)
        (h : ∀ i, odd (u i) ↔ odd (u' i)) : regroupPhase u w = regroupPhase u' w := by
    …

    Mentions: OAI.CoordinateSweeps.SignedTensor.Word, OAI.CoordinateSweeps.SignedTensor.odd, OAI.CoordinateSweeps.SignedTensor.regroupPhase