entries_distinct
The theorem establishes that the five non-trivial entries in the cross-pattern matrix (25, 40, 64, 360, 2025) are pairwise distinct. A researcher working on the Wave-64 meta-theorem would cite it to confirm the matrix is non-degenerate. The proof is a single-term application of the decide tactic that discharges all ten inequalities at once.
claimThe integers 25, 40, 64, 360, and 2025 arising from the cross products of the RS patterns satisfy $25 ≠ 40$, $40 ≠ 64$, $64 ≠ 360$, $360 ≠ 2025$, $25 ≠ 64$, $25 ≠ 360$, $25 ≠ 2025$, $40 ≠ 360$, $40 ≠ 2025$, and $64 ≠ 2025$.
background
The module defines a 5x5 cross-product matrix whose rows and columns are indexed by the core RS patterns: D=5 (cognitive pair states), 2³=8 (cube period), J=0, φ (golden ratio), and gap-45. Each entry is the product or relation of a pair, such as D²=25, D·2³=40, 2^6=64, 2³·45=360, and 45²=2025. Upstream, the Pattern type is imported from Measurement, Patterns, Streams, and Streams.Blocks as a finite window of length n, i.e., a function from Fin n to Bool, used to count ones in windows. The period definition from PulsarEmissionRegimesFromRS supplies phi^k for scaling. The local setting is the C26 meta-theorem asserting that these patterns produce a non-degenerate matrix of distinct integers.
proof idea
The proof is a one-line wrapper that refines the goal into ten separate inequalities and then applies the decide tactic to each, which succeeds because all comparisons are decidable on concrete natural numbers.
why it matters in Recognition Science
This declaration closes the non-degeneracy part of the C26 cross-pattern matrix meta-theorem in the module doc. It ensures that the structural claim (each pair of patterns produces a distinct integer) holds without collisions, supporting the broader Recognition Science framework where the eight-tick octave (T7) and D=3 dimensions generate these specific cardinalities. No downstream uses are recorded yet, but it underpins any application of the matrix to cross-domain relations such as attention space (40) or full-turn (360).
scope and limits
- Does not address whether the matrix entries match physical observables beyond the listed integers.
- Does not prove uniqueness for entries involving φ or J=0.
- Does not extend to larger pattern sets or arbitrary products.
- Does not derive the matrix values from the Recognition Composition Law.
formal statement (Lean)
53theorem entries_distinct :
54 25 ≠ 40 ∧ 40 ≠ 64 ∧ 64 ≠ 360 ∧ 360 ≠ 2025 ∧
55 25 ≠ 64 ∧ 25 ≠ 360 ∧ 25 ≠ 2025 ∧
56 40 ≠ 360 ∧ 40 ≠ 2025 ∧
57 64 ≠ 2025 := by
proof body
Term-mode proof.
58 refine ⟨?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_⟩ <;> decide
59
60/-! ## Pattern combinations across cardinalities. -/
61
62/-- D² · 2³ = 200 (D-pair × cube period). -/