five_squared_lt_two_5
plain-language theorem explainer
The theorem establishes that 25 is strictly less than 32 as the base case for information bounds on products of two five-dimensional domains in the recognition lattice. Researchers modeling cross-domain state spaces, such as cognitive-oncology combinations, cite it to verify that small products remain inside exponential bit capacities. The proof is a direct decision procedure that evaluates the concrete natural-number comparison without lemmas.
Claim. $5^{2} < 2^{5}$
background
The module constructs a lattice of recognition state spaces from products of D=5 domains, with sizes 5²=25 for pairs, 5³=125 for single triples such as C1 or C3, and 5⁶=15625 for the joint cognitive-oncology state. The local setting requires these sizes to obey RS-derived information bounds, including the explicit constraint that the full 15625-element product fits inside 2¹⁴=16384. Upstream structures on spectral emergence supply the dimensional origin of the base-5 counting while phi-forcing and ledger factorization calibrate the underlying J-cost that motivates the exponential comparison.
proof idea
The proof is a one-line wrapper that applies the decide tactic to the concrete inequality 25 < 32.
why it matters
This base inequality anchors the product lattice hierarchy and confirms that the 5⁶ joint state satisfies the 14-bit bound required by the module. It fills the small-k case of the information-bound theorem stated in the doc-comment and supports downstream claims on cross-domain recognition capacity. The result aligns with the T5 J-uniqueness and T8 D=3 forcing steps that generate the discrete domain sizes used throughout the lattice.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.