structure
definition
def or abbrev
PhiInt
show as:
view Lean formalization →
formal statement (Lean)
123@[ext]
124structure PhiInt where
125 /-- The "rational" part -/
126 a : ℤ
127 /-- The "φ" part -/
128 b : ℤ
129deriving DecidableEq, Repr
130
131/-- Interpret a PhiInt as a real number: a + bφ -/
132noncomputable def PhiInt.toReal (z : PhiInt) : ℝ := z.a + z.b * φ
proof body
Definition body.
133
134/-- Zero element: 0 + 0·φ = 0 -/
135def PhiInt.zero : PhiInt := ⟨0, 0⟩
136
137/-- One element: 1 + 0·φ = 1 -/
138def PhiInt.one : PhiInt := ⟨1, 0⟩
139
140/-- The element φ itself: 0 + 1·φ -/
141def PhiInt.phi : PhiInt := ⟨0, 1⟩
142
143/-- Addition in ℤ[φ]: (a₁ + b₁φ) + (a₂ + b₂φ) = (a₁+a₂) + (b₁+b₂)φ -/
144def PhiInt.add (z w : PhiInt) : PhiInt := ⟨z.a + w.a, z.b + w.b⟩
145
146/-- Negation in ℤ[φ]: -(a + bφ) = (-a) + (-b)φ -/
147def PhiInt.neg (z : PhiInt) : PhiInt := ⟨-z.a, -z.b⟩
148
149/-- Multiplication in ℤ[φ]: uses φ² = φ + 1 to reduce.
150 (a₁ + b₁φ)(a₂ + b₂φ) = a₁a₂ + (a₁b₂ + a₂b₁)φ + b₁b₂φ²
151 = a₁a₂ + (a₁b₂ + a₂b₁)φ + b₁b₂(φ + 1)
152 = (a₁a₂ + b₁b₂) + (a₁b₂ + a₂b₁ + b₁b₂)φ -/
153def PhiInt.mul (z w : PhiInt) : PhiInt :=
154 ⟨z.a * w.a + z.b * w.b, z.a * w.b + z.b * w.a + z.b * w.b⟩
155
156instance : Add PhiInt := ⟨PhiInt.add⟩
157instance : Neg PhiInt := ⟨PhiInt.neg⟩
158instance : Mul PhiInt := ⟨PhiInt.mul⟩
159instance : Zero PhiInt := ⟨PhiInt.zero⟩
160instance : One PhiInt := ⟨PhiInt.one⟩
161
162/-! ## §3. Ring Axioms for ℤ[φ] -/
163
164/-- **PROVED: Addition is commutative.** -/
165theorem PhiInt.add_comm (z w : PhiInt) : z + w = w + z := by
166 cases z with
167 | mk a b =>
168 cases w with
169 | mk c d =>
170 ext
171 · change a + c = c + a
172 omega
173 · change b + d = d + b
174 omega
175
176/-- **PROVED: Addition is associative.** -/
177theorem PhiInt.add_assoc (z w v : PhiInt) : z + w + v = z + (w + v) := by
178 cases z with
179 | mk a b =>
180 cases w with
181 | mk c d =>
182 cases v with
183 | mk e f =>
184 ext
185 · change (a + c) + e = a + (c + e)
186 omega
187 · change (b + d) + f = b + (d + f)
188 omega
189
190/-- **PROVED: Zero is additive identity.** -/
191theorem PhiInt.add_zero (z : PhiInt) : z + 0 = z := by
192 cases z with
193 | mk a b =>
194 ext
195 · change a + 0 = a
196 omega
197 · change b + 0 = b
198 omega
199
200/-- **PROVED: Negation gives additive inverse.** -/
201theorem PhiInt.add_neg (z : PhiInt) : z + (-z) = 0 := by
202 cases z with
203 | mk a b =>
204 ext
205 · change a + -a = 0
206 omega
207 · change b + -b = 0
208 omega
209
210/-- **PROVED: Multiplication is commutative.** -/
211theorem PhiInt.mul_comm (z w : PhiInt) : z * w = w * z := by
212 cases z with
213-- ... 209 more lines elided ...