IndisputableMonolith.Holography.KeystoneFactorThree

   1import IndisputableMonolith.Holography.RecordCostAsymmetry
   2import Mathlib.Analysis.SpecialFunctions.Log.Basic
   3
   4/-!
   5# The Factor-3 Keystone: a conditional exclusion of the microstate reading
   6
   7**Status: CONDITIONAL theorem (panel-greenlit Live Bet 2, 2026-07-01). Nothing here is
   8unconditional physics; the value of this module is the exclusion STRUCTURE.**
   9
  10## The claim, in one paragraph
  11
  12The rank/nullity selector (`RecordCostAsymmetry`) leaves ONE explicit physical premise for
  13the Bekenstein-Hawking `1/4`: `HorizonEntropyIsRecordCost`. The counterfactual premise
  14`HorizonEntropyIsMicrostateCost` yields `3/4`, i.e. `S = 3·(A/4)` — a factor EXACTLY 3, at
  15every horizon radius, machine-checked from the ledger floor (`microstateCost = 3 =
  163 · recordCost`). The keystone: IF the Bekenstein bound `S ≤ 2πER` holds for TOTAL
  17thermodynamic horizon entropy (LEG-B, an OPEN hypothesis stated here as a typed premise,
  18never proved), and IF the record reading saturates it at the horizon (`A/4 = 2πER`,
  19Schwarzschild saturation), THEN the microstate reading VIOLATES the bound by the fixed
  20factor 3 — no volume scaling, no bulk map, no large-`R` limit needed. Conditional on those
  21two named inputs plus per-pixel additivity (LEG-A), `HorizonEntropyIsRecordCost` is
  22discharged by exclusion within the proved two-reading dichotomy.
  23
  24## The typing audit (the panel's explicit question)
  25
  26The panel asked whether LEG-B's statement "can be total-entropy-typed." Answer, enforced
  27here by construction: the bound hypothesis `TotalEntropyBekensteinBound` is typed on a
  28STATIC entropy `S : ℝ` in the same units as the area term — the per-pixel-summed count of
  29`EntropyCandidateAudit` (candidates C3/C6 scale, bits, or their `ln 2`-converted nats).
  30It must NOT be typed on `HawkingTemperature.accessibleInfo`, which is a RATE
  31(nats·tick⁻¹); `EntropyCandidateAudit.accessibleInfo_unfold` exhibits the type mismatch.
  32The exclusion is invariant under the bits→nats conversion
  33(`violation_survives_unit_conversion`) because it is a strict ratio-3 statement, so the
  34unit choice cannot rescue the microstate reading.
  35
  36## Honest scope (per `soul.mdc`)
  37
  38- LEG-B (the Casini-form bound as a theorem about RS total entropy): **OPEN.** Stated as
  39  the explicit `Prop` `TotalEntropyBekensteinBound`, consumed as a hypothesis, never
  40  asserted.
  41- Horizon saturation `A/4 = 2πER`: **MODEL input** (Schwarzschild `R = 2GE` in RS units);
  42  consumed as a hypothesis.
  43- LEG-A (per-pixel additivity, the spectrometer's `PerPixelRecordAdditivity`): **MODEL
  44  premise**, measured to hold for private/unshared pixels under GLOBAL closure
  45  (`SharedCutMarginal`, spectrometer 2026-07-01); consumed as the hypothesis `hAdd`.
  46- The factor 3 itself: **THEOREM, axiom-clean** (`factor_three_is_ledger_forced`), from
  47  `decide` on the ledger floor.
  48- The exclusion given the above: **THEOREM** (`microstate_chain_contradicts_bound`).
  49
  50The weakest link (LEG-B) sets the tag: this module is a CONDITIONAL discharge, not an
  51unconditional derivation of `1/4`. What it buys: the selector premise is no longer a bare
  52identification — inside the holographic program (bound + saturation + additivity) the
  53kernel reading is INCONSISTENT, not merely disfavored.
  54-/
  55
  56namespace IndisputableMonolith
  57namespace Holography
  58namespace KeystoneFactorThree
  59
  60open RecordCostAsymmetry
  61
  62/-! ## The machine-checked factor 3 -/
  63
  64/-- **The factor 3 is ledger-forced, not hand-typed.** The kernel-side (microstate) cost of
  65the one-face closure map is exactly three times its image-side (record) cost: `3 = 3 · 1`.
  66Both sides are computed by `decide` on the actual map; the `3` in "the microstate reading
  67assigns `3·(A/4)`" is THIS `3`. -/
  68theorem factor_three_is_ledger_forced :
  69    microstateCost (fun c : PixelLocal.FaceCfg => PixelLocal.closed c) true
  70      = 3 * recordCost (fun c : PixelLocal.FaceCfg => PixelLocal.closed c) := by
  71  decide
  72
  73/-- The same factor at the density level: the nullity density `3/4` is three times the rank
  74density `1/4` (`CoefficientBridge.freeBits = 3 · closureRank`). -/
  75theorem density_ratio_is_three :
  76    (CoefficientBridge.freeBits : ℚ) / (CoefficientBridge.rawBits : ℚ)
  77      = 3 * ((CoefficientBridge.closureRank : ℚ) / (CoefficientBridge.rawBits : ℚ)) := by
  78  rw [CoefficientBridge.freeBits_eq_three, CoefficientBridge.closureRank_eq_one,
  79    CoefficientBridge.rawBits_eq_four]
  80  norm_num
  81
  82/-! ## LEG-B as an explicit typed premise -/
  83
  84/-- **LEG-B, total-entropy-typed (OPEN; a premise, never proved here).** The Casini-form
  85Bekenstein bound on the TOTAL static thermodynamic horizon entropy `S` (same units as the
  86area term; bits or nats, fixed consistently on both sides). This is the reading the panel
  87demanded: `S` is a static count (candidates C3/C6 of `EntropyCandidateAudit`), NOT the
  88posted-information RATE `accessibleInfo` (nats·tick⁻¹), which has the wrong type to appear
  89here. -/
  90def TotalEntropyBekensteinBound (S E R : ℝ) : Prop :=
  91  S ≤ 2 * Real.pi * E * R
  92
  93/-! ## The keystone at the area level -/
  94
  95/-- **Record reading saturates the bound.** Given horizon saturation `A/4 = 2πER`, the
  96record-reading entropy `A/4` satisfies the bound with equality. -/
  97theorem record_reading_saturates (A E R : ℝ)
  98    (hSat : A / 4 = 2 * Real.pi * E * R) :
  99    TotalEntropyBekensteinBound (A / 4) E R :=
 100  le_of_eq hSat
 101
 102/-- **Microstate reading violates the saturated bound — at every radius.** Given the same
 103saturation and a nondegenerate horizon (`0 < A`), the microstate-reading entropy `3·(A/4)`
 104strictly exceeds the bound. The violation is the fixed factor 3: no volume scaling, no
 105bulk-to-boundary map, no asymptotics. -/
 106theorem microstate_reading_violates (A E R : ℝ) (hA : 0 < A)
 107    (hSat : A / 4 = 2 * Real.pi * E * R) :
 108    ¬ TotalEntropyBekensteinBound (3 * (A / 4)) E R := by
 109  unfold TotalEntropyBekensteinBound
 110  rw [← hSat]
 111  intro h
 112  linarith
 113
 114/-- **The keystone package.** Under saturation, the two readings are separated by the
 115bound itself: record passes (with equality), microstate fails (strictly). Conditional on
 116LEG-B this is the selector discharge. -/
 117theorem keystone_selects_record_reading (A E R : ℝ) (hA : 0 < A)
 118    (hSat : A / 4 = 2 * Real.pi * E * R) :
 119    TotalEntropyBekensteinBound (A / 4) E R
 120      ∧ ¬ TotalEntropyBekensteinBound (3 * (A / 4)) E R :=
 121  ⟨record_reading_saturates A E R hSat, microstate_reading_violates A E R hA hSat⟩
 122
 123/-- **Scale-freeness of the violation.** The excess is exactly the constant 3 at every
 124saturated horizon: `3·(A/4) = 3·(2πER)` whenever `A/4 = 2πER`. This is what distinguishes
 125the keystone from a `δ`-shell or large-`R` correction argument. -/
 126theorem violation_is_scale_free (A E R : ℝ)
 127    (hSat : A / 4 = 2 * Real.pi * E * R) :
 128    3 * (A / 4) = 3 * (2 * Real.pi * E * R) := by
 129  rw [hSat]
 130
 131/-- **The unit choice cannot rescue the microstate reading.** A strict violation in bits
 132stays a strict violation in nats (multiplying both sides by `ln 2 > 0`), so the exclusion
 133is invariant under the `EntropyCandidateAudit.bitsToNats` conversion. -/
 134theorem violation_survives_unit_conversion (S bound : ℝ) (h : bound < S) :
 135    bound * Real.log 2 < S * Real.log 2 :=
 136  mul_lt_mul_of_pos_right h (Real.log_pos (by norm_num))
 137
 138/-! ## The full conditional chain, from the named ℕ-level premises -/
 139
 140/-- **The microstate chain is inconsistent (the keystone, fully typed).** Assemble the
 141named premises: the horizon carries per-pixel multiplicity `m` under the MICROSTATE
 142reading (`HorizonEntropyIsMicrostateCost`, so `m = 3` by `decide`); total entropy is
 143per-pixel additive over `N ≥ 1` private pixels (LEG-A, `hAdd`); the horizon area in pixel
 144units is `rawBits · N = 4N` and saturates `A/4 = 2πER` (`hSat`); and the total-entropy
 145Bekenstein bound holds (LEG-B, `hBound`). CONTRADICTION: `S = 3N > N = 2πER`. So within
 146the dichotomy, conditional on LEG-A + LEG-B + saturation, the microstate reading is
 147excluded and `HorizonEntropyIsRecordCost` is forced. -/
 148theorem microstate_chain_contradicts_bound
 149    (m N : ℕ) (S E R : ℝ) (hN : 0 < N)
 150    (hMicro : HorizonEntropyIsMicrostateCost m)
 151    (hAdd : S = (m : ℝ) * N)
 152    (hSat : ((CoefficientBridge.rawBits * N : ℕ) : ℝ) / 4 = 2 * Real.pi * E * R)
 153    (hBound : TotalEntropyBekensteinBound S E R) :
 154    False := by
 155  have hm : m = 3 := by
 156    unfold HorizonEntropyIsMicrostateCost at hMicro
 157    rw [hMicro]; decide
 158  have hA : ((CoefficientBridge.rawBits * N : ℕ) : ℝ) = 4 * N := by
 159    rw [CoefficientBridge.rawBits_eq_four]; push_cast; ring
 160  rw [hA] at hSat
 161  unfold TotalEntropyBekensteinBound at hBound
 162  rw [hAdd, hm, ← hSat] at hBound
 163  have hNpos : (0 : ℝ) < N := by exact_mod_cast hN
 164  push_cast at hBound
 165  linarith
 166
 167/-- **The record chain is consistent (saturation).** The same assembly under the RECORD
 168reading (`m = 1`) yields `S = N = 2πER`: the bound is saturated, not violated. Together
 169with `microstate_chain_contradicts_bound` this is the conditional discharge of
 170`HorizonEntropyIsRecordCost`: within the proved dichotomy, it is the unique reading
 171consistent with the (hypothesized) total-entropy Bekenstein bound at a saturated
 172horizon. -/
 173theorem record_chain_saturates_bound
 174    (m N : ℕ) (S E R : ℝ)
 175    (hRec : HorizonEntropyIsRecordCost m)
 176    (hAdd : S = (m : ℝ) * N)
 177    (hSat : ((CoefficientBridge.rawBits * N : ℕ) : ℝ) / 4 = 2 * Real.pi * E * R) :
 178    TotalEntropyBekensteinBound S E R := by
 179  have hm : m = 1 := by
 180    unfold HorizonEntropyIsRecordCost at hRec
 181    rw [hRec]; exact recordCost_closed
 182  have hA : ((CoefficientBridge.rawBits * N : ℕ) : ℝ) = 4 * N := by
 183    rw [CoefficientBridge.rawBits_eq_four]; push_cast; ring
 184  rw [hA] at hSat
 185  unfold TotalEntropyBekensteinBound
 186  rw [hAdd, hm]
 187  push_cast
 188  linarith [le_of_eq hSat]
 189
 190/-- **Certificate.** The keystone in one statement: conditional on LEG-A (per-pixel
 191additivity), LEG-B (total-entropy Bekenstein bound), and horizon saturation, the
 192microstate reading is inconsistent and the record reading saturates. The `1/4` premise
 193`HorizonEntropyIsRecordCost` is thereby discharged BY EXCLUSION within the dichotomy —
 194modulo exactly the named open legs, nothing else. -/
 195theorem keystone_certificate :
 196    (∀ (m N : ℕ) (S E R : ℝ), 0 < N →
 197        HorizonEntropyIsMicrostateCost m →
 198        S = (m : ℝ) * N →
 199        ((CoefficientBridge.rawBits * N : ℕ) : ℝ) / 4 = 2 * Real.pi * E * R →
 200        TotalEntropyBekensteinBound S E R → False)
 201    ∧ (∀ (m N : ℕ) (S E R : ℝ),
 202        HorizonEntropyIsRecordCost m →
 203        S = (m : ℝ) * N →
 204        ((CoefficientBridge.rawBits * N : ℕ) : ℝ) / 4 = 2 * Real.pi * E * R →
 205        TotalEntropyBekensteinBound S E R) :=
 206  ⟨fun m N S E R hN hMicro hAdd hSat hBound =>
 207      microstate_chain_contradicts_bound m N S E R hN hMicro hAdd hSat hBound,
 208    fun m N S E R hRec hAdd hSat =>
 209      record_chain_saturates_bound m N S E R hRec hAdd hSat⟩
 210
 211end KeystoneFactorThree
 212end Holography
 213end IndisputableMonolith
 214