lcm_9_5_eq_45
plain-language theorem explainer
The lemma shows that lcm(9,5) equals 45, locating the first alignment of 9-fold and 5-fold periodicities on the Recognition ladder. Gap45 analysts cite it when building the initial conflict rung and related coprimeness facts. The tactic proof invokes the gcd-lcm product identity after a direct coprimeness check, then reduces the product via one_mul and arithmetic simplification.
Claim. $lcm(9,5)=45$
background
The Gap45 module treats 9 and 5 as coprime inputs whose periodicities first coincide at their least common multiple. The proof rests on the identity gcd(a,b) * lcm(a,b) = a * b from GCDLCM.gcd_mul_lcm and the multiplicative unit succ(zero) * n = n from ArithmeticFromLogic.one_mul. These supply the algebraic reduction once coprimeness is confirmed.
proof idea
Tactic proof begins with a decide tactic establishing Nat.gcd 9 5 = 1. It applies gcd_mul_lcm to obtain the product relation, then uses simpa with the gcd value and one_mul to isolate lcm(9,5) = 9 * 5. A second decide confirms 9 * 5 = 45, after which simpa finishes the goal.
why it matters
The result supplies the base multiple for the 45-rung in the phi-ladder and feeds the first-conflict construction rung45_first_conflict within the same module. It anchors the gap analysis that later connects to mass formulas and Berry thresholds via the eight-tick octave and D=3 structure. No open scaffolding remains here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.