lambdaA
plain-language theorem explainer
lambdaA is the natural logarithm of the golden ratio phi taken from the Constants bundle. Workers on phi-exponential scaling in Recognition Science reference it when building logarithmic mappings for integer rungs. The declaration is supplied by a single-line noncomputable definition.
Claim. $λ_A := ln φ$, where $φ$ is the golden ratio supplied inside the abstract Constants structure of CPM constants.
background
The module addresses binary scales and φ-exponential wrappers. Upstream, Constants is an abstract structure bundling CPM constants (Knet, Cproj, Ceng, Cdisp) with the axiom that Knet is nonnegative. The definition supplies the logarithmic base required for exponential mappings that wrap integer arguments onto the phi ladder.
proof idea
The declaration is a direct definition that assigns lambdaA to the real logarithm of phi drawn from Constants.
why it matters
The definition is referenced by the scaling function for integer Z and by the lemma establishing that the constant is nonzero. It supplies the logarithmic factor inside the phi-exponential wrappers of the Recognition framework and thereby supports the self-similar fixed point phi (T6) used in rung constructions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.