lambdaA_ne_zero
plain-language theorem explainer
Establishes that the natural logarithm of the golden ratio is nonzero. Workers on phi-ladder scalings and binary exponential wrappers in Recognition Science cite it to avoid singularities in scale factors. The proof is a one-line term application of the standard real-log nonzeroness lemma after pulling positivity and inequality facts for phi.
Claim. The natural logarithm of the golden ratio constant satisfies $ln phi ≠ 0$.
background
The RecogSpec.Scales module treats binary scales and phi-exponential wrappers. lambdaA is introduced as the natural logarithm of the golden ratio constant phi. Upstream results supply the needed facts: phi_ne_one states phi ≠ 1 (proved via one_lt_phi or phi_gt_one), while the Constants structure bundles real parameters including positivity constraints. The local setting uses these to define scale factors that appear in phi-ladder constructions.
proof idea
One-line term proof. It obtains positivity of phi from Constants.phi_pos, obtains phi ≠ 1 from phi_ne_one (sourced from either Constants or PhiLadderLattice), then applies Real.log_ne_zero_of_pos_of_ne_one via simpa after unfolding the definition of lambdaA.
why it matters
Secures a basic non-singularity fact for the phi-exponential wrappers that appear throughout binary scales. It aligns with the self-similar fixed point phi in the forcing chain (T6) and supports the eight-tick octave and phi-ladder mass formulas. No immediate downstream theorems are recorded, so the lemma functions as a module-level guard rather than feeding a named parent result.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.