five_four_lt_two_ten
plain-language theorem explainer
The inequality 5^4 < 2^10 places four-fold recognition state spaces inside a 10-bit register. Cross-domain lattice work in Recognition Science cites the bound when sizing products such as cognitive times tumor-stage domains. The proof is a direct decide evaluation of the concrete natural-number comparison.
Claim. The inequality $5^4 < 2^{10}$ holds.
background
The module constructs a lattice of product recognition state spaces whose sizes are successive powers of five. Explicit entries include 5^2 = 25 for domain pairs, 5^3 = 125 for single triples, 5^4 = 625 for four-fold combinations, and 5^6 = 15625 for joint cognitive-oncology states. All sizes are required to satisfy bit-width constraints that keep the joint state computationally tractable, with the strongest listed requirement being 5^6 < 2^14.
proof idea
The proof is a one-line wrapper that applies the decide tactic to evaluate the arithmetic comparison 625 < 1024 directly.
why it matters
The declaration supplies the numerical verification for the 5^4 level in the C23 product lattice hierarchy. It supports the overall cross-domain claim that the full 5^6 joint state remains inside a 14-bit bound. No parent theorems are listed; the result is a basic feasibility check within the Recognition framework bit constraints.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.