IndisputableMonolith.Physics.NullRecognitionMode

   1import Mathlib
   2import IndisputableMonolith.Cost
   3
   4/-!
   5# Null Recognition Mode
   6
   7The null recognition mode (NRM) is the upstream recognition-theoretic
   8object: the unique zero-cost propagating mode of the eight-tick recognition
   9cycle, up to ratio-gauge equivalence.
  10
  11This module deliberately does **not** call the mode a photon and does not
  12attach physical labels such as spin, polarization, or lightlike propagation.
  13Those belong in `Physics.PhotonAsZeroCostMode`.
  14-/
  15
  16namespace IndisputableMonolith
  17namespace Physics
  18namespace NullRecognitionMode
  19
  20open Cost
  21
  22noncomputable section
  23
  24/-! ## Propagating modes on the eight-tick cycle -/
  25
  26/-- A carrier event at one tick: a positive recognition ratio. -/
  27structure CarrierEvent where
  28  ratio : ℝ
  29  ratio_pos : 0 < ratio
  30
  31/-- A propagating recognition mode assigns a carrier event to each tick of
  32the eight-tick recognition cycle. -/
  33structure PropagatingMode where
  34  event : Fin 8 → CarrierEvent
  35
  36/-- Per-tick reciprocal recognition cost of a propagating mode. -/
  37def perTickCost (M : PropagatingMode) (i : Fin 8) : ℝ :=
  38  Jcost ((M.event i).ratio)
  39
  40/-- Total recognition cost across the eight-tick cycle. -/
  41def totalModeCost (M : PropagatingMode) : ℝ :=
  42  ∑ i : Fin 8, perTickCost M i
  43
  44/-- Gauge equivalence at the NRM level: two modes are equivalent if they
  45have the same recognition ratio at every tick. -/
  46def GaugeEquivalent (M N : PropagatingMode) : Prop :=
  47  ∀ i : Fin 8, (M.event i).ratio = (N.event i).ratio
  48
  49/-- The canonical null recognition mode: identity ratio at every tick. -/
  50def canonicalNRM : PropagatingMode where
  51  event := fun _ => ⟨1, by norm_num⟩
  52
  53/-- Backward-compatible short name for the canonical NRM. -/
  54abbrev zeroMode : PropagatingMode := canonicalNRM
  55
  56@[simp] theorem canonicalNRM_ratio (i : Fin 8) :
  57    (canonicalNRM.event i).ratio = 1 := rfl
  58
  59@[simp] theorem zeroMode_ratio (i : Fin 8) :
  60    (zeroMode.event i).ratio = 1 := rfl
  61
  62/-- The canonical NRM has zero per-tick recognition cost. -/
  63theorem canonicalNRM_perTickCost (i : Fin 8) :
  64    perTickCost canonicalNRM i = 0 := by
  65  simp [perTickCost]
  66  exact Jcost_unit0
  67
  68/-- The canonical NRM has total recognition cost zero. -/
  69theorem nrm_totalCost_zero : totalModeCost canonicalNRM = 0 := by
  70  unfold totalModeCost
  71  apply Finset.sum_eq_zero
  72  intro i _
  73  exact canonicalNRM_perTickCost i
  74
  75/-- Backward-compatible theorem name for the canonical zero-mode cost. -/
  76theorem zeroMode_totalCost : totalModeCost zeroMode = 0 :=
  77  nrm_totalCost_zero
  78
  79/-- A null recognition mode exists. -/
  80theorem nullRecognitionMode_nonempty :
  81    ∃ M : PropagatingMode, totalModeCost M = 0 :=
  82  ⟨canonicalNRM, nrm_totalCost_zero⟩
  83
  84/-- Backward-compatible existence theorem. -/
  85theorem zeroCostMode_nonempty :
  86    ∃ M : PropagatingMode, totalModeCost M = 0 :=
  87  nullRecognitionMode_nonempty
  88
  89/-! ## Uniqueness up to gauge -/
  90
  91/-- Per-tick costs are nonnegative. -/
  92theorem perTickCost_nonneg (M : PropagatingMode) (i : Fin 8) :
  93    0 ≤ perTickCost M i := by
  94  unfold perTickCost
  95  exact Jcost_nonneg ((M.event i).ratio_pos)
  96
  97/-- If total mode cost vanishes, then every per-tick cost vanishes. -/
  98theorem perTickCost_zero_of_total_zero
  99    (M : PropagatingMode) (h : totalModeCost M = 0) (i : Fin 8) :
 100    perTickCost M i = 0 := by
 101  have hsum : ∑ j : Fin 8, perTickCost M j = 0 := h
 102  have h_nonneg : ∀ j ∈ (Finset.univ : Finset (Fin 8)), 0 ≤ perTickCost M j := by
 103    intro j _
 104    exact perTickCost_nonneg M j
 105  have h_all := Finset.sum_eq_zero_iff_of_nonneg h_nonneg |>.mp hsum
 106  exact h_all i (Finset.mem_univ i)
 107
 108/-- If total mode cost vanishes, then every tick is at the identity ratio. -/
 109theorem ratio_eq_one_of_total_zero
 110    (M : PropagatingMode) (h : totalModeCost M = 0) (i : Fin 8) :
 111    (M.event i).ratio = 1 := by
 112  have hz := perTickCost_zero_of_total_zero M h i
 113  unfold perTickCost at hz
 114  exact (Jcost_eq_zero_iff (M.event i).ratio (M.event i).ratio_pos).mp hz
 115
 116/-- Any zero-cost propagating mode is gauge-equivalent to the canonical NRM. -/
 117theorem zeroCostMode_unique_up_to_gauge
 118    (M : PropagatingMode) (h : totalModeCost M = 0) :
 119    GaugeEquivalent M canonicalNRM := by
 120  intro i
 121  exact ratio_eq_one_of_total_zero M h i
 122
 123/-! ## Certificate -/
 124
 125structure NullRecognitionModeCert where
 126  exists_nrm : ∃ M : PropagatingMode, totalModeCost M = 0
 127  canonical_zero_cost : totalModeCost canonicalNRM = 0
 128  unique_up_to_gauge :
 129    ∀ M : PropagatingMode, totalModeCost M = 0 → GaugeEquivalent M canonicalNRM
 130
 131def nullRecognitionModeCert : NullRecognitionModeCert where
 132  exists_nrm := nullRecognitionMode_nonempty
 133  canonical_zero_cost := nrm_totalCost_zero
 134  unique_up_to_gauge := zeroCostMode_unique_up_to_gauge
 135
 136theorem nullRecognitionModeCert_inhabited :
 137    Nonempty NullRecognitionModeCert :=
 138  ⟨nullRecognitionModeCert⟩
 139
 140end
 141end NullRecognitionMode
 142end Physics
 143end IndisputableMonolith
 144