five_pow_7
plain-language theorem explainer
The declaration verifies that five raised to the seventh power equals 78125 in the natural numbers. Modelers of cross-domain recognition lattices cite this value when enumerating state-space sizes for combined domains such as cognitive and oncological systems. The proof reduces the equality to a direct numerical check via the decide tactic.
Claim. In the natural numbers, $5^7 = 78125$.
background
The module develops a lattice of product recognition state spaces under Recognition Science bounds. It lists successive powers of five that arise when combining domains: 5^2 for pairs, 5^3 for single triples such as C1 or C3, 5^4 for four-fold products, 5^5 for full domain hierarchies, 5^6 for joint cognitive-oncology states, and continuing to 5^7 and 5^8. The local setting requires that the 5^6 joint space remain below 2^14 to fit an information-theoretic bound of 14 bits.
proof idea
The proof is a one-line wrapper that invokes the decide tactic. This tactic evaluates the concrete arithmetic expression (5 : ℕ)^7 and confirms equality with 78125 by exhaustive computation.
why it matters
The result supplies the explicit 5^7 entry in the product recognition lattice hierarchy described in the module documentation. It extends the sequence that begins with 5^2 = 25 and reaches 5^8 = 390625, supporting the structural claim that cross-domain products generate bounded recognition state spaces. No downstream theorems depend on it in the current graph.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.