fortyfive_eq_three_sq_mul_five
plain-language theorem explainer
The equality 45 equals 3 squared times 5 holds in the natural numbers. Modelers working with Recognition Science constants cite this to stabilize repeated references to the factorization of 45 in bridge lemmas. The proof is a one-line wrapper that invokes native_decide for direct computational verification.
Claim. $45 = 3^{2} 5$ in the natural numbers.
background
This declaration belongs to a module collecting small decidable arithmetic facts about integers that recur in the reality repo, including 8, 45, 360, 840 and prime markers such as 11, 17, 37, 103 and 137. These facts function as stable anchors that keep later bridge lemmas readable and prevent repeated arithmetic proofs. The local setting is purely computational number theory with no hypotheses beyond the natural-number type.
proof idea
The proof is a one-line wrapper that applies native_decide to verify the arithmetic equality by computation.
why it matters
This theorem supplies a stable anchor for the factorization of 45 inside the RSConstants module, which gathers prime facts and factorizations that support later bridge lemmas. It contributes to the collection of decidable constants that appear in contexts such as the eight-tick octave and related integer structures. No open questions or scaffolding are touched.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.