sqrt_10_pow_8
plain-language theorem explainer
The real square root of ten to the eighth equals ten to the fourth. Residual-stacking arguments in the ledger-hum verification path cite it to turn an N ≈ 10⁸ sample count into a clean 10⁴ factor. The proof rewrites 10⁸ as a square and applies the nonnegative form of the square-root-of-square identity.
Claim. As real numbers, $\sqrt{10^8} = 10^4$ (natural-number powers cast to $\mathbb{R}$).
background
The LedgerHum verification module studies whether a Recognition-Science residual signature, once stacked over many independent samples, reaches an observationally accessible amplitude. Sibling material fixes a nanosecond-scale pulsar residual template and a stacked residual functional of the sample count N.
When N is taken near 10⁸, the stacked amplitude involves a factor $\sqrt{N}$. Closing the comparison to a fixed threshold such as $10^{-10}$ therefore needs an exact evaluation of $\sqrt{10^8}$. This private lemma supplies that evaluation so the observability theorem can stay arithmetic rather than numeric.
Upstream scale and residual definitions elsewhere in the monolith (phi-ladder scales, alpha residual against CODATA) set the broader RS constant bookkeeping; they are not used in the body of this identity.
proof idea
Tactic proof in three short steps. First cast the natural power through Nat.cast_pow and Nat.cast_ofNat so the goal is about real powers of ten. Second, prove by ring that $(10:\mathbb{R})^8 = (10^4)^2$. Third, rewrite and apply Real.sqrt_sq, discharging nonnegativity of $10^4$ by norm_num. No Recognition-specific lemmas are required.
why it matters
The sole downstream consumer is stacked_residual_observable, whose doc-comment states that for $N \sim 10^8$ the stacked residual approaches observable scale. That theorem instantiates $N = 10^8$ and reduces the inequality stackedResidual N > 1e-10 to an arithmetic estimate of the form $8 \cdot 7.30\times 10^{-15}\cdot\sqrt{10^8}$. Substituting this lemma replaces the square root by $10^4$ and yields $\approx 5.84\times 10^{-10} > 10^{-10}$.
In the broader RS verification story this is bookkeeping, not a forcing-chain step: it lets the pulsar-timing falsifier path claim that a realistic PTA-scale stack pushes the residual above a fixed observational floor. Without the exact radical identity the observability proof would need a numeric approximation lemma instead.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.