nine_is_D_sq
plain-language theorem explainer
The equality 9 equals 3 squared holds in the natural numbers and supplies the algebraic identity for the square of the spatial dimension. Cross-domain matrix constructions reference it when tabulating pattern products among the five core RS patterns. The proof applies the decide tactic to confirm the arithmetic fact directly.
Claim. $9 = 3^{2}$ holds in the natural numbers, encoding the square of the spatial dimension $D$ in the Recognition Science cross-pattern matrix.
background
The Cross-Pattern Matrix module assembles a 5 by 5 array of products among five RS patterns: the D=5 pattern count, the 2^3 octave, the J=0 null entry, the phi self-similar fixed point, and the gap-45 quantity. Matrix entries include 25 = D^2 for cognitive pair states and the present identity 9 = 3^2 for the dimension square. The local setting is the structural meta-claim that these patterns form a non-degenerate matrix of cross-products, each corresponding to a known RS quantity, with zero sorrys and zero axioms.
proof idea
The proof is a one-line wrapper that applies the decide tactic to the equality (9 : ℕ) = 3^2.
why it matters
This theorem supplies the algebraic identity 9 = D^2 for the spatial dimension D=3 inside the cross-pattern matrix of the Wave-64 meta-theorem. It supports framework step T8 that fixes D=3 and the eight-tick octave. No downstream uses are recorded, yet the identity closes a basic arithmetic claim required by the matrix tabulation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.