violation_survives_unit_conversion
plain-language theorem explainer
A strict inequality between two reals remains strict after both sides are scaled by ln 2. Citers of the factor-3 keystone use it to show that a bits-level microstate violation of the Bekenstein bound is still a nats-level violation, so unit choice cannot rescue that reading. The proof is a one-line positivity argument: multiply on the right by ln 2 > 0.
Claim. If $S, B \in \mathbb{R}$ satisfy $B < S$, then $B \cdot \ln 2 < S \cdot \ln 2$.
background
The Factor-3 Keystone module is a conditional exclusion structure, not unconditional physics. Within the proved two-reading dichotomy, the record-cost reading of horizon entropy yields the Bekenstein-Hawking factor $1/4$, while the microstate reading yields $S = 3\cdot(A/4)$ at every horizon radius, forced from the ledger floor (microstateCost = 3). Conditional on per-pixel additivity (LEG-A), the total-entropy Bekenstein bound (LEG-B, still open), and Schwarzschild saturation $A/4 = 2\pi E R$, the microstate reading violates the bound by exactly three.
Entropy candidates may be counted in bits or converted to nats by multiplying by $\ln 2$. The module's typing audit insists LEG-B be stated on static total entropy in the same units as the area term, not on a rate such as accessible information per tick. This lemma records that a strict inequality is preserved under that conversion, so the unit choice cannot erase the factor-3 violation.
proof idea
Term-mode one-liner. Apply mul_lt_mul_of_pos_right to the hypothesis $B < S$, supplying positivity of $\ln 2$ via Real.log_pos and a norm_num proof that $2 > 1$. No Recognition-specific lemmas enter; the step is pure ordered-field arithmetic on $\mathbb{R}$.
why it matters
The module doc names this result as the reason the exclusion is invariant under the bits-to-nats conversion: a strict ratio-3 statement cannot be rescued by changing units. It closes a typing loophole in the conditional chain that, given LEG-A, LEG-B, and horizon saturation, excludes the microstate reading and forces the record-cost reading inside the dichotomy left by RecordCostAsymmetry.
Sibling results assemble the full contradiction (microstate_chain_contradicts_bound, keystone_certificate, keystone_selects_record_reading). This lemma is the unit-invariance hinge those assemblies rely on when entropy is audited in nats rather than bits. LEG-B itself remains an open typed hypothesis; the value here is structural, not a claim that the bound has been proved in RS.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.