module module moderate

`IndisputableMonolith.CrossDomain.ProductRecognitionLattice`

The ProductRecognitionLattice module supplies numerical inequalities between powers of 5 and 2. It proves 5^6 < 2^14 to confirm that cognitive-oncology joint states fit inside 14 bits. The module assembles a short list of independent computational lemmas verified directly from Mathlib arithmetic.

claimThe module establishes the inequalities $5^6 < 2^{14}$, $5^5 < 2^{13}$, $5^4 < 2^{10}$, $5^3 < 2^7$ and $5^2 < 2^5$.

background

This module operates in the cross-domain section of the Recognition Science framework and focuses on product recognition lattices. It introduces no new definitions and depends only on Mathlib for arithmetic. The inequalities verify compact bit-length encodings for joint states, consistent with the module documentation stating that 5^6 < 2^14 allows cognitive-oncology states to fit in 14 bits.

proof idea

The module consists of independent lemmas. Each inequality is proved by direct numerical evaluation using Mathlib tactics that unfold the powers and compare the resulting integers.

why it matters in Recognition Science

These bounds feed the product recognition lattice constructions by ensuring state sizes remain within practical bit limits. The module supplies the concrete verification for the 14-bit joint-state claim in its documentation and supports cross-domain integration without exceeding the stated width.

scope and limits

Does not prove general bounds for arbitrary exponents.
Does not reference the J-function or phi-ladder.
Does not depend on core Recognition Science modules.
Does not contain conditional hypotheses or scaffolding.

declarations in this module (24)

theorem five_pow_2 L30
theorem five_pow_3 L31
theorem five_pow_4 L32
theorem five_pow_5 L33
theorem five_pow_6 L34
theorem five_pow_7 L35
theorem five_pow_8 L36
theorem five_six_lt_two_fourteen L41
theorem five_five_lt_two_thirteen L44
theorem five_four_lt_two_ten L47
theorem five_three_lt_two_seven L50
theorem five_squared_lt_two_5 L53
theorem cognitive_oncology_joint L58
theorem cognitive_oncology_size L61
theorem joint_125_squared L64
theorem triple_joint L69
theorem five_nine_lt_two_21 L72
abbrev RSTriple L77
theorem rsTriple_card L79
abbrev RSJoint L83
theorem rsJoint_card L85
theorem rsJoint_fits_14_bits L89
structure ProductRecognitionLatticeCert L92
def productRecognitionLatticeCert L102