F_ofZ
plain-language theorem explainer
F_ofZ maps each integer Z to log(1 + Z/phi) divided by log(phi), which equals the base-phi logarithm of (1 + Z/phi). Researchers modeling masses on the phi-ladder cite it when converting anchor integers into scale factors. The definition is a direct noncomputable expression built from the module constants kappaA and lambdaA.
Claim. $F(Z) = {}_phi log(1 + Z/phi)$ for integer $Z$, where the logarithm base equals phi.
background
The module RecogSpec.Scales supplies binary scales and phi-exponential wrappers. kappaA is defined as Constants.phi while lambdaA is Real.log Constants.phi, so the ratio yields a pure base-phi logarithm. The input Z is the integer map from Masses.Anchor.Z, which converts a sector and rational charge Q into an integer via Z = (Q6^2 + Q6^4) (or the variant with an added 4 for quarks), where Q6 = 6 * Q.num / Q.den.
proof idea
Direct definition that substitutes the two sibling constants kappaA and lambdaA into the displayed expression; no lemmas or tactics are applied.
why it matters
It supplies the explicit conversion from anchor integers Z to real scale factors on the phi-ladder, supporting the mass formula yardstick * phi^(rung - 8 + gap(Z)). The definition sits inside the binary-scale machinery that implements the self-similar fixed point T6 and the eight-tick octave T7 of the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.