IndisputableMonolith.CrossDomain.CrossPatternMatrix
The CrossPatternMatrix module supplies algebraic identities and definitions for a cross-domain pattern matrix in Recognition Science. It centers on the full turn relation tying the eight-tick octave to a complete rotation. Researchers working on periodicity and domain crossings in the phi-ladder would cite these relations. The module assembles a set of sibling definitions for squared and product terms without proofs.
claimThe full turn satisfies $2^3 times 45 = 360^circ$, with the cross pattern matrix assembled from component identities including $D_5^2$, $D_5 times 2^3$, $2^3$ squared, gap squared, and combinations such as $D^2 times$ cube and $D times$ double cube.
background
This module sits in the CrossDomain section and imports Mathlib for basic algebraic and numeric structures. It introduces definitions for matrix components built from D5 terms, the two-cube factor, and gap quantities, together with a distinctness condition on entries. These support pattern constructions that extend the eight-tick octave structure whose period is $2^3$ and the associated angular measure.
proof idea
This is a definition module, no proofs. It organizes the material as a collection of sibling declarations that enumerate the required algebraic combinations and the full-turn identity.
why it matters in Recognition Science
The module feeds cross-domain pattern results that sit above the forcing-chain steps T5 through T8. It supplies the angular closure for the eight-tick octave (T7) by equating $2^3 times 45$ to a full turn, thereby supporting later matrix constructions used in domain-interaction theorems.
scope and limits
- Does not prove any theorems or contain sorry placeholders.
- Does not reference physical constants such as alpha or G.
- Does not give an explicit matrix array or dimension.
- Does not depend on upstream lemmas or appear in downstream uses within the supplied graph.
declarations in this module (23)
-
theorem
D5_squared -
theorem
D5_times_2cube -
theorem
D5_times_gap -
theorem
twoCube_squared -
theorem
twoCube_times_gap -
theorem
gap_squared -
theorem
full_turn -
theorem
entries_distinct -
theorem
D_sq_times_cube -
theorem
D_times_double_cube -
theorem
cube_sq_plus_cube -
theorem
D_times_cube_faces -
theorem
D_sq_cube_faces_minus_gap -
theorem
cube_faces_squared -
theorem
face_pairs_minus_gap -
theorem
nine_is_D_sq -
def
matrixSize -
def
offDiagSize -
def
offDiagEntries -
theorem
offDiagEntries_eq -
theorem
offDiag_is_two_fourth -
structure
CrossPatternMatrixCert -
def
crossPatternMatrixCert