horizonCombPreflightStatus_flags
plain-language theorem explainer
Records the eight boolean preflight flags for the φ-horizon absorption-comb model: scaling family present, area gap not forced, no discrete horizon state class, asymptotic entropy-gap theorem landed, exact gap not derived, no transition capital, mechanism unforced, and the dead 0.618 echo not revived. Anyone auditing Pillar 3 openness cites this snapshot. Proof is pure reflexivity against the canonical status definition.
Claim. The canonical horizon-comb preflight status satisfies: a continuous scaling family $A(\lambda e)=\lambda^2 A(e)$ exists at the current formalization (true); the area gap $\Delta A=4\ln\varphi\,\ell_P^2$ is forced (false); a discrete horizon state class sits in RS capital (false); the asymptotic entropy-gap theorem $\ln F\to\ln\varphi$ has landed (true); an exact area gap is derived (false); transition capital exists (false); the mechanism is forced (false); the echo discriminator is revived (false).
background
This module is a falsifier-gated preflight of a model mechanism for Pillar 3, not a prediction. The candidate claims horizon-area quantization 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)\approx 0.019147$ for Schwarzschild. Existing capital supplies continuous horizon area $A=4\pi R_s^2$, a real capacity bound $A/\ell_0^2$, and a real-valued recognition ledger with boundary cost on a substrate bipartition; none of these quantize area.
The status structure packages eight booleans that score how much of that model the present formalization forces. Upstream, the canonical status definition hard-codes the honest answers: P1's continuous scaling family exists (and blocks a uniform gap), P2's discrete state class is absent, P3 contributes only the asymptotic Fibonacci entropy-gap fragment, and P4/transition capital is empty. The dead $\varphi$-rung echo-train route (damping $1/\varphi\approx 0.618$) is kept explicitly off; this preflight concerns absorption level structure, a different observable.
proof idea
One-line term proof: the eight conjuncts are definitional equalities of boolean fields. Unfolding the canonical status definition reduces each side to the same literal true or false, discharged by eight rfl constructors packed as an anonymous product. No lemmas, no tactics, no arithmetic.
why it matters
This is documentation capital, not new mathematics: it freezes the honest forced fraction of the horizon-comb model so Pillar 3 cannot be silently closed. Module status is explicit that Pillar 3 stays open; the kinematic algebra and one asymptotic entropy-gap theorem are real, while quantization content is 0% forced. Downstream use is empty by design: the record is a gate, not a lemma consumers rewrite with. It also locks the separation from the killed O3/O4 echo discriminator, preventing revival of the 0.618 train under a new name. In the broader RS map this sits outside the T0–T8 forcing chain; $\varphi$ appears only through the model gap and the landed asymptotic $\ln F\to\ln\varphi$ fragment, not as a derived horizon spectrum.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.