entries_distinct
plain-language theorem explainer
The cross-pattern matrix entries 25, 40, 64, 360, and 2025 are pairwise distinct. Researchers verifying non-degeneracy of the Wave-64 meta-theorem cite this to confirm the matrix structure. The proof is a term-mode application of refine to split the conjunction followed by decide on each inequality.
Claim. The non-trivial entries of the cross-pattern matrix are pairwise distinct: $25 ≠ 40 ∧ 40 ≠ 64 ∧ 64 ≠ 360 ∧ 360 ≠ 2025 ∧ 25 ≠ 64 ∧ 25 ≠ 360 ∧ 25 ≠ 2025 ∧ 40 ≠ 360 ∧ 40 ≠ 2025 ∧ 64 ≠ 2025$.
background
The module defines the cross-pattern matrix over five RS patterns (D=5, 2³=8, J=0, φ, gap45) whose products yield the listed integers: 25=D², 40=D·2³, 64=2⁶, 360=2³·45, 2025=45². Each entry is asserted to match a known RS quantity such as cognitive pair states or full-turn ceiling. Upstream results supply Pattern as the type Fin n → Bool (finite boolean windows) in Measurement, Patterns, Streams, and Streams.Blocks, plus the noncomputable period function returning phi^k.
proof idea
Term-mode proof. The refine tactic constructs the ten-element conjunction; the decide tactic then discharges every inequality by direct computation.
why it matters
Establishes non-degeneracy for the C26 cross-pattern matrix meta-theorem. The result confirms that distinct pattern pairs produce distinct integers, consistent with Recognition Science emphasis on unique products in the phi-ladder and eight-tick constructions. No downstream theorems yet reference it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.