cube_sq_plus_cube
plain-language theorem explainer
The equality (2^3)^2 + 2^3 = 72 holds as an arithmetic identity appearing in Recognition Science bounds on cross-pattern products. Researchers verifying the Wave-62 matrix of D=5, cube, and gap relations would cite it when confirming integer entries. The proof applies a direct decision procedure to the natural-number equality.
Claim. $(2^3)^2 + 2^3 = 72$
background
The module establishes a cross-pattern matrix among five RS patterns from the Wave-62 report: D=5, 2^3=8, J(1)=0, the phi-ladder, and gap45/cube-faces. Non-trivial matrix entries include 25=D^2 for cognitive pair states, 40=D·2^3 for attention space, 64=2^6 for double cube, 360=2^3·45 for full turn, and 2025=45^2. Upstream results supply configDim as 5 in CosmicMicrowaveBackgroundFromRS, as d+2 in IntegrationGap (where it yields parity count D^2), and as 3 in CoalitionSizeFromConfigDim (where it yields 2^D-1 coalition types).
proof idea
The proof is a one-line wrapper that applies the decide tactic to confirm the natural-number equality.
why it matters
This supplies one verified entry in the C26 cross-pattern matrix meta-theorem, confirming that the 2^3 pattern with its square produces a distinct integer used in RS bounds. It aligns with the eight-tick octave (T7) via the 2^3 factor. The result feeds no downstream theorems in the current graph and touches no open scaffolding.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.