HorizonCombModel
plain-language theorem explainer
Hypothesis bundle for the φ-horizon absorption comb: a discrete patch class, exact Fibonacci microstate counts, and a positive Planck area unit. Anyone citing the model-side entropy or area gap limits uses this package. It is a pure structure definition; the three IF-side assumptions are inserted, not forced by RS capital.
Claim. A horizon comb model is a triple consisting of (i) a discrete horizon patch class: a level-indexed family of positive microstate counts obeying the exact Fibonacci recurrence $\mathrm{count}(n+2)=\mathrm{count}(n+1)+\mathrm{count}(n)$; (ii) the identification $\mathrm{count}(n)=F_{n+1}$ with the Fibonacci sequence; and (iii) a positive Planck area unit $\ell_P^2>0$.
background
This module is a falsifier-gated preflight of a MODEL mechanism for Pillar 3 (φ-horizon absorption comb). Nothing here is a prediction. The candidate claims a quantized horizon area spectrum with gap $\Delta A=4\ln\varphi,\ell_P^2$, which via black-hole thermodynamics would yield a repeated absorption comb at $GM\omega_*=\ln\varphi/(8\pi)$. The sealed capital only supplies continuous horizon area $A=4\pi R_s^2$ and a real-valued ledger capacity bound; it does not quantize area or force a discrete patch spectrum.
The open P2 target packaged here is a horizon patch class: positive level-indexed microstate counts with the exact Fibonacci recurrence. A real derivation would need a ledger/voxel-forced patch state type, an automorphism quotient, and a counting theorem; none exist yet. The present structure adds the stronger identification that counts equal $F_{n+1}$, plus a positive bookkeeping Planck area.
Entropy is read as $\log$ of the microstate count (Boltzmann), and area as $A=4\ell_P^2 S$ (Bekenstein-Hawking). Both readings are MODEL; the sealed capital states $S=N/4$ only definitionally.
proof idea
No proof: this is a structure definition bundling three fields and one positivity hypothesis. patchClass carries the open P2 target (positive Fibonacci-recurrent counts). counts_are_fib strengthens that to exact equality with Nat.fib (n+1). lP2 with lP2_pos is the positive area unit. Downstream defs read entropy and area off these fields; the gap theorems then reduce to the unconditional Fibonacci log-ratio limit.
why it matters
This is the IF-side carrier for the entire comb preflight. Downstream, entropy and area are MODEL readings off the bundle; entropy_gap_tendsto and area_gap_tendsto then deliver the kernel-checked THEN: under the inserted hypotheses the per-level entropy gap tends to $\ln\varphi$ and the area gap to $4\ln\varphi,\ell_P^2$ (the comb's target gap). The inhabitation witness horizonCombModelWitness shows the bundle is consistent (with placeholder $\ell_P^2=1$).
Framework role: Pillar 3 stays OPEN. The module measures how much of the absorption-comb mechanism existing capital forces. Answer: kinematic algebra plus one asymptotic entropy-gap theorem are real; quantization itself is not forced, and the P1 scaling falsifier already blocks a uniform ledger gap at the current formalization level. This is categorically not the dead 0.618 echo-train route; it is an absorption/level-structure claim only.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.