F_ofZ
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 in Recognition Science
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.
scope and limits
- Does not evaluate F_ofZ at concrete Z values.
- Does not prove monotonicity or other analytic properties.
- Does not connect F_ofZ to the J-cost function or defectDist.
formal statement (Lean)
91@[simp] noncomputable def F_ofZ (Z : ℤ) : ℝ := (Real.log (1 + (Z : ℝ) / kappaA)) / lambdaA
proof body
Definition body.
92