D5_times_gap
plain-language theorem explainer
The declaration confirms the arithmetic product of the dimension-five pattern and the gap-forty-five pattern equals two hundred twenty-five. Workers on the Wave-64 cross-domain meta-theorem cite it to populate one cell in the non-degenerate matrix of Recognition Science pattern pairs. The proof proceeds by a direct decision procedure on natural-number equality.
Claim. $5$ times the gap parameter $45$ equals $225$ in the natural numbers.
background
The CrossPatternMatrix module develops the C26 meta-theorem asserting that five core RS patterns (D=5, 2³=8, J(1)=0, phi-ladder, gap-45/cube-faces) generate a matrix of distinct cross-products. The supplied module document lists the matrix explicitly and notes that each non-trivial entry matches a known RS quantity such as 25 = D² for cognitive pair states or 360 = 2³ · 45 for the full turn. This particular theorem isolates the D=5 row and gap-45 column product.
proof idea
The proof is a one-line wrapper that applies the decide tactic to verify the numerical equality.
why it matters
It supplies one concrete integer entry required by the C26 structural meta-claim that pattern pairs remain non-degenerate. The result sits among sibling theorems that together demonstrate the matrix produces distinct RS quantities, consistent with the eight-tick octave and phi-ladder landmarks. No downstream theorems are recorded, leaving its use as a building block for further matrix-derived relations open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.