density_ratio_is_three
plain-language theorem explainer
On the coefficient bridge the free-bit (nullity) density equals three times the closure-rank density: both sides evaluate to 3/4. Anyone citing the factor-3 keystone at density level, rather than as a raw integer identity, would quote this. The proof rewrites the three bridge equalities freeBits=3, closureRank=1, rawBits=4 and closes by arithmetic.
Claim. Writing $F$, $R$, and $K$ for the free-bit count, raw-bit count, and closure rank of the coefficient bridge (as rationals), one has $F/R = 3\cdot(K/R)$. Concretely $F=3$, $K=1$, $R=4$, so the nullity density $3/4$ is three times the rank density $1/4$.
background
The module develops the Factor-3 Keystone: a conditional exclusion of the microstate reading of horizon entropy. The rank/nullity selector of RecordCostAsymmetry leaves two ledger readings. Record cost saturates the Bekenstein–Hawking $1/4$; microstate cost yields $3/4$, i.e. $S=3\cdot(A/4)$, a fixed factor of three at every horizon radius.
The coefficient bridge packages the integer ledger floor into three rationals: free bits (nullity) equal to 3, closure rank equal to 1, and raw bits equal to 4. The integer identity free bits $= 3\cdot$ closure rank is already available; the present statement lifts it to densities by dividing through by the raw-bit count.
Local setting is conditional. LEG-B (Casini-form Bekenstein bound on total static thermodynamic horizon entropy) and Schwarzschild saturation $A/4=2\pi ER$ remain named open hypotheses. Nothing in this file asserts unconditional physics; the value is the exclusion structure once those premises are granted.
proof idea
One-line algebraic reduction. Rewrite free bits by the bridge equality that sets them to 3, closure rank by the equality that sets it to 1, and raw bits by the equality that sets them to 4. The goal becomes the rational identity $3/4 = 3\cdot(1/4)$, discharged by norm_num. No analysis, no continuum limit, and no appeal to the open LEG-B premise.
why it matters
This is the density-level restatement of the ledger-forced factor three that drives the keystone. The integer form free bits $= 3\cdot$ closure rank already shows microstate cost is three times record cost; dividing by raw bits exhibits the same factor as a ratio of densities ($3/4$ versus $1/4$), which is the form that survives unit conversion and scale changes in the sibling violation lemmas.
Downstream the module uses this factor inside the conditional exclusion: if LEG-B holds for total static entropy and the record reading saturates at the horizon, then the microstate reading overshoots the bound by exactly three, with no volume scaling or large-$R$ limit required. That exclusion, together with the proved two-reading dichotomy and per-pixel additivity, is what discharges the record-cost reading of horizon entropy inside the holography stack.
No parent theorem currently imports this declaration (used-by is empty); it sits as a named density certificate beside factor_three_is_ledger_forced and the keystone certificate chain. Framework landmark: the $1/4$ versus $3/4$ split is the holographic content being selected, not a continuum GR input.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.