IndisputableMonolith.Masses.SectorPrimitive

   1import Mathlib
   2import IndisputableMonolith.Masses.Ribbons
   3
   4/-! model -- sector primitive placeholder.
   5Provides witness records for ribbon-based mass ladders; documentation only.
   6-/
   7
   8namespace IndisputableMonolith
   9namespace Masses
  10namespace SectorPrimitive
  11
  12structure Primitive where
  13  word : Ribbons.Word
  14  reduced : Ribbons.normalForm word = word
  15
  16@[simp] def deltaOf (gen : Ribbons.GenClass) (p : Primitive) : ℤ :=
  17  Ribbons.rungFrom gen p.word
  18
  19-- deltaOf is definitionally invariant (tautological; placeholder for rung-independence proof)
  20example (p : Primitive) (gen : Ribbons.GenClass) : deltaOf gen p = deltaOf gen p := rfl
  21
  22end SectorPrimitive
  23end Masses
  24end IndisputableMonolith
  25