IndisputableMonolith.CrossDomain.ProductRecognitionLattice
The ProductRecognitionLattice module supplies the bound 5^6 < 2^14 to confirm that a cognitive-oncology joint state fits inside 14 bits. Cross-domain modelers would cite the collection when encoding product lattices under bit constraints. The module is a container for direct power-comparison lemmas rather than a single derived theorem.
claim$5^6 < 2^{14}$ together with the auxiliary comparisons $5^k < 2^m$ for $2 \le k \le 8$.
background
The module sits in the CrossDomain section of the Recognition Science mirror and imports only Mathlib. It introduces no new definitions or axioms; its sole content is the set of sibling lemmas that verify concrete power bounds. These bounds are required when Recognition Composition Law structures are mapped onto finite-bit product spaces.
proof idea
This is a module collecting supporting lemmas rather than a single proof; each sibling lemma verifies a specific power inequality through basic arithmetic.
why it matters in Recognition Science
The module supplies the numerical fact required for the 14-bit joint-state encoding noted in its documentation. It therefore supports any downstream cross-domain lattice construction that must remain inside a fixed bit width.
declarations in this module (24)
-
theorem
five_pow_2 -
theorem
five_pow_3 -
theorem
five_pow_4 -
theorem
five_pow_5 -
theorem
five_pow_6 -
theorem
five_pow_7 -
theorem
five_pow_8 -
theorem
five_six_lt_two_fourteen -
theorem
five_five_lt_two_thirteen -
theorem
five_four_lt_two_ten -
theorem
five_three_lt_two_seven -
theorem
five_squared_lt_two_5 -
theorem
cognitive_oncology_joint -
theorem
cognitive_oncology_size -
theorem
joint_125_squared -
theorem
triple_joint -
theorem
five_nine_lt_two_21 -
abbrev
RSTriple -
theorem
rsTriple_card -
abbrev
RSJoint -
theorem
rsJoint_card -
theorem
rsJoint_fits_14_bits -
structure
ProductRecognitionLatticeCert -
def
productRecognitionLatticeCert