entropy
plain-language theorem explainer
Horizon entropy at discrete level n is the natural log of the patch-class microstate count: a Boltzmann reading inside the horizon-comb model bundle. Anyone citing the Seven Gaps Pillar-3 preflight or FRW entropy bookkeeping will hit this definition. It is a one-line Real.log wrapper, not a derived theorem from RS capital.
Claim. Given a horizon comb model $M$ (discrete patch class, Fibonacci microstate counts, positive Planck area) and level $n\in\mathbb{N}$, the horizon entropy is $S(M,n)=\log(\Omega_n)$, where $\Omega_n$ is the number of microstates of $M$'s patch class at level $n$.
background
This module is a falsifier-gated preflight of a candidate $\varphi$-horizon absorption comb. Pillar 3 stays open: nothing here is a prediction. The candidate mechanism (area quantization $\Delta A=4\ln(\varphi),\ell_P^2$, converting via BH thermodynamics to a comb at $GM\omega_*=\ln(\varphi)/(8\pi)$) is MODEL; its load-bearing hypotheses are not forced by RS capital.
The ambient structure is a horizon comb model: a discrete horizon patch class (P2, open), the stipulation that microstate counts equal Fibonacci numbers, and a positive Planck-area bookkeeping constant $\ell_P^2$. Entropy is read as log-count (Boltzmann); the sibling area reading is $A=4,\ell_P^2,S$, i.e. the Bekenstein–Hawking identity $S=A/(4\ell_P^2)$, mirrored definitionally from sealed capital rather than re-derived.
Upstream capital supplies continuous horizon area $4\pi R_s^2$, a real capacity bound $A/\ell_0^2$, and a real-valued recognition-ledger boundary cost. None of those quantize area or force a discrete spectrum; this definition only packages the MODEL Boltzmann reading.
proof idea
Pure definition: cast the patch-class microstate count at level $n$ to a real and take $\mathrm{Real.log}$. No lemmas, no tactics, no algebraic reduction. The Fibonacci count hypothesis lives on the model structure and is not invoked in the body.
why it matters
This is the entropy carrier for the Pillar-3 horizon-comb preflight. Downstream cosmology consumes it heavily: FRW entropy conservation (continuity from Friedmann, comoving entropy conservation, dilution from FRW, radiation $aT$ constancy, Gibbs–Duhem) and baryogenesis staging (entropy/photon ratio post-annihilation, sphaleron magnitude bounds, source orientation). The module header is explicit that kinematic algebra and one asymptotic entropy-gap theorem are real capital, while quantization itself is not forced; the P1 scaling falsifier currently blocks a uniform ledger gap. Paired with the sibling area reading $A=4\ell_P^2 S$, it lets the preflight state Bekenstein–Hawking bookkeeping without importing the sealed BH subtree. It does not revive the dead $0.618$ echo-train route; the observable here is an absorption/level-structure comb, not an echo time series.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.