log_rho_ne_zero
plain-language theorem explainer
The forced per-step weight ρ = φ⁻¹ lies in (0,1), so its real logarithm is strictly negative and in particular nonzero. Anyone writing the unique closing load δ₂ as a ratio of logs needs this denominator fact. The proof is a two-line term argument: log of a positive number less than one is negative, hence not zero.
Claim. Let $\rho = \varphi^{-1}$ be the forced per-step weight from measure forcing. Then $\log\rho \neq 0$. (Equivalently, since $0 < \rho < 1$, one has $\log\rho < 0$.)
background
This sits in the Alpha Genesis residual-target quarantine module: the only Alpha module allowed to mention the measured inverse fine-structure constant. M1–M3 stay blind to CODATA; here one compares the dressed prediction to the anchor and isolates a single open second-order load.
Measure forcing supplies the geometric weight $\rho = \varphi^{-1}$. The golden ratio satisfies $\varphi > 1$, so $\rho \in (0,1)$: positivity is rho_pos, and the strict upper bound is rho_lt_one. The continuous weight that dresses the channel budget is built from powers of $\rho$, so logarithms of $\rho$ appear whenever one solves for an additive correction in the spectral-load exponent.
The load-form correction is correctedAlphaInv(δ₂) = channelBudget · contWeight(spectralLoad + δ₂). The unique load that matches CODATA is written in closed form as a ratio whose denominator is exactly $\log\rho$.
proof idea
Term proof, no induction. From rho_pos ($0 < \rho$) and rho_lt_one ($\rho < 1$), Real.log_neg yields $\log\rho < 0$. Then ne_of_lt upgrades the strict inequality to $\log\rho \neq 0$.
why it matters
Without $\log\rho \neq 0$, the closed-form expression for closingLoad is ill-defined: that definition divides by $\log\rho$ to solve correctedAlphaInv(δ₂) = α⁻¹_CODATA for the unique second-order load. Downstream, corrected_at_closingLoad unfolds that definition and needs the denominator to be legitimate so the algebra recovers the CODATA anchor exactly.
In the broader RS chain this is bookkeeping on the φ-forced weight (T5–T6: J-uniqueness and φ as self-similar fixed point), not a new physical input. It keeps the residual target sharp: one number δ₂ must still be derived blind from D=3 voxel seam geometry. If a seam derivation hits closingLoad, α closes at experimental precision; if not, the channel-budget bridge is falsified. This lemma only clears the analytic path to stating that unique target.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.