IndisputableMonolith.Holography.RecordMonotonicity

   1import Mathlib
   2import IndisputableMonolith.Holography.CellInjection
   3
   4/-!
   5# RecordMonotonicity: no free erasure ⇒ weak complementarity (on the forced cell)
   6
   7Step 3 of the entropy-fork development chain (panel `holo_unconditional_20260701`; step 1
   8was the cell-injection test `CellInjection.lean`, step 2 the Clausius selector
   9`ClausiusSelector.lean`; plan `plans/RS_Entropy_Fork_Development_Plan_20260701.html`).
  10The full holography manuscript (`holography/papers/Recognition_Holography_20260629.tex`) confesses
  11that recognition complementarity is its strongest premise and isolates the minimal
  12sufficient form: *weak complementarity* = an injection from physical bulk states into the
  13boundary letter space. This module derives that injection on the forced D=3 cell from
  14record accounting, replacing the monolithic complementarity premise with two strictly
  15weaker, independently falsifiable inputs.
  16
  17## The argument, and what carries which tag
  18
  191. **The ledger books balance (THEOREM).** Boundary heat is the posted record flux,
  20   channel by channel (the same posting rule as `ClausiusSelector.stepHeat`, here summed
  21   over the six face channels). The flux is EXACT against the record-weight potential:
  22   along any bulk trajectory, `pathHeat = Φ(end) − Φ(start)` (`books_balance`). So a
  23   posted bit can never be silently destroyed: an erasure (weight drop) is always exported
  24   as negative boundary heat (`erasure_exports_debit`), and a zero-heat step preserves the
  25   record weight exactly (`no_free_erasure`). This is the generalized-second-law
  26   bookkeeping — "no free erasure of the posted record" — proved, not assumed, for the
  27   posting rule itself.
  28
  292. **Gauge classes are exactly kernel cosets (THEOREM, `decide`).** Call two bulk
  30   configurations gauge-related when they carry the same boundary record (`gaugeRel`).
  31   This relation is exactly the coset structure of the 16-element record kernel isolated
  32   by the injection test: `gaugeRel c c' ↔ xorCfg c c' ∈ recordKernel`
  33   (`gauge_iff_kernel`). The only candidate violations of complementarity are the 16
  34   global parity moves — a named, finite, explicitly classified set.
  35
  363. **No posting-compatible protocol separates a gauge pair (THEOREM).** A dynamics `U`
  37   is *record-compatible* when it never manufactures a boundary distinction between two
  38   states whose difference was never posted; `recordCompatible_iff_no_free_record` shows
  39   this is literally the "no free record" condition — the difference-ledger form of the
  40   no-free-erasure discipline of (1), now imposed on dynamics. Any finite protocol built
  41   from record-compatible steps preserves gauge equivalence (`no_protocol_separates`), so
  42   gauge pairs are operationally inseparable (`gauge_never_separated`).
  43
  444. **Weak complementarity (THEOREM on the quotient; conditional operationally).**
  45   Quotient the cell by `gaugeRel`: the record readout descends to an INJECTION
  46   `physRecord : PhysState ↪ records` (`weak_complementarity`) — bulk physical states
  47   embed in the boundary record space, with 16 physical states = 16 posted records = 4
  48   posted bits against a 6-bit boundary capacity (`holographic_bound_of_weak_comp`).
  49   Operationally: for ANY notion of physical distinguishability that is witnessed by
  50   posting-compatible protocols (`KernelIsGauge dist`), record-equal states are
  51   physically indistinguishable (`weak_complementarity_of_gsl`).
  52
  53## What is input (honest tags, per `soul.mdc`)
  54
  55* INPUT (MODEL, inherited): boundary heat = posted record flux, one signed bit per face
  56  flip (the posting rule of `ClausiusSelector`, applied per channel).
  57* INPUT (HYPOTHESIS, named, falsifiable): `KernelIsGauge dist` — every physical
  58  distinguishing experiment factors through posting-compatible protocols. FALSIFIER
  59  (`kernelIsGauge_falsifier`): exhibit a physical process separating two record-equal
  60  configurations, i.e. a dynamics that creates a boundary distinction with no posted
  61  source. That would realize the manuscript's countermodel and break weak
  62  complementarity.
  63* DERIVED (THEOREM, axiom-clean): everything else — the balance law, the coset
  64  classification, protocol closure, the quotient injection, and the counting.
  65
  66Net effect on the manuscript: the single monolithic complementarity premise is replaced
  67by (a) the posting rule already carried by the Clausius selector, and (b) the
  68no-free-record condition on dynamics. The erasure half of the GSL is DISCHARGED (it is
  69the balance theorem); only the creation half remains a physical premise. This is
  70strictly weaker than what the manuscript assumed, which is the panel's step-3 target.
  71-/
  72
  73namespace IndisputableMonolith
  74namespace Holography
  75namespace RecordMonotonicity
  76
  77open CellInjection
  78
  79/- The `decide` proofs enumerate pairs over `Fin 256`; same budget rationale as
  80`CellInjection`: the kernel still checks every case. -/
  81set_option maxRecDepth 100000
  82set_option maxHeartbeats 4000000
  83
  84/-! ## 1. The ledger books balance: no free erasure is a THEOREM of the posting rule -/
  85
  86/-- **Per-channel posted flux** between two boundary records: the signed sum, over the
  87face channels, of one bit per record flip (`+1` up, `−1` down, `0` unchanged). This is
  88the six-channel form of `ClausiusSelector.stepHeat` — the same MODEL input (boundary
  89heat = posted ledger flux), applied per face. -/
  90def recordFlux (r r' : List Bool) : ℤ :=
  91  (List.zipWith (fun b b' => (if b' then (1 : ℤ) else 0) - (if b then 1 else 0)) r r').sum
  92
  93/-- **Record weight**: total posted bits of a boundary record (the record potential). -/
  94def recordWeight (r : List Bool) : ℤ :=
  95  (r.map (fun b => if b then (1 : ℤ) else 0)).sum
  96
  97/-- The flux is exact: between equal-length records it is the difference of the record
  98weights. Nothing is created or destroyed off the books. -/
  99theorem recordFlux_eq_weight_sub (r : List Bool) :
 100    ∀ r' : List Bool, r.length = r'.length →
 101      recordFlux r r' = recordWeight r' - recordWeight r := by
 102  induction r with
 103  | nil =>
 104    intro r' h
 105    cases r' with
 106    | nil => simp [recordFlux, recordWeight]
 107    | cons b' t' => simp at h
 108  | cons b t ih =>
 109    intro r' h
 110    cases r' with
 111    | nil => simp at h
 112    | cons b' t' =>
 113      have ht : t.length = t'.length := by simpa using h
 114      have hrec := ih t' ht
 115      simp only [recordFlux, recordWeight, List.zipWith_cons_cons, List.map_cons,
 116        List.sum_cons] at hrec ⊢
 117      rw [hrec]
 118      ring
 119
 120/-- A record posts zero flux against itself. -/
 121theorem recordFlux_self (r : List Bool) : recordFlux r r = 0 := by
 122  rw [recordFlux_eq_weight_sub r r rfl]
 123  ring
 124
 125/-- The record potential of a cell configuration: posted bits on its six faces. -/
 126def cellPotential (c : CellCfg) : ℤ := recordWeight (faceRecord c)
 127
 128/-- Boundary heat of one bulk step: the posted flux across the six face channels. -/
 129def stepHeatCell (c c' : CellCfg) : ℤ := recordFlux (faceRecord c) (faceRecord c')
 130
 131theorem faceRecord_length (c : CellCfg) : (faceRecord c).length = 6 := rfl
 132
 133/-- One bulk step posts exactly the change of the record potential: `δQ = ΔΦ`. -/
 134theorem stepHeatCell_eq_potential (c c' : CellCfg) :
 135    stepHeatCell c c' = cellPotential c' - cellPotential c :=
 136  recordFlux_eq_weight_sub _ _ (by rw [faceRecord_length, faceRecord_length])
 137
 138/-- Total boundary heat along a bulk trajectory (step-by-step posted flux). -/
 139def pathHeatCell : List CellCfg → ℤ
 140  | [] => 0
 141  | [_] => 0
 142  | c :: c' :: rest => stepHeatCell c c' + pathHeatCell (c' :: rest)
 143
 144/-- **The books balance (the GSL's erasure half, as a THEOREM).** Along any bulk
 145trajectory the total posted heat equals the change of the record potential. A record bit
 146can therefore never disappear silently: every erasure along the way is exported to the
 147boundary as negative heat, every posting imported as positive heat. -/
 148theorem books_balance (c : CellCfg) (p : List CellCfg) :
 149    pathHeatCell (c :: p) = cellPotential (p.getLastD c) - cellPotential c := by
 150  induction p generalizing c with
 151  | nil => simp [pathHeatCell]
 152  | cons c' rest ih =>
 153    simp only [pathHeatCell, List.getLastD_cons, stepHeatCell_eq_potential, ih c']
 154    ring
 155
 156/-- **No free erasure, step form.** A step that posts nothing preserves the record
 157weight exactly; erasing a posted bit without exporting the debit is impossible under the
 158posting rule. -/
 159theorem no_free_erasure (c c' : CellCfg) (h : stepHeatCell c c' = 0) :
 160    cellPotential c' = cellPotential c := by
 161  have hb := stepHeatCell_eq_potential c c'
 162  omega
 163
 164/-- Erasure exports the debit: any weight decrease shows up as strictly negative
 165boundary heat (double entry — the debit lands at the boundary, it is not destroyed). -/
 166theorem erasure_exports_debit (c c' : CellCfg) (h : cellPotential c' < cellPotential c) :
 167    stepHeatCell c c' < 0 := by
 168  rw [stepHeatCell_eq_potential]
 169  omega
 170
 171/-- **Record monotonicity** (the GSL predicate on trajectories): the record potential
 172never decreases along the path. -/
 173def RecordMonotone (p : List CellCfg) : Prop :=
 174  List.IsChain (fun c c' => cellPotential c ≤ cellPotential c') p
 175
 176/-- A closed-system trajectory — one that exports no heat at any step — is
 177record-monotone. (With the balance theorem: the GSL for the posted record is bookkeeping,
 178not an extra law.) -/
 179theorem recordMonotone_of_no_export (p : List CellCfg)
 180    (h : List.IsChain (fun c c' => 0 ≤ stepHeatCell c c') p) : RecordMonotone p := by
 181  refine List.IsChain.imp ?_ h
 182  intro c c' hcc
 183  have hb := stepHeatCell_eq_potential c c'
 184  omega
 185
 186/-! ## 2. Gauge classes are exactly the kernel cosets -/
 187
 188/-- **Gauge relation**: two bulk configurations carry the same boundary record. The
 189candidate "physically identical" relation of the fork selector (an unposted difference is
 190not a performed distinction). -/
 191def gaugeRel (c c' : CellCfg) : Prop := faceRecord c = faceRecord c'
 192
 193instance : DecidableRel gaugeRel :=
 194  fun c c' => inferInstanceAs (Decidable (faceRecord c = faceRecord c'))
 195
 196theorem gaugeRel_equivalence : Equivalence gaugeRel :=
 197  ⟨fun _ => rfl, Eq.symm, Eq.trans⟩
 198
 199/-- Gauge motion is heat-free: a gauge step posts nothing on any channel. -/
 200theorem gauge_step_zero_heat (c c' : CellCfg) (h : gaugeRel c c') :
 201    stepHeatCell c c' = 0 := by
 202  have h' : faceRecord c = faceRecord c' := h
 203  unfold stepHeatCell
 204  rw [h']
 205  exact recordFlux_self _
 206
 207/-- Silent moves are exactly the kernel (re-export of the injection test's
 208classification). -/
 209theorem silent_iff_kernel (d : CellCfg) :
 210    (∀ c : CellCfg, faceRecord (xorCfg c d) = faceRecord c) ↔ d ∈ recordKernel :=
 211  invisible_iff_kernel d
 212
 213theorem mem_recordKernel_iff (d : CellCfg) :
 214    d ∈ recordKernel ↔ faceRecord d = faceRecord cell0 := by
 215  simp [recordKernel]
 216
 217/-- Gauge relation, kernel-predicate form (checked over all 65 536 pairs). -/
 218theorem gauge_iff_kernel_record :
 219    ∀ c c' : CellCfg, gaugeRel c c' ↔ faceRecord (xorCfg c c') = faceRecord cell0 := by
 220  decide
 221
 222/-- **Gauge classes = kernel cosets.** Two configurations are gauge-related iff their
 223difference lies in the 16-element record kernel of `CellInjection`. The entire candidate
 224failure of complementarity is the coset structure of one named finite group. -/
 225theorem gauge_iff_kernel (c c' : CellCfg) :
 226    gaugeRel c c' ↔ xorCfg c c' ∈ recordKernel := by
 227  rw [mem_recordKernel_iff]
 228  exact gauge_iff_kernel_record c c'
 229
 230/-! ## 3. No posting-compatible protocol separates a gauge pair -/
 231
 232/-- A bulk dynamics is **record-compatible** when it never turns an unposted difference
 233into a posted one: gauge-related inputs go to gauge-related outputs. -/
 234def RecordCompatible (U : CellCfg → CellCfg) : Prop :=
 235  ∀ c c', gaugeRel c c' → gaugeRel (U c) (U c')
 236
 237/-- A dynamics **creates a free record** when some gauge pair (identical posted data,
 238zero-heat difference channel) is driven to distinct boundary records — a boundary
 239distinction with no posted source. -/
 240def CreatesFreeRecord (U : CellCfg → CellCfg) : Prop :=
 241  ∃ c c', gaugeRel c c' ∧ ¬ gaugeRel (U c) (U c')
 242
 243/-- Record compatibility IS the no-free-record condition: the GSL discipline of Part 1
 244(nothing enters or leaves the books unposted), imposed on dynamics. -/
 245theorem recordCompatible_iff_no_free_record (U : CellCfg → CellCfg) :
 246    RecordCompatible U ↔ ¬ CreatesFreeRecord U := by
 247  constructor
 248  · rintro hU ⟨c, c', hcc, hne⟩
 249    exact hne (hU c c' hcc)
 250  · intro h c c' hcc
 251    by_contra hne
 252    exact h ⟨c, c', hcc, hne⟩
 253
 254/-- Run a finite protocol (a list of bulk evolution steps) on a configuration. -/
 255def runProtocol (Us : List (CellCfg → CellCfg)) (c : CellCfg) : CellCfg :=
 256  Us.foldl (fun x U => U x) c
 257
 258/-- **Protocol closure.** Any finite protocol whose every step is record-compatible
 259preserves gauge equivalence: it cannot separate states whose difference was never
 260posted. -/
 261theorem no_protocol_separates (Us : List (CellCfg → CellCfg))
 262    (hUs : ∀ U ∈ Us, RecordCompatible U) :
 263    ∀ c c', gaugeRel c c' → gaugeRel (runProtocol Us c) (runProtocol Us c') := by
 264  induction Us with
 265  | nil => intro c c' h; exact h
 266  | cons U rest ih =>
 267    intro c c' h
 268    have h1 : gaugeRel (U c) (U c') := hUs U List.mem_cons_self c c' h
 269    have h2 := ih (fun V hV => hUs V (List.mem_cons_of_mem U hV)) (U c) (U c') h1
 270    simpa [runProtocol, List.foldl_cons] using h2
 271
 272/-- Two configurations are **operationally separated** when some posting-compatible
 273protocol drives them to distinct boundary records. -/
 274def Separated (c c' : CellCfg) : Prop :=
 275  ∃ Us : List (CellCfg → CellCfg), (∀ U ∈ Us, RecordCompatible U) ∧
 276    ¬ gaugeRel (runProtocol Us c) (runProtocol Us c')
 277
 278/-- **Gauge pairs are operationally inseparable** by posting-compatible protocols. -/
 279theorem gauge_never_separated (c c' : CellCfg) (h : gaugeRel c c') : ¬ Separated c c' := by
 280  rintro ⟨Us, hUs, hne⟩
 281  exact hne (no_protocol_separates Us hUs c c' h)
 282
 283/-! ## 4. Weak complementarity: the injection on the gauge quotient -/
 284
 285/-- The gauge setoid on cell configurations. -/
 286def gaugeSetoid : Setoid CellCfg := ⟨gaugeRel, gaugeRel_equivalence⟩
 287
 288/-- **Physical states of the cell**: bulk configurations modulo gauge (= modulo the
 28916-element record kernel, by `gauge_iff_kernel`). -/
 290def PhysState : Type := Quotient gaugeSetoid
 291
 292/-- The physical state carried by a bulk configuration. -/
 293def physState (c : CellCfg) : PhysState := Quotient.mk gaugeSetoid c
 294
 295/-- The boundary record of a physical state (well-defined by construction). -/
 296def physRecord : PhysState → List Bool :=
 297  Quotient.lift faceRecord (fun _ _ h => h)
 298
 299@[simp] theorem physRecord_mk (c : CellCfg) : physRecord (physState c) = faceRecord c :=
 300  rfl
 301
 302/-- **WEAK COMPLEMENTARITY (quotient form, THEOREM).** The boundary record readout is
 303injective on physical states: distinct physical states of the bulk carry distinct
 304boundary records. This is the injection `bulk_phys(B) ↪ records(∂B)` the holography
 305manuscript assumes; here it is a theorem of the gauge quotient. -/
 306theorem weak_complementarity : Function.Injective physRecord := by
 307  intro a b
 308  refine Quotient.inductionOn₂ a b ?_
 309  intro c c' h
 310  exact Quotient.sound h
 311
 312/-- Every physical state's record is a posted record. -/
 313theorem physRecord_mem_image (s : PhysState) :
 314    physRecord s ∈ Finset.univ.image faceRecord := by
 315  refine Quotient.inductionOn s ?_
 316  intro c
 317  exact Finset.mem_image_of_mem faceRecord (Finset.mem_univ c)
 318
 319/-- No ghost records: every posted record is realized by a physical state. With
 320`weak_complementarity`, physical states biject with posted records. -/
 321theorem physRecord_surjective_on_records :
 322    ∀ r ∈ Finset.univ.image faceRecord, ∃ s : PhysState, physRecord s = r := by
 323  intro r hr
 324  obtain ⟨c, -, rfl⟩ := Finset.mem_image.mp hr
 325  exact ⟨physState c, rfl⟩
 326
 327/-- 16 posted records = 16 physical states = 4 posted bits (re-export of the cell rank
 328computation of the injection test). -/
 329theorem physState_records_card : (Finset.univ.image faceRecord).card = 16 :=
 330  record_image_card
 331
 332/-- **The holographic bound through weak complementarity.** The physical states of the
 3338-vertex bulk embed (via `weak_complementarity` + `physRecord_mem_image`) into the
 334posted-record set: 16 states = 4 posted bits, strictly inside the 6-bit boundary record
 335capacity — the cell-scale instance of the boundary access law
 336(`HolographicAccessBound.access_bounded_by_aperture`). -/
 337theorem holographic_bound_of_weak_comp :
 338    (Finset.univ.image faceRecord).card ≤ 2 ^ 6 := by
 339  rw [physState_records_card]
 340  norm_num
 341
 342/-! ## 5. The conditional headline and its falsifier -/
 343
 344/-- **The named premise (`KernelIsGauge`, HYPOTHESIS).** A physical distinguishability
 345relation `dist` respects the ledger when every physical distinction is witnessed by a
 346posting-compatible protocol. This is the operational content of "the record kernel is
 347gauge": distinguishing bulk states requires posting the difference. -/
 348def KernelIsGauge (dist : CellCfg → CellCfg → Prop) : Prop :=
 349  ∀ c c', dist c c' → Separated c c'
 350
 351/-- **WEAK COMPLEMENTARITY FROM THE GSL (the step-3 headline).** For any physical
 352distinguishability witnessed by posting-compatible protocols, record-equal bulk states
 353are physically indistinguishable: the manuscript's complementarity injection holds with
 354the monolithic premise replaced by the no-free-record discipline. -/
 355theorem weak_complementarity_of_gsl (dist : CellCfg → CellCfg → Prop)
 356    (hG : KernelIsGauge dist) (c c' : CellCfg) (h : gaugeRel c c') : ¬ dist c c' :=
 357  fun hd => gauge_never_separated c c' h (hG c c' hd)
 358
 359/-- **The falsifier horn, stated.** If any physical process distinguishes two
 360record-equal configurations (a global parity move made observable), then `KernelIsGauge`
 361fails for that physics and weak complementarity breaks — the manuscript's countermodel is
 362realized. The fork inside step 3 is honest: this module isolates the breaking set (the 16
 363kernel moves); it does not prove no physics ever separates them. -/
 364theorem kernelIsGauge_falsifier (dist : CellCfg → CellCfg → Prop) (c c' : CellCfg)
 365    (h : gaugeRel c c') (hd : dist c c') : ¬ KernelIsGauge dist :=
 366  fun hG => weak_complementarity_of_gsl dist hG c c' h hd
 367
 368/-! ## 6. Bundled target + certificate handle -/
 369
 370/-- **The record-monotonicity target.** (1) Boundary heat is exact against the record
 371potential (no free erasure — the GSL's erasure half as bookkeeping); (2) gauge classes
 372are exactly the kernel cosets; (3) posting-compatible protocols never separate gauge
 373pairs; (4) the record readout is injective on physical states (weak complementarity);
 374(5) under the named `KernelIsGauge` premise, record-equal states are physically
 375indistinguishable; (6) 16 physical states = 4 posted bits within the 6-bit boundary
 376capacity. -/
 377def target_record_monotonicity : Prop :=
 378  (∀ c c' : CellCfg, stepHeatCell c c' = cellPotential c' - cellPotential c)
 379  ∧ (∀ c c' : CellCfg, gaugeRel c c' ↔ xorCfg c c' ∈ recordKernel)
 380  ∧ (∀ (Us : List (CellCfg → CellCfg)), (∀ U ∈ Us, RecordCompatible U) →
 381      ∀ c c', gaugeRel c c' → gaugeRel (runProtocol Us c) (runProtocol Us c'))
 382  ∧ Function.Injective physRecord
 383  ∧ (∀ (dist : CellCfg → CellCfg → Prop), KernelIsGauge dist →
 384      ∀ c c', gaugeRel c c' → ¬ dist c c')
 385  ∧ (Finset.univ.image faceRecord).card = 16
 386
 387theorem target_record_monotonicity_holds : target_record_monotonicity :=
 388  ⟨stepHeatCell_eq_potential, gauge_iff_kernel, no_protocol_separates,
 389   weak_complementarity, weak_complementarity_of_gsl, physState_records_card⟩
 390
 391/-- Verify-target certificate handle (`#print axioms`-gated). -/
 392theorem recordMonotonicityCert : target_record_monotonicity :=
 393  target_record_monotonicity_holds
 394
 395end RecordMonotonicity
 396end Holography
 397end IndisputableMonolith
 398