IndisputableMonolith.Holography.LocalRecognitionHorizonCut

   1import IndisputableMonolith.Holography.HorizonOneSidedCut
   2import IndisputableMonolith.Holography.HorizonClockRate
   3import IndisputableMonolith.Holography.RecordMonotonicity
   4
   5/-!
   6# Local recognition horizon cuts
   7
   8This module joins three audited legs on one shared context:
   9
  10* LEG-A one-sided cut: `HorizonSumsPerSide` (MODEL) forces the horizon record to
  11  double-post the seam (`horizon_record_double_posts_seam`);
  12* posted-record heat: exterior projection of a closed `CutCfg` with discrete
  13  books balance / unit-temperature Clausius as THEOREMS about that record;
  14* LEG-B near-horizon rate: `NearHorizonRindlerForm` (MODEL, currently only
  15  `kappa > 0`) with the least positive deficit-free period as a THEOREM.
  16
  17A `LocalCut` is then a closed cut configuration living in that shared context.
  18Interior-private and rest-of-universe data are not visible in the exterior
  19record. No stress tensor, Ricci tensor, focusing law, curvature match, Unruh
  20claim, or Einstein equation occurs in this module.
  21-/
  22
  23namespace IndisputableMonolith
  24namespace Holography
  25namespace LocalRecognitionHorizonCut
  26
  27open HorizonOneSidedCut HorizonClockRate DeficitFreePeriod RecordMonotonicity
  28
  29/--
  30Shared local-horizon context joining the one-sided-cut MODEL, the posted-record
  31carrier dimensions, and the near-horizon rate MODEL. No thermality or curvature
  32premise is included.
  33-/
  34structure LocalHorizonContext (a s b r : ℕ) (kappa : ℝ) where
  35  horizonRecord : ℕ
  36  oneSided : HorizonSumsPerSide a s b r horizonRecord
  37  rindler : NearHorizonRindlerForm kappa
  38
  39/--
  40A globally closed one-sided cut configuration living in a shared local-horizon
  41context. Cut data are relative to the context; rate and one-sided premises live
  42on the context itself.
  43-/
  44structure LocalCut {a s b r : ℕ} {kappa : ℝ}
  45    (H : LocalHorizonContext a s b r kappa) where
  46  cfg : CutCfg a s b r
  47  closed : cutClosed cfg
  48
  49/-- Read a `ZMod 2` cut entry as its posted Boolean bit. -/
  50def bitReadout (x : ZMod 2) : Bool :=
  51  decide (x = 1)
  52
  53/--
  54The exterior-accessible record: exterior-private entries followed by seam
  55entries. Interior-private and rest-of-universe entries are traced out.
  56-/
  57def exteriorRecord {a s b r : ℕ} {kappa : ℝ}
  58    {H : LocalHorizonContext a s b r kappa}
  59    (c : LocalCut H) : List Bool :=
  60  List.ofFn (fun i : Fin a => bitReadout (c.cfg.1 i))
  61    ++ List.ofFn (fun j : Fin s => bitReadout (c.cfg.2.1 j))
  62
  63theorem exteriorRecord_length {a s b r : ℕ} {kappa : ℝ}
  64    {H : LocalHorizonContext a s b r kappa}
  65    (c : LocalCut H) :
  66    (exteriorRecord c).length = a + s := by
  67  simp [exteriorRecord]
  68
  69/-- Exterior posted-record potential in integer bit units. -/
  70def exteriorPotential {a s b r : ℕ} {kappa : ℝ}
  71    {H : LocalHorizonContext a s b r kappa}
  72    (c : LocalCut H) : ℤ :=
  73  recordWeight (exteriorRecord c)
  74
  75/--
  76One-step exterior heat in integer bit units. The physical identification of
  77this posted flux with horizon heat is the inherited posting-rule MODEL.
  78-/
  79def exteriorStepHeat {a s b r : ℕ} {kappa : ℝ}
  80    {H : LocalHorizonContext a s b r kappa}
  81    (c c' : LocalCut H) : ℤ :=
  82  recordFlux (exteriorRecord c) (exteriorRecord c')
  83
  84/-- Posted exterior heat is exactly the change of record potential. -/
  85theorem exteriorStepHeat_eq_potential {a s b r : ℕ} {kappa : ℝ}
  86    {H : LocalHorizonContext a s b r kappa}
  87    (c c' : LocalCut H) :
  88    exteriorStepHeat c c' = exteriorPotential c' - exteriorPotential c := by
  89  exact recordFlux_eq_weight_sub _ _ (by
  90    rw [exteriorRecord_length, exteriorRecord_length])
  91
  92/--
  93Unit-temperature discrete Clausius predicate on the local cut carrier. This is
  94record thermodynamics in bit units, not continuum Unruh thermality.
  95-/
  96def ExteriorClausius {a s b r : ℕ} {kappa : ℝ}
  97    {H : LocalHorizonContext a s b r kappa}
  98    (entropy : LocalCut H → ℤ) : Prop :=
  99  ∀ c c', exteriorStepHeat c c' = entropy c' - entropy c
 100
 101/-- The exterior record potential satisfies cut-level discrete Clausius. -/
 102theorem exterior_record_potential_clausius {a s b r : ℕ} {kappa : ℝ}
 103    {H : LocalHorizonContext a s b r kappa} :
 104    ExteriorClausius (exteriorPotential : LocalCut H → ℤ) :=
 105  exteriorStepHeat_eq_potential
 106
 107/-- Total posted exterior heat along a path of closed local cuts. -/
 108def exteriorPathHeat {a s b r : ℕ} {kappa : ℝ}
 109    {H : LocalHorizonContext a s b r kappa} :
 110    List (LocalCut H) → ℤ
 111  | [] => 0
 112  | [_] => 0
 113  | c :: c' :: rest => exteriorStepHeat c c' + exteriorPathHeat (c' :: rest)
 114
 115/-- The cut-level books balance along every finite local-horizon trajectory. -/
 116theorem exterior_books_balance {a s b r : ℕ} {kappa : ℝ}
 117    {H : LocalHorizonContext a s b r kappa}
 118    (c : LocalCut H)
 119    (p : List (LocalCut H)) :
 120    exteriorPathHeat (c :: p) =
 121      exteriorPotential (p.getLastD c) - exteriorPotential c := by
 122  induction p generalizing c with
 123  | nil => simp [exteriorPathHeat]
 124  | cons c' rest ih =>
 125      simp only [exteriorPathHeat, List.getLastD_cons,
 126        exteriorStepHeat_eq_potential, ih c']
 127      ring
 128
 129/--
 130Exterior heat ignores every change hidden behind the same exterior projection.
 131This is the exact one-sidedness statement used by the record bookkeeping.
 132-/
 133theorem exteriorStepHeat_zero_of_same_projection
 134    {a s b r : ℕ} {kappa : ℝ}
 135    {H : LocalHorizonContext a s b r kappa}
 136    (c c' : LocalCut H)
 137    (h : projA c.cfg = projA c'.cfg) :
 138    exteriorStepHeat c c' = 0 := by
 139  have hA : c.cfg.1 = c'.cfg.1 := by
 140    simpa [projA] using congrArg Prod.fst h
 141  have hS : c.cfg.2.1 = c'.cfg.2.1 := by
 142    simpa [projA] using congrArg Prod.snd h
 143  have hRecord : exteriorRecord c = exteriorRecord c' := by
 144    simp only [exteriorRecord]
 145    rw [hA, hS]
 146  unfold exteriorStepHeat
 147  rw [hRecord]
 148  exact recordFlux_self _
 149
 150/-- Every exterior and seam reading extends to a closed local cut in context `H`. -/
 151def ofExteriorReading {a s b r : ℕ} {kappa : ℝ}
 152    (H : LocalHorizonContext a s b r kappa)
 153    (gA : Fin a → ZMod 2) (gS : Fin s → ZMod 2) :
 154    LocalCut H where
 155  cfg := compA (b := b) (r := r) gA gS
 156  closed := compA_closed gA gS
 157
 158/--
 159Given the one-sided-cut MODEL on the shared context, the horizon record equals
 160the joint boundary marginal bit count plus the seam bit count.
 161-/
 162theorem horizonRecord_eq_joint_plus_seam {a s b r : ℕ} {kappa : ℝ}
 163    (H : LocalHorizonContext a s b r kappa) :
 164    H.horizonRecord =
 165      Nat.log2 (((closedSet a s b r).image projAB).card) + s :=
 166  horizon_record_double_posts_seam a s b r H.horizonRecord H.oneSided
 167
 168/--
 169Discrimination: when the seam is nonempty, the one-sided horizon record cannot
 170equal the joint boundary marginal. The seam double-post is load-bearing.
 171-/
 172theorem oneSided_horizonRecord_ne_joint_marginal {a s b r : ℕ} {kappa : ℝ}
 173    (H : LocalHorizonContext a s b r kappa)
 174    (hs : 0 < s) :
 175    H.horizonRecord ≠ Nat.log2 (((closedSet a s b r).image projAB).card) := by
 176  intro heq
 177  have h := horizonRecord_eq_joint_plus_seam H
 178  have hEq :
 179      Nat.log2 (((closedSet a s b r).image projAB).card) + s =
 180        Nat.log2 (((closedSet a s b r).image projAB).card) := by
 181    rw [← h, heq]
 182  have hs0 : s = 0 := Nat.add_eq_left.mp hEq
 183  exact (Nat.pos_iff_ne_zero.mp hs) hs0
 184
 185/-- The existing B3 rate theorem applies to every local recognition context. -/
 186theorem clockRateBundle {a s b r : ℕ} {kappa : ℝ}
 187    (H : LocalHorizonContext a s b r kappa) :
 188    ClockRateBundle kappa :=
 189  clockRateBundle_of_rindler H.rindler
 190
 191/--
 192The boost return period attached to a local-horizon context is the least
 193positive deficit-free period. This imports no KMS or entropy premise.
 194-/
 195theorem euclideanPeriod_isLeast_for_context {a s b r : ℕ} {kappa : ℝ}
 196    (H : LocalHorizonContext a s b r kappa) :
 197    IsLeast {T : ℝ | 0 < T ∧ deficitCost (kappa * T) = 0}
 198      (euclideanPeriod kappa) :=
 199  euclideanPeriod_isLeast kappa H.rindler.kappa_pos
 200
 201end LocalRecognitionHorizonCut
 202end Holography
 203end IndisputableMonolith
 204