n
plain-language theorem explainer
The real product 7·(1/0.515)·0.583 equals exactly the rational 4081/515. Auditors of the neutrino reference-index arithmetic in arXiv:2601.12194v1 Eq. (3.25) cite this to pin the exact value. The proof is a one-line norm_num reduction of decimal literals to rationals.
Claim. As real numbers, $7 \cdot (1/0.515) \cdot 0.583 = 4081/515$.
background
The module is a pure arithmetic check of the neutrino reference index formula written in a Recognition Science preprint screenshot. The claimed identity is $n_\nu = 7 \cdot (1/X_{\mathrm{opt}}) \cdot R_{\mathrm{RS}}$ with the concrete decimals $X_{\mathrm{opt}} = 0.515$ and $R_{\mathrm{RS}} = 0.583$, asserted there to be about 85.5.
No Recognition-cost functional, phi-ladder, or forcing-chain hypothesis enters. The only objects are real numerals; Lean treats the decimals as rationals and reduces the product exactly. Sibling statements in the same file bound the same product in $(7.92, 7.93)$ and separate it from 85.5.
proof idea
One-line tactic proof. norm_num interprets every decimal literal as a rational, multiplies, and checks equality against the target fraction 4081/515. No lemmas are invoked beyond the built-in numeric normalizer.
why it matters
The declaration is a self-contained certificate that the numeric evaluation of Eq. (3.25) in arXiv:2601.12194v1 is 4081/515 ≈ 7.924, not ≈ 85.5. Together with the sibling bounds and inequality theorems in the same module, it documents a decimal-scale arithmetic error in the published screenshot. The graph lists no downstream dependents; the result stands as a verification artifact rather than a step in the T0–T8 forcing chain or the mass ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.