OAI/RepresentationTheory/SignedTensor/Resolution.lean

GitHub source file

46 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CoordinateSweeps.SignedTensor.ActiveType line 38
  2. instance OAI.CoordinateSweeps.SignedTensor.(instance at line 41) line 41
  3. instance OAI.CoordinateSweeps.SignedTensor.(instance at line 45) line 45
  4. def OAI.CoordinateSweeps.SignedTensor.activeIrrep line 47
  5. def OAI.CoordinateSweeps.SignedTensor.activeProjector line 50
  6. lemma OAI.CoordinateSweeps.SignedTensor.activeProjector_nonzero line 54
  7. lemma OAI.CoordinateSweeps.SignedTensor.active_inequivalent line 57
  8. lemma OAI.CoordinateSweeps.SignedTensor.activeProjector_mul line 65
  9. lemma OAI.CoordinateSweeps.SignedTensor.activeProjector_independent line 73
  10. theorem OAI.CoordinateSweeps.SignedTensor.active_card_le line 87

    Source comment

    Number of actually occurring local types is polynomial even without a hook-support classification; this is exactly the term-count scale in06:eq20.
    theorem active_card_le (p l : ℕ) :
    Fintype.card (ActiveType p l) ≤ (l+1)^((2*p)*(2*p)) :=
…

    Mentions: OAI.CoordinateSweeps.SignedTensor.ActiveType

  11. theorem OAI.CoordinateSweeps.SignedTensor.active_resolution line 92

    Source comment

    Omitting zero type projections preserves the actual identity resolution.
    theorem active_resolution (p l : ℕ) :
    ∑ a : ActiveType p l, (activeProjector a).val=1 := by
…

    Mentions: OAI.CoordinateSweeps.a, OAI.CoordinateSweeps.SignedTensor.ActiveType, OAI.CoordinateSweeps.SignedTensor.activeProjector

  12. abbrev OAI.CoordinateSweeps.SignedTensor.BlockType line 112
  13. abbrev OAI.CoordinateSweeps.SignedTensor.blockProjector line 114
  14. lemma OAI.CoordinateSweeps.SignedTensor.block_resolution line 117

    Source comment

    Actual polynomial-size identity resolution of each product subgroup.
    lemma block_resolution : ∑ α : BlockType n p, blockProjector n α=1 := by
