gap_eq_log_phi_add_sub_one
plain-language theorem explainer
The theorem equates the Recognition residue gap(Z) to log(φ + Z)/log φ minus one whenever φ + Z exceeds zero. Spectrum modelers cite it to rewrite the structural defect for direct substitution into phi-ladder mass assignments. The argument rewrites the defining ratio logarithm via field simplifications and log-division identities, using one_lt_phi to secure the nonzero denominator.
Claim. For any integer $Z$ with $0 < φ + Z$, the gap function satisfies $gap(Z) = (log(φ + Z)/log φ) - 1$.
background
The gap function is defined as the structural residue $gap(Z) = log(1 + Z/φ)/log φ$, serving as the zero-parameter Recognition-side residue $f^{Rec}$ in the mass framework. This module verifies algebraic properties of gap(Z) to support direct Lean-checked behavior without external kernels. The upstream definition appears in IndisputableMonolith.Masses.RSBridge.Anchor.gap, which states the closed form for the residue at the anchor scale μ⋆.
proof idea
The proof applies a calc block starting from the definition gap Z = log(1 + Z/phi)/log phi. It rewrites the argument as (phi + Z)/phi using field_simp, then applies log_div to obtain the difference of logs, and finally uses field_simp to isolate the -1 term. The key supporting fact is one_lt_phi to show log phi ≠ 0.
why it matters
This result closes the algebraic identity for the gap residue, allowing direct substitution into mass formulas on the phi-ladder. It supports the claim that the integrated RG residue equals gap(Z) at the anchor scale, as described in the RSBridge.Anchor definition. The identity aligns with the self-similar fixed point phi from the forcing chain and enables verification of monotonicity properties listed as sibling declarations in the module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.