lcm_eight_fortyfive_eq_360
plain-language theorem explainer
The identity lcm(8, 45) = 360 supplies a fixed numerical anchor for repeated arithmetic steps in Recognition Science calculations that involve the eight-tick octave and prime factorizations of 360 and 840. Framework developers writing valuation or lcm-based bridge lemmas cite it to keep those lemmas short and stable. The proof is a one-line wrapper that invokes native_decide on the decidable equality.
Claim. $lcm(8, 45) = 360$
background
The module collects small decidable arithmetic facts about integers that recur across the Recognition Science development, such as the values 8, 45, 360 and 840. These facts act as stable anchors that keep later bridge lemmas readable and avoid re-proving the same arithmetic repeatedly. The local setting is the file of prime facts and factorizations, where 8 = 2^3 links directly to the eight-tick octave while 45 = 3^2 * 5 appears among the prime markers.
proof idea
The proof is a one-line wrapper that applies native_decide to discharge the decidable equality.
why it matters
This equality supplies the concrete value required by the downstream vp characterization theorem, which states that the valuation at each prime of 360 equals the maximum of the valuations of 8 and 45. It anchors the factorization of 360 inside the RSConstants module and supports later work on wheel840. In the framework it connects to the eight-tick octave (T7) through the explicit factor 8 = 2^3.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.