D5_times_2cube
plain-language theorem explainer
The theorem establishes that five times eight equals forty in the natural numbers. Cross-domain matrix work cites it to populate the attention-space entry in the wave-64 structural claim. The proof is a direct decision tactic that resolves the arithmetic equality with no lemmas or hypotheses.
Claim. $5 × 2^3 = 40$
background
The CrossPatternMatrix module presents a structural meta-claim for five RS patterns (D=5, 2³=8, J(1)=0, φ-ladder, gap-45) whose pairwise products form a non-degenerate integer matrix. The entry at D5 and 2³ is listed as 40 and labeled attention space. The module documentation states that each non-trivial entry corresponds to a known RS quantity, with 40 = D · 2³.
proof idea
The proof is a one-line wrapper that applies the decide tactic directly to the arithmetic equality.
why it matters
The result is referenced inside crossPatternMatrixCert, the definition that bundles all matrix entries for certification. It supplies the concrete integer for the D5 × 2³ position, which the module documentation identifies as the attention-space quantity. In the Recognition framework this supports the eight-tick octave (T7) cross-product with the D=5 pattern.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.