pith. machine review for the scientific record. sign in
theorem proved term proof high

gap45_from_D

show as:
view Lean formalization →

The theorem establishes that gap45 equals D squared times (D plus 2) evaluated at D equals 3, which simplifies to the arithmetic identity 9 times 5 equals 45. Number theorists assembling the Recognition Science catalogue of five canonical identities would cite this when confirming the gap45 slot. The proof is a one-line wrapper that applies the decide tactic to the numerical equality.

claim$D^2(D + 2) = 45$ when $D = 3$, where gap45 denotes the recognition gap at rung 45.

background

The Number Theory from RS module catalogues five key identities derived from Recognition Science. gap45 is introduced as the quantity 45 arising directly from the expression D squared times (D plus 2) at D equals 3, alongside phi squared equals phi plus one, phi to the fifth equals five phi plus three, phi to the eighth greater than 46, and phi to the 44 greater than 10 to the 8. The module states that all five identities are proved with zero sorry statements and draws from prior modules on constants where D equals 3 is fixed by the unified forcing chain.

proof idea

The proof is a one-line wrapper that invokes the decide tactic to confirm the concrete arithmetic equality 3 squared times (3 plus 2) equals 45.

why it matters in Recognition Science

This identity is referenced inside the numberTheoryCert definition, which bundles the five RS identities (phi_sq_identity, phi5_fibonacci, phi8_fibonacci, gap45_from_D, and rsi_count_five). It supplies the gap45 entry in the Recognition Science number theory catalogue, connecting to the eight-tick octave and the assignment D equals 3 from the forcing chain (T8). The arithmetic is fully settled with no open questions remaining.

scope and limits

Lean usage

noncomputable def exampleCert : NumberTheoryCert where gap45_D := gap45_from_D

formal statement (Lean)

  48theorem gap45_from_D : 3 ^ 2 * (3 + 2) = 45 := by decide

proof body

Term-mode proof.

  49
  50/-- 5 key RS number-theoretic identities. -/

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.