IndisputableMonolith.Foundation.PreTemporalForcingOrder

   1import Mathlib
   2
   3/-!
   4# Pre-Temporal Forcing Order
   5
   6This module records the dependency order that exists "before time" in
   7Recognition Science. Since physical time is itself a forced object, the
   8ordering here is not chronological. It is a forcing order: `A` is before `B`
   9when `B` requires `A` as prior structure.
  10
  11The central distinction is between:
  12
  13* **recognition-light**: the primitive revealing act of distinction, prior to
  14  time and spacetime;
  15* **physical light**: the null-cone / photon / electromagnetic carrier,
  16  downstream of J-cost, ticks, and spacetime.
  17
  18So light is fundamental in two senses, but only the first sense is pre-temporal.
  19Physical light is the first boundary of spacetime, not the first item in the
  20forcing chain.
  21-/
  22
  23namespace IndisputableMonolith
  24namespace Foundation
  25namespace PreTemporalForcingOrder
  26
  27/-! ## Stages -/
  28
  29/-- The dependency stages in the pre-temporal forcing chain. -/
  30inductive Stage where
  31  | distinction
  32  | recognitionInterface
  33  | singleValuedPredicate
  34  | symmetricComparison
  35  | compositionConsistency
  36  | rcl
  37  | jCost
  38  | arithmeticObject
  39  | timeTick
  40  | spacetime
  41  | lightCone
  42  | photonEM
  43  | embodiedObserver
  44  deriving DecidableEq, Repr
  45
  46/-- A numerical rank for the forcing order. Lower rank means prior structure. -/
  47def rank : Stage → ℕ
  48  | .distinction => 0
  49  | .recognitionInterface => 1
  50  | .singleValuedPredicate => 2
  51  | .symmetricComparison => 3
  52  | .compositionConsistency => 4
  53  | .rcl => 5
  54  | .jCost => 6
  55  | .arithmeticObject => 7
  56  | .timeTick => 8
  57  | .spacetime => 9
  58  | .lightCone => 10
  59  | .photonEM => 11
  60  | .embodiedObserver => 12
  61
  62/-- Forcing priority: `a` is before `b` iff its dependency rank is smaller. -/
  63def Before (a b : Stage) : Prop := rank a < rank b
  64
  65instance (a b : Stage) : Decidable (Before a b) := Nat.decLt _ _
  66
  67/-! ## Main order theorems -/
  68
  69theorem distinction_first (s : Stage) (h : s ≠ Stage.distinction) :
  70    Before Stage.distinction s := by
  71  cases s <;> simp [Before, rank] at h ⊢
  72
  73theorem recognition_before_predicate :
  74    Before Stage.recognitionInterface Stage.singleValuedPredicate := by
  75  decide
  76
  77theorem predicate_before_symmetry :
  78    Before Stage.singleValuedPredicate Stage.symmetricComparison := by
  79  decide
  80
  81theorem symmetry_before_composition :
  82    Before Stage.symmetricComparison Stage.compositionConsistency := by
  83  decide
  84
  85theorem composition_before_rcl :
  86    Before Stage.compositionConsistency Stage.rcl := by
  87  decide
  88
  89theorem rcl_before_jCost :
  90    Before Stage.rcl Stage.jCost := by
  91  decide
  92
  93theorem jCost_before_arithmetic :
  94    Before Stage.jCost Stage.arithmeticObject := by
  95  decide
  96
  97theorem arithmetic_before_time :
  98    Before Stage.arithmeticObject Stage.timeTick := by
  99  decide
 100
 101theorem time_before_spacetime :
 102    Before Stage.timeTick Stage.spacetime := by
 103  decide
 104
 105theorem spacetime_before_lightCone :
 106    Before Stage.spacetime Stage.lightCone := by
 107  decide
 108
 109theorem lightCone_before_photonEM :
 110    Before Stage.lightCone Stage.photonEM := by
 111  decide
 112
 113theorem photonEM_before_embodiedObserver :
 114    Before Stage.photonEM Stage.embodiedObserver := by
 115  decide
 116
 117/-! ## Light: two senses -/
 118
 119/-- Recognition-light: the revealing act of an interface making distinction
 120available. This is pre-temporal. -/
 121def RecognitionLight : Stage := Stage.recognitionInterface
 122
 123/-- Physical light: the null boundary / electromagnetic carrier of spacetime. -/
 124def PhysicalLight : Stage := Stage.lightCone
 125
 126theorem recognition_light_before_time :
 127    Before RecognitionLight Stage.timeTick := by
 128  decide
 129
 130theorem recognition_light_before_spacetime :
 131    Before RecognitionLight Stage.spacetime := by
 132  decide
 133
 134theorem recognition_light_before_physical_light :
 135    Before RecognitionLight PhysicalLight := by
 136  decide
 137
 138theorem physical_light_after_spacetime :
 139    Before Stage.spacetime PhysicalLight := by
 140  decide
 141
 142/-- Physical light is not first in the forcing order. It requires spacetime. -/
 143theorem physical_light_not_first :
 144    ¬∀ s : Stage, s ≠ PhysicalLight → Before PhysicalLight s := by
 145  intro h
 146  have hbad := h Stage.distinction (by decide)
 147  norm_num [Before, PhysicalLight, rank] at hbad
 148
 149/-! ## Observer: two senses -/
 150
 151/-- Primitive observer-like structure: a recognizer/interface. This is forced
 152as soon as recognition, not merely bare abstract distinction, is in play. -/
 153def PrimitiveObserver : Stage := Stage.recognitionInterface
 154
 155/-- Embodied observer: a physical subsystem with finite resolution, downstream
 156of spacetime and physical light. -/
 157def PhysicalObserver : Stage := Stage.embodiedObserver
 158
 159theorem primitive_observer_before_time :
 160    Before PrimitiveObserver Stage.timeTick := by
 161  decide
 162
 163theorem primitive_observer_before_physical_light :
 164    Before PrimitiveObserver PhysicalLight := by
 165  decide
 166
 167theorem physical_observer_after_physical_light :
 168    Before PhysicalLight PhysicalObserver := by
 169  decide
 170
 171/-! ## Certificate -/
 172
 173structure PreTemporalOrderCert where
 174  recognition_light_pre_time : Before RecognitionLight Stage.timeTick
 175  recognition_light_pre_spacetime : Before RecognitionLight Stage.spacetime
 176  physical_light_post_spacetime : Before Stage.spacetime PhysicalLight
 177  light_cone_pre_photon : Before Stage.lightCone Stage.photonEM
 178  primitive_observer_pre_time : Before PrimitiveObserver Stage.timeTick
 179  physical_observer_post_light : Before PhysicalLight PhysicalObserver
 180
 181def cert : PreTemporalOrderCert where
 182  recognition_light_pre_time := recognition_light_before_time
 183  recognition_light_pre_spacetime := recognition_light_before_spacetime
 184  physical_light_post_spacetime := physical_light_after_spacetime
 185  light_cone_pre_photon := lightCone_before_photonEM
 186  primitive_observer_pre_time := primitive_observer_before_time
 187  physical_observer_post_light := physical_observer_after_physical_light
 188
 189theorem cert_inhabited : Nonempty PreTemporalOrderCert := ⟨cert⟩
 190
 191end PreTemporalForcingOrder
 192end Foundation
 193end IndisputableMonolith
 194