mass_ratio_phi_power
plain-language theorem explainer
The declaration equates the exponential form of the RG-evolved mass ratio to its expression as a negative power of phi. Researchers converting integrated residues into the phi-ladder mass formula in Recognition Science would cite it when substituting the lambda-normalized transport into structural mass expressions. The proof is a short tactic sequence that rewrites the exponent via ring lemmas and applies the exp-log identity after confirming positivity of phi.
Claim. If the mass ratio satisfies $m(μ_1)/m(μ_0) = exp(-λ f)$, then $m(μ_1)/m(μ_0) = φ^{-f}$, where $λ = ln φ$.
background
In the RGTransport module the integrated residue is defined by $f(μ_0, μ_1) = (1/λ) ∫_{ln μ_0}^{ln μ_1} γ_m(μ') d(ln μ')$, with λ = ln φ chosen so that the transport aligns with the phi-ladder mass formula. The structural mass at the anchor satisfies $m(μ⋆) = m_phys · φ^{f(μ⋆, m_phys)}$, which rearranges to the physical mass $m_phys = m_struct · φ^{-f}$. Upstream results supply positivity of phi via one_lt_phi and the discrete scale definition phi^k in LargeScaleStructureFromRS, embedding the continuous RG flow inside the discrete phi-tiers of the framework.
proof idea
The tactic proof first obtains 0 < phi from lt_trans applied to one_lt_phi. It simplifies the definition of lambda, then uses two ring rewrites to move the exponent into the form log phi · (-f_residue). The final step invokes Real.log_rpow on the positive base together with Real.exp_log to replace exp(log phi · (-f_residue)) by phi^(-f_residue).
why it matters
The theorem supplies the direct substitution that converts the RG residue into the phi-power mass formula, closing the interface between residueAtAnchor and the structural mass expression. It therefore supports anchorClaimHolds and the phenomenological identification of f with gap(Z). In the larger Recognition Science setting it reinforces the self-similar fixed point forced at T6, where phi makes mass ratios commensurate with the eight-tick octave and the D = 3 spatial structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.