lam_canonical_ne_zero
plain-language theorem explainer
The theorem shows that the canonical recognition base lambda, defined as the natural logarithm of the golden ratio, is strictly positive. Researchers deriving the Global Co-Identity Constraint in its phi-anchored form cite it to keep the phase stiffness parameter nonzero. The proof is a one-line term reduction that unfolds the definition and applies the positivity of the logarithm to an argument greater than one.
Claim. $λ = ln φ$ satisfies $λ ≠ 0$, where $φ$ is the golden ratio fixed point of the Recognition Science forcing chain.
background
The Global Co-Identity Constraint module derives global phase uniqueness on connected recognition lattices from local ratio-rigidity and reduced-phase-potential conditions. The canonical base is introduced as lam_canonical := Real.log phi, the value used by gcic_kappa in the stiffness term of the reduced phase potential. The upstream lemma one_lt_phi supplies the fact that phi exceeds one, which is required for the logarithm to be positive.
proof idea
The proof is a term-mode one-liner. It unfolds lam_canonical to Real.log phi and applies ne_of_gt to Real.log_pos applied to the lemma one_lt_phi.
why it matters
This result is invoked directly by the canonical GCIC instance gcic_canonical, the form used in the Anno Recognitionis §V argument. It guarantees that the stiffness constant derived from lam_canonical remains well-defined when the recognition lattice operates at the phi-ratio. In the framework it anchors the T5 J-uniqueness step where phi is forced as the self-similar fixed point before the eight-tick octave and D = 3 are extracted.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.