phi_power_ten_large
plain-language theorem explainer
The integer exponent 10 is strictly positive. Cosmologists citing the φ^10 correction between Hubble-radius and particle-horizon vacuum predictions need this elementary positivity fact when the rung offset is treated as a signed integer. The proof is a one-line numeric normalization.
Claim. As an integer, $10 > 0$.
background
In the vacuum-horizon forcing module, the cosmological constant density is written $\rho_\Lambda = \rho_{\mathrm{Pl}},\varphi^{-2s}$ with rung count $s$ measured from the substrate scale out to a chosen cosmological horizon. Three candidate horizons (particle, Hubble radius, de Sitter) give three different $s$ and three different predicted densities.
The particle horizon ($s\approx 294$) matches observation; the Hubble radius ($s\approx 289$) overshoots. The integer gap of five rungs, doubled in the exponent, produces a factor $\varphi^{10}$. The module doc frames the selection of the particle horizon by the causal-accumulation principle: the vacuum ledger sums only over cells that have already exchanged a comparison, whose maximal set is bounded by the particle horizon.
This declaration simply records that the exponent 10 is a positive integer, so that later algebraic manipulations treating the offset as an element of $\mathbb{Z}$ remain well-typed and sign-correct.
proof idea
One-line tactic proof: norm_num discharges the concrete inequality $(10:\mathbb{Z})>0$ by evaluating the numeral.
why it matters
The surrounding documentation ties $\varphi^{10}$ to the $\sim 123\times$ (or paper-convention $\sim 12.7\times$) mismatch between Hubble-radius and particle-horizon vacuum answers. Establishing positivity of the integer 10 is the minimal arithmetic prerequisite for treating that offset as a positive rung power on the $\varphi$-ladder. The module itself is a structural theorem (zero sorry) deriving horizon selection from causal accumulation; this lemma sits in the arithmetic support layer for the $\varphi^{10}$ discrepancy discussion, even though no downstream edge is currently recorded in the graph.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.