IndisputableMonolith.Gravity.SevenGaps.HorizonLedgerPreflight

   1import Mathlib
   2import IndisputableMonolith.Constants
   3import IndisputableMonolith.Gravity.RecognitionLedger
   4import IndisputableMonolith.Numerics.Interval.Log
   5
   6/-!
   7# Seven Gaps, Pillar 3 fallback: φ-horizon absorption comb PREFLIGHT
   8
   9## Status: FALSIFIER-GATED PREFLIGHT of a MODEL mechanism. Pillar 3 stays OPEN.
  10
  11NOTHING in this module is a prediction. The candidate mechanism (horizon area
  12quantization with gap ΔA = 4·ln(φ)·ℓ_P², converting via black-hole
  13thermodynamics into a repeated absorption comb at GMω* = ln(φ)/(8π) ≈ 0.019147
  14for Schwarzschild) is a MODEL whose load-bearing hypotheses are NOT derived
  15from RS capital. This module measures exactly how much of the mechanism the
  16existing capital forces. Answer: the kinematic algebra and one asymptotic
  17entropy-gap theorem are real; the quantization itself is NOT forced, and the
  18P1 scaling falsifier FAILS the mechanism at the current formalization level
  19(see `scaling_family_blocks_ledger_gap`, `ledger_boundary_cost_no_uniform_gap`).
  20
  21THE DEAD 0.618 ECHO IS NOT BEING REVIVED. `Gravity.BlackHoleEchoesSI` records
  22the φ-rung ECHO-TRAIN route (damping ratio 1/φ ≈ 0.618); that discriminator
  23was killed against O3/O4 bounds and stays dead. The present preflight concerns
  24an ABSORPTION/LEVEL-STRUCTURE claim (a comb of transition frequencies from a
  25quantized area spectrum), a categorically different observable from an
  26echo-train time series. Every docstring below keeps that distinction.
  27
  28## Capital map (what exists, file:line, verified 2026-07-15)
  29
  30* `IndisputableMonolith/Relativity/Compact/BlackHoleEntropy.lean`
  31  (SEALED subtree; the ci_guard sealed-import rule forbids importing it here,
  32  so the area function is definitionally MIRRORED below):
  33  - :19 `HorizonArea (Rs : ℝ) : ℝ := 4·π·Rs²` — area is a CONTINUOUS REAL of a
  34    continuous real radius. No discretization anywhere.
  35  - :32 `LedgerCapacityLimit (A ell0 : ℝ) : ℝ := A / ell0²` — a capacity BOUND
  36    as a real number, not a state count; scale-covariant, imposes no spectrum.
  37  - :41 `bh_entropy_from_ledger` — definitional identity S = N/4; :54
  38    `max_recognition_flux` — existential shell. Neither quantizes area.
  39* `IndisputableMonolith/Relativity/Compact/BlackHoleDerivation.lean` — the
  40  BH-001..006 sections are `True := trivial` placeholders; NOT capital.
  41* `IndisputableMonolith/Gravity/RecognitionLedger.lean` (ACTIVE, imported):
  42  - :74 `RecognitionLedger` — REAL-valued cost function on a finite lattice
  43    with symmetry, diagonal-zero, nonnegativity, RCL subadditivity.
  44  - :175 `SubstrateBipartition` — the horizon analogue (interior/exterior).
  45  - :184 `boundaryCost` — real-valued horizon cost. No quantization.
  46* `IndisputableMonolith/Gravity/BlackHoleEchoesSI.lean` — the DEAD echo route
  47  (rung radius φ^N, delay 2·t_P·φ^N·ln φ, damping 1/φ). Killed as an
  48  observable; quarantined; understood; not touched here.
  49* `IndisputableMonolith/Holography/BekensteinReduction.lean` — the closest
  50  prior area-quantization capital. Its single named postulate
  51  `SectorAreaQuantization` (:169) is REFUTED (2026-07-01, lossy-quotient
  52  construction). Its live edge-based successors (κ = 4 vs κ = 3, OPEN) would
  53  give an area quantum κ·H·ℓ_P² with H = (φ+2)·ln φ, i.e.
  54  ΔA = κ·(φ+2)·ln(φ)·ℓ_P² — NOT the comb's 4·ln(φ)·ℓ_P²; the ratio is exactly
  55  (κ/4)·(φ+2) ≈ 3.62 at κ = 4. So even the nearest OPEN quantization line does
  56  not produce this mechanism's gap. (Scratch receipt:
  57  `state/qg_full_theory/horizon_comb_preflight/comb_values.txt`.)
  58* Foundation 8-tick / voxel capital (`Patterns`, T7): TEMPORAL discreteness
  59  (period 2³ = 8). No module discretizes HORIZON AREA in φ-tied units.
  60
  61KEY ANSWER to the preflight's central question: horizon area is a continuous
  62real everywhere in the capital, with a capacity bound only. Nothing
  63discretizes it.
  64
  65## Panel-locked gate verdicts
  66
  67* **P1 (λ-scaling-modulus falsifier): the scaling family EXISTS; the area gap
  68  is NOT forced at the current formalization level; the mechanism FAILS P1 at
  69  that level.** Kernel-checked in two independent forms. Continuum form:
  70  admissibility in the capital is exactly `0 < Rs`; scaling `Rs ↦ λ·Rs`
  71  preserves it and scales area by λ² (`horizonAreaMirror_scaling`), the area
  72  map achieves EVERY positive real (`horizonArea_achieves_every_positive`),
  73  hence no positive gap separates achievable areas
  74  (`scaling_family_blocks_ledger_gap`). Ledger form: for every λ ≥ 1 the
  75  scaled ledger λ·ℒ satisfies ALL FOUR RecognitionLedger axioms including RCL
  76  subadditivity (`scaleLedger`), boundary cost scales linearly
  77  (`scaleLedger_boundaryCost`), hence the achievable horizon boundary-cost
  78  spectrum has no uniform gap either
  79  (`ledger_boundary_cost_no_uniform_gap`).
  80* **P2 (canonical horizon patch class + Fibonacci counts): NO discrete horizon
  81  state class exists in the capital.** The named missing ingredient is
  82  recorded as the Prop-level target `HorizonPatchClassTarget` with the exact
  83  Fibonacci recurrence as a field. `fibPatchWitness` shows the target is
  84  SATISFIABLE (by `Nat.fib` by fiat) — it is a consistency witness, NOT a
  85  derivation; no physics is invented. OPEN, flag false.
  86* **P3 (area-gap theorem shape): the asymptotic entropy-gap fragment is a REAL
  87  THEOREM landed here** (`fib_ratio_tendsto_phi`,
  88  `log_fib_gap_tendsto_log_phi`: ln F_{n+1} − ln F_n → ln φ, kernel-checked
  89  against `Constants.phi` via Mathlib's `tendsto_fib_succ_div_fib_atTop`).
  90  The IF-THEN chain (IF a discrete patch class exists AND its counts are
  91  Fibonacci AND S = ln(count) AND S = A/(4ℓ_P²), THEN the entropy gap tends to
  92  ln φ and the area gap tends to 4·ln(φ)·ℓ_P²) is kernel-checked with the IFs
  93  as named structure fields (`HorizonCombModel`, honestly MODEL). The EXACT
  94  per-level gap (`AreaGapTarget`) and the derivation of the IFs from RS
  95  capital remain OPEN, flag false.
  96* **P4 (nonzero adjacent-sector transition): named target only**
  97  (`AdjacentSectorTransitionNonzero`). There is NO capital for a horizon
  98  transition operator; none is pretended. OPEN, flag false.
  99
 100## Comb observable (MODEL-tier consequences, recorded with kernel bounds)
 101
 102* `combFrequencyGM = ln(φ)/(8π)` exactly; numerically 0.01914681…
 103  (scratch receipt above); kernel interval (0.0191, 0.0193) proved in
 104  `combFrequencyGM_bounds` from `Numerics.log_phi_gt_0481/lt_0483` and
 105  `Real.pi_gt_d6/pi_lt_d6`.
 106* Kerr locked shape: ω − mΩ_H = κ·ln(φ)/(2π) (`kerrCombOffset`), related to
 107  the Schwarzschild value by `kerrCombOffset_eq` (= 4κ·combFrequencyGM), and
 108  derived from the MODEL area gap by `model_area_gap_gives_kerr_comb` and
 109  `schwarzschild_comb_frequency` (GM·ω* = ln(φ)/(8π)).
 110
 111## Honest fraction forced
 112
 113Existing capital forces: the kinematic φ-algebra, the asymptotic Fibonacci
 114entropy-gap limit, and the exact-value/interval lemmas — and it POSITIVELY
 115REFUTES the quantization at the current formalization level (P1). The
 116load-bearing physical content (discrete horizon states, Fibonacci counting,
 117entropy = log-count at the horizon, the first-law conversion) is 0% forced.
 118`mechanism_forced := false`.
 119
 120Zero `sorry`, zero `admit`, zero new axioms. No vacuous `True` shells: every
 121theorem below has real mathematical content or is an `rfl`-forced status
 122record explicitly labeled as documentation.
 123-/
 124
 125namespace IndisputableMonolith
 126namespace Gravity
 127namespace SevenGaps
 128namespace HorizonLedgerPreflight
 129
 130open Constants
 131
 132noncomputable section
 133
 134/-! ## §P1a. Continuum form: the λ-scaling modulus on the horizon-area capital
 135
 136The sealed `Relativity.Compact.BlackHoleEntropy.HorizonArea` (BlackHoleEntropy
 137.lean:19) is `4·π·Rs²` on a continuous real radius with sole admissibility
 138condition `0 < Rs`. We mirror it definitionally (the sealed-import guard in
 139`scripts/ci_guard.sh` forbids importing the Relativity subtree here) and prove
 140the scaling family survives, so no area gap is forced. -/
 141
 142/-- Definitional MIRROR of the sealed capital's horizon area
 143(`Relativity/Compact/BlackHoleEntropy.lean:19`): `A(Rs) = 4·π·Rs²`.
 144Same formula, restated here because the Relativity subtree is sealed.
 145
 146CAVEAT (critic 2026-07-15): the identity between this mirror and the
 147sealed definition is INSPECTION-VERIFIED only, not kernel-checked (the
 148sealed-import guard forbids stating the equality in Lean). Any edit to
 149the sealed `HorizonArea` formula silently invalidates the P1 no-go
 150below; keep the two textually in sync. -/
 151def schwarzschildHorizonAreaMirror (Rs : ℝ) : ℝ := 4 * Real.pi * Rs ^ 2
 152
 153/-- **P1 (scaling family exists, area law).** The capital's horizon area is
 154exactly quadratically covariant under the radial scaling `Rs ↦ λ·Rs`:
 155`A(λ·Rs) = λ²·A(Rs)`. This is the continuous scaling modulus the falsifier
 156asks about. -/
 157theorem horizonAreaMirror_scaling (lam Rs : ℝ) :
 158    schwarzschildHorizonAreaMirror (lam * Rs)
 159      = lam ^ 2 * schwarzschildHorizonAreaMirror Rs := by
 160  simp only [schwarzschildHorizonAreaMirror]
 161  ring
 162
 163/-- **P1 (scaling family exists, admissibility).** The capital's ONLY
 164admissibility condition on a Schwarzschild horizon configuration is `0 < Rs`
 165(every theorem in `BlackHoleEntropy.lean` quantifies over exactly this), and
 166it is preserved by every positive scaling. So the family
 167`Rs ↦ λ·Rs (λ > 0)` stays inside the admissible class. -/
 168theorem horizonAreaMirror_scaling_admissible (lam Rs : ℝ)
 169    (hlam : 0 < lam) (hRs : 0 < Rs) : 0 < lam * Rs :=
 170  mul_pos hlam hRs
 171
 172/-- The capital's capacity bound (`LedgerCapacityLimit A ell0 = A/ell0²`,
 173BlackHoleEntropy.lean:32) is itself scale-covariant: capacity of a λ²-scaled
 174area is λ² times the capacity. A real-valued bound cannot quantize the
 175spectrum. -/
 176theorem ledgerCapacityMirror_scaling (lam A ell0 : ℝ) :
 177    (lam ^ 2 * A) / ell0 ^ 2 = lam ^ 2 * (A / ell0 ^ 2) := by
 178  ring
 179
 180/-- Every positive real is an achieved horizon area of an admissible
 181configuration: take `Rs = √(A/(4π))`. The achievable area spectrum is the
 182full ray `(0, ∞)`. -/
 183theorem horizonArea_achieves_every_positive (A : ℝ) (hA : 0 < A) :
 184    ∃ Rs : ℝ, 0 < Rs ∧ schwarzschildHorizonAreaMirror Rs = A := by
 185  have h4pi : (0 : ℝ) < 4 * Real.pi := by positivity
 186  refine ⟨Real.sqrt (A / (4 * Real.pi)),
 187    Real.sqrt_pos.mpr (div_pos hA h4pi), ?_⟩
 188  simp only [schwarzschildHorizonAreaMirror]
 189  rw [Real.sq_sqrt (le_of_lt (div_pos hA h4pi))]
 190  have hpi : Real.pi ≠ 0 := Real.pi_ne_zero
 191  field_simp
 192
 193/-- **P1 VERDICT (continuum form): the scaling family blocks the ledger area
 194gap.** For every claimed gap `g > 0` and every achieved area `A > 0` there is
 195an ADMISSIBLE configuration whose area differs from `A` but by less than `g`.
 196Hence the existing capital forces NO quantized area spectrum — in particular
 197not `ΔA = 4·ln(φ)·ℓ_P²` — and the comb mechanism FAILS gate P1 at the current
 198formalization level. This is the kernel-checked no-go the preflight was gated
 199on. -/
 200theorem scaling_family_blocks_ledger_gap (g A : ℝ) (hg : 0 < g) (hA : 0 < A) :
 201    ∃ Rs : ℝ, 0 < Rs ∧
 202      schwarzschildHorizonAreaMirror Rs ≠ A ∧
 203      |schwarzschildHorizonAreaMirror Rs - A| < g := by
 204  obtain ⟨Rs, hRs, hArea⟩ :=
 205    horizonArea_achieves_every_positive (A + g / 2) (by linarith)
 206  refine ⟨Rs, hRs, ?_, ?_⟩
 207  · rw [hArea]
 208    intro h
 209    linarith
 210  · rw [hArea, show A + g / 2 - A = g / 2 from by ring,
 211      abs_of_pos (half_pos hg)]
 212    linarith
 213
 214/-! ## §P1b. Ledger form: the λ-scaling modulus on the RecognitionLedger capital
 215
 216The active horizon capital is `Gravity.RecognitionLedger`: real-valued costs,
 217a bipartition as the horizon, `boundaryCost` as the horizon ledger content.
 218We exhibit the scaling family ON THE ACTUAL STRUCTURE: for every λ ≥ 1 the
 219pointwise-scaled ledger satisfies all four ledger axioms (RCL subadditivity
 220survives because `λ·R(u,v) ≤ R(λu, λv)` for λ ≥ 1), and the boundary cost
 221scales linearly. So the discrete-lattice layer does not quantize horizon cost
 222either. -/
 223
 224/-- The λ-scaled recognition ledger (λ ≥ 1): every cost multiplied by `lam`.
 225All four `RecognitionLedger` axioms are re-proved for the scaled object; RCL
 226subadditivity uses `lam·(2uv+2u+2v) ≤ 2(lam·u)(lam·v)+2(lam·u)+2(lam·v)`,
 227which holds because `lam² ≥ lam` for `lam ≥ 1` and costs are nonnegative. -/
 228def scaleLedger {Λ : Type*} [Fintype Λ] [DecidableEq Λ]
 229    (L : RecognitionLedger.RecognitionLedger Λ) (lam : ℝ) (hlam : 1 ≤ lam) :
 230    RecognitionLedger.RecognitionLedger Λ where
 231  cost i j := lam * L.cost i j
 232  symmetric i j := by rw [L.symmetric i j]
 233  diagonal_zero i := by rw [L.diagonal_zero i, mul_zero]
 234  nonneg i j := mul_nonneg (le_trans zero_le_one hlam) (L.nonneg i j)
 235  rcl_subadditive i j k := by
 236    have h := L.rcl_subadditive i j k
 237    have hu := L.nonneg i j
 238    have hv := L.nonneg j k
 239    have hlam0 : (0 : ℝ) ≤ lam := le_trans zero_le_one hlam
 240    simp only [RecognitionLedger.rclGate] at h ⊢
 241    nlinarith [mul_le_mul_of_nonneg_left h hlam0,
 242      mul_nonneg (mul_nonneg (mul_nonneg (sub_nonneg.mpr hlam) hlam0) hu) hv,
 243      mul_nonneg hu hv]
 244
 245/-- Boundary (horizon) cost of the scaled ledger is exactly `lam` times the
 246original: the scaling family acts CONTINUOUSLY on the horizon ledger content
 247while preserving every ledger axiom. -/
 248theorem scaleLedger_boundaryCost {Λ : Type*} [Fintype Λ] [DecidableEq Λ]
 249    (L : RecognitionLedger.RecognitionLedger Λ) (lam : ℝ) (hlam : 1 ≤ lam)
 250    (P : RecognitionLedger.SubstrateBipartition Λ) :
 251    RecognitionLedger.boundaryCost (scaleLedger L lam hlam) P
 252      = lam * RecognitionLedger.boundaryCost L P := by
 253  simp only [RecognitionLedger.boundaryCost, scaleLedger, Finset.mul_sum]
 254
 255/-- **P1 VERDICT (ledger form): no uniform gap in the horizon boundary-cost
 256spectrum.** For every claimed gap `g > 0`, every recognition ledger with
 257positive horizon boundary cost admits an axiom-preserving scaling whose
 258boundary cost is distinct but within `g`. The discrete-lattice capital does
 259not quantize horizon cost. -/
 260theorem ledger_boundary_cost_no_uniform_gap
 261    {Λ : Type*} [Fintype Λ] [DecidableEq Λ]
 262    (L : RecognitionLedger.RecognitionLedger Λ)
 263    (P : RecognitionLedger.SubstrateBipartition Λ)
 264    (hB : 0 < RecognitionLedger.boundaryCost L P)
 265    (g : ℝ) (hg : 0 < g) :
 266    ∃ (lam : ℝ) (hlam : 1 ≤ lam),
 267      RecognitionLedger.boundaryCost (scaleLedger L lam hlam) P
 268        ≠ RecognitionLedger.boundaryCost L P ∧
 269      |RecognitionLedger.boundaryCost (scaleLedger L lam hlam) P
 270        - RecognitionLedger.boundaryCost L P| < g := by
 271  set B := RecognitionLedger.boundaryCost L P with hBdef
 272  have hBne : B ≠ 0 := ne_of_gt hB
 273  have hlam : 1 ≤ 1 + g / (2 * B) := by
 274    have hpos : 0 < g / (2 * B) := div_pos hg (by linarith)
 275    linarith
 276  have hexp : (1 + g / (2 * B)) * B = B + g / 2 := by
 277    field_simp
 278  refine ⟨1 + g / (2 * B), hlam, ?_, ?_⟩
 279  · rw [scaleLedger_boundaryCost, ← hBdef, hexp]
 280    intro h
 281    linarith
 282  · rw [scaleLedger_boundaryCost, ← hBdef, hexp,
 283      show B + g / 2 - B = g / 2 from by ring, abs_of_pos (half_pos hg)]
 284    linarith
 285
 286/-! ## §P2. The named missing ingredient: a discrete horizon patch class
 287
 288The capital offers NO discrete horizon state structure: `RecognitionLedger`
 289costs are reals, `SubstrateBipartition` carries no per-patch state type, the
 290sealed `LedgerCapacityLimit` is a real bound, and the pixel-area line's only
 291quantization postulate is refuted (`Holography.BekensteinReduction`,
 292docstring). Per the preflight rules we therefore DO NOT invent physics; we
 293record the target as a Prop-level definition with the exact Fibonacci
 294recurrence as a named field, and leave existence-from-capital OPEN
 295(flag false in `horizonCombPreflightStatus`). -/
 296
 297/-- **P2 TARGET (OPEN; no RS capital constructs this).** A canonical horizon
 298patch class: a level-indexed microstate count that is positive and satisfies
 299the EXACT Fibonacci recurrence `count(n+2) = count(n+1) + count(n)`. What a
 300real derivation would require: a horizon patch state type forced by the
 301ledger/voxel capital, an automorphism quotient, and a counting theorem — none
 302of which exist yet. -/
 303structure HorizonPatchClassTarget where
 304  /-- Microstate count at area level `n` (mod horizon automorphisms). -/
 305  microstates : ℕ → ℕ
 306  /-- Every level has at least one state. -/
 307  microstates_pos : ∀ n, 0 < microstates n
 308  /-- The exact Fibonacci recurrence the φ-comb mechanism needs. -/
 309  fibonacci_recurrence :
 310    ∀ n, microstates (n + 2) = microstates (n + 1) + microstates n
 311
 312/-- CONSISTENCY WITNESS ONLY (NOT a derivation): `Nat.fib (· + 1)` satisfies
 313the target, so `HorizonPatchClassTarget` is a satisfiable specification, not
 314a vacuous one. The witness inserts Fibonacci BY FIAT; nothing in RS capital
 315selects it. The OPEN problem is existence FROM CAPITAL, which this witness
 316does not touch. -/
 317def fibPatchWitness : HorizonPatchClassTarget where
 318  microstates n := Nat.fib (n + 1)
 319  microstates_pos n := Nat.fib_pos.mpr (Nat.succ_pos n)
 320  fibonacci_recurrence n := by
 321    show Nat.fib (n + 1 + 2) = Nat.fib (n + 1 + 1) + Nat.fib (n + 1)
 322    rw [Nat.fib_add_two]
 323    exact Nat.add_comm _ _
 324
 325/-! ## §P3a. The REAL theorem fragment: Fibonacci log-gap tends to ln φ
 326
 327Kernel-checked against `Constants.phi` (definitionally `Real.goldenRatio`),
 328via Mathlib's `tendsto_fib_succ_div_fib_atTop`. Entropy interpretation: IF a
 329horizon microstate count is Fibonacci and entropy is the log-count, the
 330per-level entropy gap converges to ln φ. The interpretation is MODEL; the
 331limit itself is THEOREM. This fragment stands regardless of the comb's fate. -/
 332
 333/-- **THEOREM.** `F(n+1)/F(n) → φ` with `φ = Constants.phi` (definitionally
 334`Real.goldenRatio`). Re-export of Mathlib's `tendsto_fib_succ_div_fib_atTop`
 335against the RS constant. -/
 336theorem fib_ratio_tendsto_phi :
 337    Filter.Tendsto (fun n => (Nat.fib (n + 1) : ℝ) / (Nat.fib n : ℝ))
 338      Filter.atTop (nhds Constants.phi) :=
 339  tendsto_fib_succ_div_fib_atTop
 340
 341/-- **THEOREM (the entropy-gap fragment).** `ln F(n+1) − ln F(n) → ln φ`.
 342With `S(n) = ln(count(n))` and Fibonacci counts, the per-level entropy gap
 343converges to `ln φ`; with `S = A/(4ℓ_P²)` (MODEL) the area gap converges to
 344`4·ln(φ)·ℓ_P²`. The limit here is unconditional. -/
 345theorem log_fib_gap_tendsto_log_phi :
 346    Filter.Tendsto
 347      (fun n => Real.log (Nat.fib (n + 1) : ℝ) - Real.log (Nat.fib n : ℝ))
 348      Filter.atTop (nhds (Real.log Constants.phi)) := by
 349  have hratio : Filter.Tendsto
 350      (fun n => Real.log ((Nat.fib (n + 1) : ℝ) / (Nat.fib n : ℝ)))
 351      Filter.atTop (nhds (Real.log Constants.phi)) :=
 352    ((Real.continuousAt_log (ne_of_gt Constants.phi_pos)).tendsto).comp
 353      fib_ratio_tendsto_phi
 354  refine Filter.Tendsto.congr' ?_ hratio
 355  filter_upwards [Filter.eventually_ge_atTop 1] with n hn
 356  have hnum : ((Nat.fib (n + 1) : ℝ)) ≠ 0 := by
 357    have h : 0 < Nat.fib (n + 1) := Nat.fib_pos.mpr (Nat.succ_pos n)
 358    exact_mod_cast ne_of_gt h
 359  have hden : ((Nat.fib n : ℝ)) ≠ 0 := by
 360    have h : 0 < Nat.fib n := Nat.fib_pos.mpr hn
 361    exact_mod_cast ne_of_gt h
 362  exact Real.log_div hnum hden
 363
 364/-! ## §P3b. The MODEL chain, with the IFs as named hypothesis fields
 365
 366`HorizonCombModel` bundles the UNPROVED hypotheses the mechanism needs. Every
 367field is an IF; the theorems below are the kernel-checked THENs. Tier: MODEL.
 368None of the fields is derived from RS capital (that is precisely what P1/P2
 369report as missing). -/
 370
 371/-- **MODEL (hypothesis bundle, NOT derived).** The IF-side of the comb chain:
 372* IF a discrete horizon patch class exists (`patchClass` — P2, OPEN),
 373* IF its counts are Fibonacci (`counts_are_fib` — inserted, not forced),
 374* IF the Planck area `lP2` is positive (`lP2_pos` — bookkeeping),
 375with horizon entropy READ as log-count (`entropy` below) and area READ as
 376`4·lP2·S` i.e. `S = A/(4ℓ_P²)` (`area` below; the sealed capital's
 377`bh_entropy_from_ledger` is definitional, so this reading is also MODEL). -/
 378structure HorizonCombModel where
 379  /-- IF: a discrete horizon patch class exists (P2 target). -/
 380  patchClass : HorizonPatchClassTarget
 381  /-- IF: its microstate counts are exactly Fibonacci. -/
 382  counts_are_fib : ∀ n, patchClass.microstates n = Nat.fib (n + 1)
 383  /-- Planck area (positive bookkeeping constant, units ℓ_P²). -/
 384  lP2 : ℝ
 385  /-- IF: positivity of the area unit. -/
 386  lP2_pos : 0 < lP2
 387
 388namespace HorizonCombModel
 389
 390/-- MODEL reading: horizon entropy at level `n` is the log of the microstate
 391count (Boltzmann reading of the patch class; NOT derived from capital). -/
 392def entropy (M : HorizonCombModel) (n : ℕ) : ℝ :=
 393  Real.log (M.patchClass.microstates n : ℝ)
 394
 395/-- MODEL reading: horizon area at level `n` via `S = A/(4ℓ_P²)`, i.e.
 396`A = 4·ℓ_P²·S` (Bekenstein-Hawking reading; the sealed capital states it only
 397definitionally). -/
 398def area (M : HorizonCombModel) (n : ℕ) : ℝ :=
 399  4 * M.lP2 * M.entropy n
 400
 401/-- **THEN (kernel-checked).** Under the model hypotheses the per-level
 402entropy gap converges to `ln φ`. -/
 403theorem entropy_gap_tendsto (M : HorizonCombModel) :
 404    Filter.Tendsto (fun n => M.entropy (n + 1) - M.entropy n)
 405      Filter.atTop (nhds (Real.log Constants.phi)) := by
 406  have hshift : Filter.Tendsto
 407      (fun n =>
 408        Real.log (Nat.fib (n + 1 + 1) : ℝ) - Real.log (Nat.fib (n + 1) : ℝ))
 409      Filter.atTop (nhds (Real.log Constants.phi)) :=
 410    log_fib_gap_tendsto_log_phi.comp (Filter.tendsto_add_atTop_nat 1)
 411  refine hshift.congr fun n => ?_
 412  simp only [entropy, M.counts_are_fib]
 413
 414/-- **THEN (kernel-checked).** Under the model hypotheses the per-level AREA
 415gap converges to `4·ln(φ)·ℓ_P²` — the comb mechanism's target gap, reached
 416here ONLY as the asymptotic consequence of the inserted hypotheses. -/
 417theorem area_gap_tendsto (M : HorizonCombModel) :
 418    Filter.Tendsto (fun n => M.area (n + 1) - M.area n)
 419      Filter.atTop (nhds (4 * M.lP2 * Real.log Constants.phi)) := by
 420  have h := (M.entropy_gap_tendsto).const_mul (4 * M.lP2)
 421  refine h.congr fun n => ?_
 422  simp only [area]
 423  ring
 424
 425end HorizonCombModel
 426
 427/-- Model inhabitation witness (consistency of the hypothesis bundle; carries
 428no physics: `lP2 = 1` is a placeholder unit). -/
 429def horizonCombModelWitness : HorizonCombModel where
 430  patchClass := fibPatchWitness
 431  counts_are_fib _ := rfl
 432  lP2 := 1
 433  lP2_pos := zero_lt_one
 434
 435/-- **P3 TARGET (OPEN).** The EXACT per-level area gap
 436`A(n+1) − A(n) = 4·ln(φ)·ℓ_P²` for all `n` (not just asymptotically). No RS
 437capital forces this; what a real derivation would require is P2's patch class
 438FROM CAPITAL plus an exact (not asymptotic) counting theorem, or a different
 439exact mechanism entirely. -/
 440def AreaGapTarget (lP2 : ℝ) (A : ℕ → ℝ) : Prop :=
 441  ∀ n, A (n + 1) - A n = 4 * Real.log Constants.phi * lP2
 442
 443/-! ## §Comb observable (MODEL-tier consequences, exact values + kernel bounds)
 444
 445ABSORPTION/LEVEL-STRUCTURE claim, NOT an echo train. Numeric receipt:
 446GMω* = ln(φ)/(8π) = 0.01914681015812707
 447(`state/qg_full_theory/horizon_comb_preflight/comb_values.txt`). -/
 448
 449/-- The Schwarzschild comb observable, exact: `GM·ω* = ln(φ)/(8π)`.
 450Tier: MODEL (a consequence of the underived chain above, via the first law
 451`ΔM = κ·ΔA/(8π)` with `ω = ΔM` in ℏ = c = 1 units; see
 452`schwarzschild_comb_frequency`). NOT a prediction until the area quantization
 453is DERIVED. -/
 454def combFrequencyGM : ℝ := Real.log Constants.phi / (8 * Real.pi)
 455
 456theorem combFrequencyGM_pos : 0 < combFrequencyGM :=
 457  div_pos (Real.log_pos Constants.one_lt_phi) (by positivity)
 458
 459/-- Kernel interval for the comb observable: `0.0191 < ln(φ)/(8π) < 0.0193`.
 460Grounded in `Numerics.log_phi_gt_0481`/`log_phi_lt_0483` (Taylor-certified)
 461and `Real.pi_gt_d6`/`pi_lt_d6`. True value 0.019147 (receipt in scratch).
 462
 463TRUST-BASE CAVEAT (critic 2026-07-15): the upstream log-φ interval lemmas
 464in `Numerics/Interval/Log.lean` use `native_decide`, so this bound
 465transitively inherits the `Lean.ofReduceBool` trust base; it is NOT on
 466the bare standard-trio axiom footing of the rest of this module. -/
 467theorem combFrequencyGM_bounds :
 468    (0.0191 : ℝ) < combFrequencyGM ∧ combFrequencyGM < (0.0193 : ℝ) := by
 469  have hphi : Constants.phi = Real.goldenRatio := rfl
 470  have hlog_lo : (0.481 : ℝ) < Real.log Constants.phi := by
 471    rw [hphi]
 472    exact Numerics.log_phi_gt_0481
 473  have hlog_hi : Real.log Constants.phi < (0.483 : ℝ) := by
 474    rw [hphi]
 475    exact Numerics.log_phi_lt_0483
 476  have hpi_lo : (3.141592 : ℝ) < Real.pi := Real.pi_gt_d6
 477  have hpi_hi : Real.pi < (3.141593 : ℝ) := Real.pi_lt_d6
 478  have h8pi : (0 : ℝ) < 8 * Real.pi := by positivity
 479  constructor
 480  · rw [combFrequencyGM, lt_div_iff₀ h8pi]
 481    nlinarith
 482  · rw [combFrequencyGM, div_lt_iff₀ h8pi]
 483    nlinarith
 484
 485/-- The Kerr locked comb shape: the offset of the absorption lines from the
 486superradiant bound, `ω − m·Ω_H = κ·ln(φ)/(2π)` at surface gravity `κ`.
 487Tier: MODEL (same underived chain). -/
 488def kerrCombOffset (kappa : ℝ) : ℝ :=
 489  kappa * Real.log Constants.phi / (2 * Real.pi)
 490
 491/-- Consistency: the Kerr offset is `4κ` times the Schwarzschild observable
 492(`κ_Schw = 1/(4GM)` reproduces `GM·ω* = ln(φ)/(8π)`). -/
 493theorem kerrCombOffset_eq (kappa : ℝ) :
 494    kerrCombOffset kappa = (4 * kappa) * combFrequencyGM := by
 495  rw [kerrCombOffset, combFrequencyGM]
 496  have hpi : Real.pi ≠ 0 := Real.pi_ne_zero
 497  field_simp
 498  ring
 499
 500/-- MODEL conversion step (the first-law input, stated as a definition so its
 501hypothesis status is explicit): a transition between adjacent area sectors
 502with gap `deltaA` at surface gravity `kappa` has frequency
 503`ω = κ·ΔA/(8π·ℓ_P²)` (from `ΔM = κ·ΔA/(8πG)`, `ω = ΔM`, `ℓ_P² = G` in
 504ℏ = c = 1 units). -/
 505def modelTransitionFrequency (kappa lP2 deltaA : ℝ) : ℝ :=
 506  kappa * deltaA / (8 * Real.pi * lP2)
 507
 508/-- **THEN (kernel-checked algebra).** Feeding the MODEL area gap
 509`ΔA = 4·ln(φ)·ℓ_P²` through the first-law conversion yields exactly the Kerr
 510comb offset `κ·ln(φ)/(2π)`. -/
 511theorem model_area_gap_gives_kerr_comb (kappa lP2 : ℝ) (hlP2 : lP2 ≠ 0) :
 512    modelTransitionFrequency kappa lP2 (4 * Real.log Constants.phi * lP2)
 513      = kerrCombOffset kappa := by
 514  rw [modelTransitionFrequency, kerrCombOffset]
 515  have hpi : Real.pi ≠ 0 := Real.pi_ne_zero
 516  field_simp
 517  ring
 518
 519/-- **THEN (kernel-checked algebra).** For Schwarzschild
 520(`κ = 1/(4GM)`) the comb sits at `GM·ω* = ln(φ)/(8π)` exactly — the
 521mechanism's headline observable, derived HERE only from the inserted MODEL
 522hypotheses. -/
 523theorem schwarzschild_comb_frequency (G M lP2 : ℝ)
 524    (hG : G ≠ 0) (hM : M ≠ 0) (hlP2 : lP2 ≠ 0) :
 525    (G * M) * modelTransitionFrequency (1 / (4 * G * M)) lP2
 526        (4 * Real.log Constants.phi * lP2)
 527      = combFrequencyGM := by
 528  rw [modelTransitionFrequency, combFrequencyGM]
 529  have hpi : Real.pi ≠ 0 := Real.pi_ne_zero
 530  field_simp
 531
 532/-! ## §P4. Adjacent-sector transition: named target, no capital -/
 533
 534/-- **P4 TARGET (OPEN; there is NO capital for this and none is pretended).**
 535For a horizon transition kernel `T` between area sectors, the comb is
 536observable only if adjacent-sector matrix elements are nonzero. No RS module
 537constructs any horizon transition operator; building one would require
 538horizon dynamics (absorption amplitudes between ledger sectors), which does
 539not exist in the formalization. Flag false. -/
 540def AdjacentSectorTransitionNonzero (T : ℕ → ℕ → ℝ) : Prop :=
 541  ∀ n, T n (n + 1) ≠ 0
 542
 543/-! ## §Status flags (documentation record; the mathematics is above) -/
 544
 545/-- Status flags for the horizon comb preflight. The mechanism is NOT forced:
 546P1's scaling family survives (kernel-checked), P2's discrete state class is
 547absent from capital, P3 landed only the asymptotic fragment plus the MODEL
 548chain, P4 has no capital. The honest forced fraction is the kinematics and
 549the Fibonacci limit; the physical quantization content is 0% forced. -/
 550structure HorizonCombPreflightStatus where
 551  /-- P1: a continuous scaling family of admissible configurations with
 552  `A(λe) = λ²A(e)` EXISTS at the current formalization level (proved). -/
 553  p1_scaling_family_exists_at_current_formalization : Bool
 554  /-- P1 consequence: the area gap `ΔA = 4·ln(φ)·ℓ_P²` is forced. FALSE. -/
 555  p1_area_gap_forced : Bool
 556  /-- P2: a discrete horizon state class exists in RS capital. FALSE. -/
 557  p2_discrete_horizon_state_class_in_capital : Bool
 558  /-- P3: the asymptotic entropy-gap theorem (`ln F ratio → ln φ`) landed. -/
 559  p3_asymptotic_entropy_gap_theorem_landed : Bool
 560  /-- P3: the exact per-level area gap is derived from capital. FALSE. -/
 561  p3_exact_area_gap_derived : Bool
 562  /-- P4: capital for an adjacent-sector transition operator exists. FALSE. -/
 563  p4_transition_capital_exists : Bool
 564  /-- The absorption-comb mechanism is forced by existing capital. FALSE. -/
 565  mechanism_forced : Bool
 566  /-- The dead 0.618 echo-train discriminator is being revived here. FALSE. -/
 567  echo_discriminator_revived : Bool
 568
 569/-- The canonical preflight status (rfl-forced documentation record). -/
 570def horizonCombPreflightStatus : HorizonCombPreflightStatus where
 571  p1_scaling_family_exists_at_current_formalization := true
 572  p1_area_gap_forced := false
 573  p2_discrete_horizon_state_class_in_capital := false
 574  p3_asymptotic_entropy_gap_theorem_landed := true
 575  p3_exact_area_gap_derived := false
 576  p4_transition_capital_exists := false
 577  mechanism_forced := false
 578  echo_discriminator_revived := false
 579
 580/-- Status record (rfl-forced; documentation, not new mathematics). -/
 581theorem horizonCombPreflightStatus_flags :
 582    HorizonCombPreflightStatus.p1_scaling_family_exists_at_current_formalization
 583        horizonCombPreflightStatus = true ∧
 584    horizonCombPreflightStatus.p1_area_gap_forced = false ∧
 585    HorizonCombPreflightStatus.p2_discrete_horizon_state_class_in_capital
 586        horizonCombPreflightStatus = false ∧
 587    HorizonCombPreflightStatus.p3_asymptotic_entropy_gap_theorem_landed
 588        horizonCombPreflightStatus = true ∧
 589    horizonCombPreflightStatus.p3_exact_area_gap_derived = false ∧
 590    horizonCombPreflightStatus.p4_transition_capital_exists = false ∧
 591    horizonCombPreflightStatus.mechanism_forced = false ∧
 592    horizonCombPreflightStatus.echo_discriminator_revived = false :=
 593  ⟨rfl, rfl, rfl, rfl, rfl, rfl, rfl, rfl⟩
 594
 595end
 596
 597end HorizonLedgerPreflight
 598end SevenGaps
 599end Gravity
 600end IndisputableMonolith
 601