five_pow_6
plain-language theorem explainer
The equality 5^6 = 15625 fixes the cardinality of the joint cognitive-oncology recognition state space in the product lattice. Cross-domain modelers in Recognition Science cite this to confirm that the combined C1-C3 configuration fits inside a 14-bit bound. The proof is a direct arithmetic decision via the decide tactic.
Claim. In the natural numbers, $5^6 = 15625$.
background
The module builds a product recognition lattice for cross-domain state spaces. It combines a cognitive domain (C1) and an oncology domain (C3), each sized by 5^3 = 125, to produce a joint space whose size is given by 5^6. The lattice hierarchy lists successive powers: 5^2 = 25 for domain pairs, 5^3 = 125 for single triples, 5^4 = 625 for four-fold products, 5^5 = 3125 for full domain hierarchies, and 5^6 = 15625 for the joint cognitive-oncology case, all subject to the bound 5^6 < 2^14.
proof idea
The proof is a one-line wrapper that invokes the decide tactic to evaluate the natural-number power and confirm the equality.
why it matters
This supplies the five_to_six field inside the ProductRecognitionLatticeCert definition that bundles lattice cardinalities and bit bounds. It realizes the C23 structural claim that cross-domain products yield a 15625-state space for the full cognitive-oncology patient configuration. In the Recognition Science setting the result anchors the 5^6 level of the hierarchy and enforces the information-theoretic constraint relative to 2^14.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.