module module moderate

`IndisputableMonolith.CrossDomain.ProductRecognitionLattice`

This module supplies concrete arithmetic lemmas on powers of five, centered on the bound 5^6 < 2^14, to certify that cognitive-oncology joint states fit inside a 14-bit encoding inside the product recognition lattice. Cross-domain researchers cite these facts when sizing state spaces or verifying bit budgets. The module consists of direct computational lemmas discharged by Mathlib arithmetic tactics.

claim$5^6 < 2^{14}$ together with the auxiliary facts $5^n = 5 imes 5^{n-1}$ for $n=2, o,8$ and the companion inequalities $5^5 < 2^{13}$, $5^4 < 2^{10}$, $5^3 < 2^7$, $5^2 < 2^5$.

background

The module lives in the CrossDomain.ProductRecognitionLattice namespace and imports only Mathlib. It introduces the family of definitions five_pow_n (n = 2 to 8) that compute successive powers of 5 and the named inequalities that bound those powers against powers of 2. The supplied module doc-comment states the intended use: the bound 5^6 < 2^14 shows that a cognitive-oncology joint state fits in 14 bits.

proof idea

This is a lemma module whose proofs are one-line wrappers that apply norm_num or decide. Each five_pow_n is introduced by a direct computation or recursive unfolding; each inequality is discharged by evaluating both sides numerically inside Mathlib.

why it matters in Recognition Science

The module supplies the numerical anchors required by the product recognition lattice construction. It directly discharges the bit-width claim stated in the module doc-comment and thereby feeds any downstream cross-domain theorem that must reason about state encoding size.

scope and limits

Does not prove general comparisons between arbitrary powers of 5 and 2.
Does not derive the bounds from Recognition Science axioms or the J-cost function.
Does not supply floating-point or asymptotic versions of the inequalities.
Does not connect the bounds to the phi-ladder or eight-tick octave.

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