five_pow_3
plain-language theorem explainer
The declaration proves that five to the third power equals one hundred twenty-five in the natural numbers. Researchers building the product recognition lattice cite this when sizing single-triple state spaces such as cognitive or oncological domains. The proof reduces to direct arithmetic evaluation by the decide tactic.
Claim. In the natural numbers, $5^3 = 125$.
background
The Product Recognition Lattice module constructs a hierarchy of recognition state spaces from cross-domain products. Five cubed corresponds to the size of a single triple domain, for example the cognitive domain C1 or the oncology domain C3. This value enters the lattice bounds that constrain the joint cognitive-oncology space at five to the sixth power.
proof idea
A one-line wrapper applies the decide tactic to verify the numerical equality.
why it matters
The result supplies the five_cubed field inside the productRecognitionLatticeCert definition. That definition assembles the full lattice bounds, including the constraint that five to the sixth is less than two to the fourteenth, which encodes the information-theoretic limit on the combined state space.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.