factor_three_is_ledger_forced
plain-language theorem explainer
On the one-face pixel closure map, the microstate (kernel/nullity) cost equals exactly three times the record (image/rank) cost: 3 = 3·1. Both integers are read off the actual Boolean map, not inserted by hand. Anyone citing the holographic factor-3 keystone or the microstate-vs-record dichotomy needs this identity. The proof is a pure `decide` on finite configuration spaces.
Claim. For the one-face ledger-closure predicate on pixel face configurations, the microstate cost (log$_2$ of the kernel cardinality) equals three times the record cost (log$_2$ of the image cardinality): $\mathrm{microstateCost}(\mathrm{closed})=3\cdot\mathrm{recordCost}(\mathrm{closed})$, i.e. $3=3\cdot 1$.
background
In the holography stack, each pixel face carries a finite configuration space FaceCfg of cardinality $2^4=16$. The closed-face predicate is a Boolean map on that space. CoefficientBridge reads two ledger invariants off the actual map: the rank is $\log_2$ of the image size (parity hits both values, so $|\mathrm{image}|=2$ and rank $=1$), and the nullity (free bits) is $\log_2$ of the kernel size ($|\ker|=2^3$, so nullity $=3$).
Record cost is the image-side rank; microstate cost is the kernel-side nullity. The module's RecordCostAsymmetry selector treats these as the two candidate readings of horizon entropy density. The local setting is the Factor-3 Keystone: a conditional exclusion argument that the microstate reading yields $S=3\cdot(A/4)$ rather than the Bekenstein–Hawking $A/4$.
Upstream, closureRank and freeBits are defined by direct Finset cardinality on the closed map, not by the algebraic identity rawBits − freeBits. That forces the factor 3 to be a computed ledger fact.
proof idea
One-line computational proof: decide. Both sides reduce to concrete natural numbers on a finite Boolean configuration space (16 face configs, kernel size 8, image size 2). Lean’s decidable equality on $\mathbb{N}$ discharges $3 = 3 \cdot 1$ with no lemmas and no arithmetic rewriting beyond what decide unfolds from the cost definitions.
why it matters
This is the numerical heart of the Factor-3 Keystone module. The microstate reading of horizon entropy is not off by an asymptotic or bulk-dependent factor: it is off by exactly this ledger-forced 3 at every radius. Downstream siblings (density_ratio_is_three, microstate_reading_violates, keystone_selects_record_reading, keystone_certificate) package the exclusion: if total thermodynamic entropy obeys a Bekenstein bound $S\le 2\pi ER$ and the record reading saturates at Schwarzschild ($A/4=2\pi ER$), then the microstate reading violates the bound by the fixed ratio 3.
In Recognition terms this pins the holographic $1/4$ coefficient to the image-side (record) cost rather than the kernel-side cost, inside the proved two-reading dichotomy. LEG-B (the bound as a theorem about RS total entropy) remains an open typed hypothesis; this lemma only supplies the machine-checked factor that makes the conditional exclusion sharp. No used_by edges are recorded yet; the certificate chain in-module is the intended consumer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.