triple_joint
plain-language theorem explainer
125 cubed equals 1953125 as a direct arithmetic identity fixing the 5^9 scale in the product recognition lattice. Cross-domain modelers in Recognition Science cite it to anchor triple products of 5^3 domains at roughly two million states. The proof is a single decide tactic on natural-number multiplication.
Claim. $125^{3} = 1953125$
background
The Product Recognition Lattice constructs state spaces from products of domains sized as powers of 5. A single triple (cognitive or oncology) has size 5^3 = 125; three such triples therefore reach 5^9. The module enumerates the lattice: 5^2 = 25, 5^3 = 125, 5^4 = 625, 5^5 = 3125, 5^6 = 15625 (joint cognitive-oncology), with the global constraint 5^6 < 2^14 = 16384. This theorem supplies the concrete value at the 5^9 level.
proof idea
One-line wrapper that applies the decide tactic to verify the equality of natural numbers.
why it matters
The identity anchors the 5^9 entry in the lattice hierarchy and confirms the sanity bound 5^9 < 2^21. It supports the structural claim that cross-domain products (C1 cognitive times C3 oncology) generate bounded recognition state spaces under RS information-theoretic limits. No open questions remain; the module reports zero sorry and zero axiom.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.