five_nine_lt_two_21
plain-language theorem explainer
The numerical bound 5^9 < 2^21 serves as a sanity check within the product recognition lattice for cross-domain state spaces. It confirms that a 5^9 configuration fits inside 21 bits, supporting information-theoretic limits on combined recognition states such as cognitive and oncological domains. The proof proceeds by direct evaluation using the decide tactic.
Claim. $5^9 < 2^{21}$
background
The Product Recognition Lattice models hierarchies of recognition state spaces arising from cross-domain products. A single triple domain yields 5^3 = 125 states while the joint cognitive-oncology space reaches 5^6 = 15625 states. The module establishes that these must satisfy 5^6 < 2^14 = 16384 to fit within 14 bits, with similar bounds for higher powers. Upstream results define A as the active edge count per fundamental tick, set to 1 in integration gaps, mass anchors, and actualization operators.
proof idea
The proof is a one-line application of the decide tactic, which evaluates the concrete natural number inequality 5^9 < 2^21 by direct computation.
why it matters
This bound contributes to the lattice constraints in the cross-domain product module, ensuring that 5^9 configurations remain within feasible bit widths for recognition states. It supports the broader claim that 5^6 joint states fit in 14 bits, aligning with RS information bounds. No open questions are directly addressed here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.