face_pairs_minus_gap
plain-language theorem explainer
The arithmetic identity 45 minus 36 equals 9 holds in the natural numbers and equals D squared for spatial dimension D equals 3. Analysts certifying the cross-pattern matrix in Recognition Science reference this relation when linking gap-45 to cube-face counts. The proof reduces to a single decidable arithmetic check with no lemmas required.
Claim. $45 - 6^2 = 9$, where the right-hand side equals $D^2$ and $D=3$ is the spatial dimension from the forcing chain.
background
The CrossPatternMatrix module builds a 5-by-5 matrix whose rows and columns are indexed by the patterns D=5, 2^3=8, J=0, the phi-ladder, and gap-45/cube-faces. Non-trivial entries recover known Recognition Science quantities such as 25 = D^2, 40 = D times 2^3, 45 = gap-45, and 360 = 2^3 times 45. The module states that these patterns form a non-degenerate matrix with zero sorry statements.
proof idea
The proof is a one-line wrapper that applies the decide tactic to the concrete natural-number equality.
why it matters
The result is referenced by the certification definition crossPatternMatrixCert that assembles the matrix entries. It supplies the explicit link 45 minus 36 equals 9, confirming 9 = D^2 and thereby closing the gap-45 row of the matrix against the T8 landmark that spatial dimensions equal 3.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.