…

    Mentions: OAI.CoordinateSweeps.SignedTensor.BlockType, OAI.CoordinateSweeps.SignedTensor.blockProjector

  15. lemma OAI.CoordinateSweeps.SignedTensor.block_card_le line 127
  16. lemma OAI.CoordinateSweeps.SignedTensor.ambient_block_resolution line 140
  17. lemma OAI.CoordinateSweeps.SignedTensor.fiber_block_resolution line 147
  18. def OAI.CoordinateSweeps.SignedTensor.blockEntropy line 151
  19. lemma OAI.CoordinateSweeps.SignedTensor.exp_blockEntropy line 154
  20. lemma OAI.CoordinateSweeps.SignedTensor.nat_pow_eq_exp line 161
  21. lemma OAI.CoordinateSweeps.SignedTensor.block_card_real_le line 164
  22. lemma OAI.CoordinateSweeps.SignedTensor.actual_label_overlap_exp line 170
  23. lemma OAI.CoordinateSweeps.SignedTensor.actual_label_overlap_contract line 192
  24. theorem OAI.CoordinateSweeps.SignedTensor.labeled_projected_moment_bound line 217

    Source comment

    The actual two-product-subgroup inequality. Its only analytic inputs are child moments; the resolution, polynomial number of types and board overlap are all constructed above. This is the row/column step of the main induction.
    theorem labeled_projected_moment_bound {c : ℕ} [NeZero r]
    (f : L → Fin r) (g : L → Fin c) (hinj : Function.Injective (fun x => (f x,g x)))
    (e : Fin (Fintype.card L) ≃ L) (s : ℕ) (hp : 0 < p) (hps : p ≤ s)
    (hnR : ∀ i, size f i ≤ s) (hnC : ∀ j, size g j ≤ s)
    (ρ : UnitaryIrrep (Equiv.Perm (Fin (Fintype.card L)))) (q : ℕ) (hq : 0 < q)
    (c₀ ER EC : ℝ) (hc : 0 ≤ c₀) (hcq : c₀ ≤ q)
    (X Y : Matrix (Word p (Fintype.card L)) (Word p (Fintype.card L)) ℂ)
    (hR : ∀ α : BlockType (size f) p,
      (Matrix.trace (((fiberProjector f e (fun i => activeIrrep (α i))*X).conjTranspose*
        (fiberProjector f e (fun i => activeIrrep (α i))*X))^q)).re ≤ Real.exp (-c₀*blockEntropy α+ER))
    (hC : ∀ β : BlockType (size g) p,
      (Matrix.trace (((Y*fiberProjector g e (fun j => activeIrrep (β j))).conjTranspose*
…

    Mentions: OAI.CoordinateSweeps.c, OAI.CoordinateSweeps.e, OAI.CoordinateSweeps.UnitaryIrrep, OAI.CoordinateSweeps.SignedTensor.Word, OAI.CoordinateSweeps.SignedTensor.BlockType, OAI.CoordinateSweeps.SignedTensor.fiberProjector, OAI.CoordinateSweeps.SignedTensor.activeIrrep, OAI.CoordinateSweeps.SignedTensor.blockEntropy

  25. lemma OAI.CoordinateSweeps.SignedTensor.phase_eq_of_same_parity line 263
  26. lemma OAI.CoordinateSweeps.SignedTensor.wordPerm_same_parity line 270
  27. lemma OAI.CoordinateSweeps.SignedTensor.phase_conj_of_parity_stable line 276
  28. lemma OAI.CoordinateSweeps.SignedTensor.phase_of_fix_odd line 285
  29. lemma OAI.CoordinateSweeps.SignedTensor.phase_swap_odd line 296
  30. lemma OAI.CoordinateSweeps.SignedTensor.phase_ofSubtype line 317
  31. lemma OAI.CoordinateSweeps.SignedTensor.phase_of_fix_even line 330
  32. def OAI.CoordinateSweeps.YoungCorner.Hook line 354
  33. def OAI.CoordinateSweeps.YoungCorner.hookLetter line 356
  34. lemma OAI.CoordinateSweeps.YoungCorner.hookLetter_odd line 359
  35. lemma OAI.CoordinateSweeps.YoungCorner.hookLetter_row_eq line 365
  36. lemma OAI.CoordinateSweeps.YoungCorner.hookLetter_col_eq line 372
  37. lemma OAI.CoordinateSweeps.YoungCorner.hook_corner_fixed line 380

    Source comment

    The geometric reason all diagonal Young-corner coefficients have positive sign on the actual even-row/odd-column hook word.
    lemma hook_corner_fixed {X : Type*} (t : X ≃ Boxes μ) (h : Hook μ p)
    (r : colorStabilizer (rowColor t)) (c : colorStabilizer (colColor t))
    (hw : ∀ x, hookLetter h (t ((r : Equiv.Perm X) (c.val x)))=hookLetter h (t x)) :
    (∀ x, (t x).val.1<p → c.val x=x) ∧ (∀ x, p≤(t x).val.1 → r.val x=x) := by
…

    Mentions: OAI.CoordinateSweeps.YoungCorner.Boxes, OAI.CoordinateSweeps.YoungCorner.Hook, OAI.CoordinateSweeps.YoungCorner.colorStabilizer, OAI.CoordinateSweeps.YoungCorner.rowColor, OAI.CoordinateSweeps.c, OAI.CoordinateSweeps.YoungCorner.colColor, OAI.CoordinateSweeps.YoungCorner.hookLetter

  38. lemma OAI.CoordinateSweeps.YoungCorner.hook_corner_phase line 413
  39. lemma OAI.CoordinateSweeps.YoungCorner.signScalar_square line 444
  40. lemma OAI.CoordinateSweeps.YoungCorner.hook_contribution line 448
  41. lemma OAI.CoordinateSweeps.YoungCorner.hook_corner_matrix_ne line 463
  42. def OAI.CoordinateSweeps.YoungCorner.signedRep line 498

    Source comment

    The literal signed action, as a linear representation.
    def signedRep (p l : ℕ) : Representation ℂ (Equiv.Perm (Fin l)) (SignedTensor.Word p l → ℂ) :=
…

    Mentions: OAI.CoordinateSweeps.SignedTensor.Word

  43. lemma OAI.CoordinateSweeps.YoungCorner.signedRep_hasShape line 501
  44. lemma OAI.CoordinateSweeps.YoungCorner.detecting_shape_constituent line 511
  45. theorem OAI.CoordinateSweeps.YoungCorner.hook_occurs line 526

    Source comment

    Source05 hook occurrence, derived for actual irreps in the exact Koszul representation. No Pieri/Schur--Weyl or hook classification is assumed.
    theorem hook_occurs {V : Type} [AddCommGroup V] [Module ℂ V] [FiniteDimensional ℂ V]
    (ρ : Representation ℂ (Equiv.Perm (Fin l)) V) [ρ.IsIrreducible]
    (t : Fin l ≃ Boxes μ) (hρ : hasShape μ t ρ) (h : Hook μ p) :
    ∃ S : Subrepresentation (signedRep p l),
      Nonempty (Representation.Equiv ρ S.toRepresentation) := by
…

    Mentions: OAI.CoordinateSweeps.YoungCorner.Boxes, OAI.CoordinateSweeps.YoungCorner.hasShape, OAI.CoordinateSweeps.YoungCorner.Hook, OAI.CoordinateSweeps.YoungCorner.signedRep

  46. lemma OAI.CoordinateSweeps.YoungCorner.hook_multiplicity_pos line 539