theorem
proved
gap45_from_D
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Mathematics.NumberTheoryFromRS on GitHub at line 48.
browse module
All declarations in this module, on Recognition.
explainer page
used by
formal source
45 nlinarith [sq_nonneg (phi ^ 4)]
46
47/-- gap45 = D²(D+2) at D=3. -/
48theorem gap45_from_D : 3 ^ 2 * (3 + 2) = 45 := by decide
49
50/-- 5 key RS number-theoretic identities. -/
51def rsKeyIdentityCount : ℕ := 5
52theorem rsi_count_five : rsKeyIdentityCount = 5 := rfl
53
54structure NumberTheoryCert where
55 phi_sq : phi ^ 2 = phi + 1
56 phi5 : phi ^ 5 = 5 * phi + 3
57 phi8 : phi ^ 8 = 21 * phi + 13
58 gap45_D : 3 ^ 2 * (3 + 2) = 45
59 five_identities : rsKeyIdentityCount = 5
60
61noncomputable def numberTheoryCert : NumberTheoryCert where
62 phi_sq := phi_sq_identity
63 phi5 := phi5_fibonacci
64 phi8 := phi8_fibonacci
65 gap45_D := gap45_from_D
66 five_identities := rsi_count_five
67
68end IndisputableMonolith.Mathematics.NumberTheoryFromRS