threehundredsixty_factorization
360 factors as 2 cubed times 3 squared times 5. Recognition Science modelers cite the equality when anchoring arithmetic steps inside bridge lemmas that reference the eight-tick octave or the 360-wheel. The proof is a one-line wrapper that delegates verification to native_decide.
claim$360 = 2^3 · 3^2 · 5$
background
The module collects small, decidable arithmetic facts about integers that recur across the reality repo, such as the numbers 8, 45, 360, 840 and the prime markers 11, 17, 37, 103, 137. These facts function as stable anchors that keep later bridge lemmas readable without repeated arithmetic proofs. The local setting is the NumberTheory.Primes subfolder, which imports basic prime and factorization machinery from Basic and Factorization.
proof idea
The proof is a one-line wrapper that invokes native_decide to confirm the arithmetic equality by decidable computation.
why it matters in Recognition Science
The declaration supplies a concrete factorization anchor used in derivations that invoke the eight-tick octave (T7) where the period 2^3 appears. It belongs to the stable collection of RS constants that support readable bridge lemmas without re-proving the same arithmetic. No open questions are touched; the result is fully proved.
scope and limits
- Does not prove uniqueness of the prime factorization.
- Does not generalize the equality to other integers.
- Does not derive the factorization from the Recognition Composition Law or the phi-ladder.
formal statement (Lean)
54theorem threehundredsixty_factorization : (360 : ℕ) = 2^3 * 3^2 * 5 := by
proof body
One-line wrapper that applies native_decide.
55 native_decide
56