D_sq_cube_faces_minus_gap
plain-language theorem explainer
The arithmetic identity 25 times 6 minus 45 equals 105 holds in the natural numbers. Cross-domain analysts working on the Wave-64 meta-theorem cite this when confirming the excess of D-squared times cube faces over gap-45. The verification proceeds by direct numerical decision that evaluates the expression without further lemmas.
Claim. $5^{2} times 6 minus 45 equals 105$
background
The module establishes the cross-pattern matrix for five RS patterns: D=5, the eight-tick cube 2^3, J(1)=0, the phi-ladder, and gap-45. Each pair of patterns yields a distinct integer entry, with D-squared times cube faces listed as 150 and the excess over gap-45 computed as 105. The local setting is the C26 structural meta-claim that these patterns form a non-degenerate matrix whose entries match known RS quantities such as cognitive pair states and attention space.
proof idea
The proof is a one-line wrapper that applies the decide tactic to evaluate the arithmetic expression directly in the natural numbers.
why it matters
This theorem fills one cell of the cross-pattern matrix in the C26 meta-claim, confirming that D-squared times cube faces exceeds gap-45 by exactly 105. It aligns with framework landmarks D=5 and the gap-45 quantity while supporting the claim that all non-trivial matrix entries correspond to known RS quantities. No downstream theorems are recorded, leaving the cell as a verified but isolated arithmetic anchor for the larger matrix.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.