five_five_lt_two_thirteen
plain-language theorem explainer
The inequality 5^5 < 2^13 shows that the full pentapod recognition state space of 3125 elements fits inside a 13-bit register. Cross-domain lattice constructions cite this bound when sizing five-fold hierarchies assembled from multiple D=5 domains. The proof reduces to a single decide tactic that evaluates the numerical comparison directly.
Claim. $5^5 < 2^{13}$
background
The Product Recognition Lattice module builds a hierarchy of recognition state spaces from cross-domain products. Powers of 5 give the cardinalities: 5^2 = 25 for pairs of D=5 domains, 5^3 = 125 for single triples such as cognitive or oncology states, 5^4 = 625 for four-fold products, 5^5 = 3125 for the full domain hierarchy, and 5^6 = 15625 for joint cognitive-oncology states. The local setting imposes information-theoretic constraints requiring these spaces to fit inside fixed bit lengths, with the module establishing the joint bound 5^6 < 2^14.
proof idea
The proof is a one-line term proof that applies the decide tactic to verify the concrete numerical inequality 3125 < 8192.
why it matters
This bound supplies the 13-bit size for the five-fold lattice and supports the module's larger claim that the joint cognitive-oncology state fits in 14 bits. It contributes to the chain of inequalities that keep product spaces computationally tractable. In the Recognition Science setting the result anchors the information-theoretic limits on the 5^n hierarchy without invoking the forcing chain or phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.