one_div_eight_sub_one_div_fortyfive
plain-language theorem explainer
The rational identity one eighth minus one forty-fifth equals thirty seven over three hundred sixty holds exactly. Recognition Science cites this as a stable arithmetic anchor when combining the eight-tick octave with the factorizations of forty five and three hundred sixty inside bridge lemmas. The proof is a one-line wrapper that invokes norm_num to perform the subtraction over a common denominator.
Claim. In the rationals, $1/8 - 1/45 = 37/360$.
background
The module collects small decidable arithmetic facts about integers that recur in Recognition Science, such as the eight-tick octave (period 2^3), the factorization of forty five as three squared times five, the gcd of eight and forty five being one, and their lcm being three hundred sixty. These facts serve as boring but stable anchors that keep later bridge lemmas readable without re-proving the same arithmetic. The local setting is standard rational arithmetic from Mathlib with no additional Recognition Science hypotheses.
proof idea
The proof is a one-line wrapper that applies the norm_num tactic to normalize the rational subtraction and confirm the common-denominator result.
why it matters
This identity supplies a concrete arithmetic fact used when Recognition Science combines the eight-tick octave (T7) with the phi-ladder and prime markers such as 37. It belongs to the collection of RSConstants that prevent repeated arithmetic in higher bridge lemmas, supporting calculations that reach the alpha inverse band and the mass formula.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.