below
plain-language theorem explainer
In the Seven Gaps horizon-ledger preflight, the continuum horizon area is the ordinary Schwarzschild capital A(R_s)=4\pi R_s^2 on a positive real radius, mirrored because the Relativity subtree is sealed. Anyone auditing Pillar 3 (φ-horizon absorption comb) cites this locus: continuous area plus λ-scaling already blocks a uniform area gap. Extraction here is documentation-adjacent with no proof body, so the mathematical payload is the P1a continuum setup, not a standalone proved lemma.
Claim. The horizon-area capital is the continuum function $A(R_s)=4\pi R_s^2$ for $R_s>0$. Under positive real scalings of the radius, the image of $A$ still covers every positive real (no forced discrete area gap). This is a definitional mirror of the sealed black-hole entropy area, restated only because that subtree cannot be imported here.
background
Module setting (Seven Gaps, Pillar 3 fallback): a falsifier-gated preflight of a model mechanism, not an RS prediction. The candidate is horizon-area quantization with gap $\Delta A=4\ln\varphi,\ell_P^2$, converted by BH thermodynamics into an absorption comb at $GM\omega_*=\ln\varphi/(8\pi)\approx 0.019$. Pillar 3 stays open; nothing here is derived capital forcing that spectrum.
Sealed Relativity capital (inspection-mirrored, not imported): HorizonArea is the continuous real $4\pi R_s^2$ with sole admissibility $0<R_s$; LedgerCapacityLimit is the real bound $A/\ell_0^2$, scale-covariant, not a state count. Active import RecognitionLedger supplies a real-valued ledger cost on a finite lattice (symmetry, diagonal zero, nonnegativity, RCL subadditivity), with boundaryCost as the horizon analogue—again unquantized.
The dead $0.618$ echo-train route in BlackHoleEchoesSI is explicitly not revived: this preflight concerns absorption/level structure, a different observable class.
proof idea
No proof body is attached to this extraction (zero body lines; claim/proof style recorded as other). Nearby P1a intent is definitional: restate $A(R_s)=4\pi R_s^2$ as a local mirror so scaling lemmas can run without importing the sealed Relativity subtree. Downstream siblings in the same section then show the positive-homogeneity/scaling family still hits every positive area and that ledger boundary cost admits no uniform gap—i.e. the continuum modulus itself is the obstruction, not a tactic script on this decl.
why it matters
Earns its place as the continuum baseline for the P1 scaling falsifier of the φ-horizon absorption-comb model. Module status is explicit: kinematic algebra and one asymptotic entropy-gap fact can be real, but quantization is not forced; scaling_family_blocks_ledger_gap and ledger_boundary_cost_no_uniform_gap (siblings) are the load-bearing no-gos that keep Pillar 3 open.
Framework contact is negative but sharp: RS landmarks (T5 J-uniqueness, RCL, φ, eight-tick) are not used to derive $\Delta A\propto\ln\varphi$. The preflight measures how little of the comb existing capital forces. CAVEAT recorded in-file: mirror equality to sealed HorizonArea is inspection-only under the sealed-import guard; drift in the sealed formula silently invalidates the P1 no-go.
Reported used-by edges span cost algebra and unrelated astrophysics/chemistry decls; treat cross-module citation edges as unreliable for this sparse extract.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.