lambdaA
lambdaA defines the natural logarithm of the golden ratio phi taken from the Constants bundle. Workers on binary scales and phi-exponential wrappers in the RecogSpec module cite it when building logarithmic scaling functions such as F_ofZ. The definition is a direct noncomputable assignment of Real.log to Constants.phi.
claim$λ_A := log φ$, where $φ$ is the golden ratio drawn from the abstract CPM constants bundle.
background
The module RecogSpec.Scales treats binary scales and φ-exponential wrappers. The upstream Constants structure from LawOfExistence bundles CPM constants (Knet, Cproj, Ceng, Cdisp, and phi) under nonnegativity conditions on Knet. lambdaA isolates the logarithm of phi to act as the scaling base for functions over the phi-ladder.
proof idea
This is a one-line definition that applies Real.log directly to the phi constant imported from the Constants bundle.
why it matters in Recognition Science
The definition supplies the denominator for F_ofZ, which computes a logarithmic expression over integer Z. It anchors the phi-exponential wrappers and supports the Recognition Science phi-ladder used in mass formulas of the form yardstick · φ^(rung − 8 + gap(Z)). It touches the self-similar fixed point from the forcing chain but leaves numerical verification to sibling lemmas.
scope and limits
- Does not prove any algebraic properties of lambdaA.
- Does not relate lambdaA to kappaA or other scaling constants.
- Does not establish bounds or connect to the alpha band or forcing chain steps T5-T8.
formal statement (Lean)
88@[simp] noncomputable def lambdaA : ℝ := Real.log Constants.phi