IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.IntegerRational
IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/IntegerRational.lean · 1720 lines · 175 declarations
show as:
view math explainer →
1/-
2 PrimitiveRecognitionCalculus/IntegerRational.lean
3
4 Round-trip source:
5 PRC_Kernel_Spec_20260526.html
6
7 Spec anchors:
8 K4.6, K4.7, K4.8, K4.9, K4.10, A5
9
10 Quotient-native PRC integers and rationals. The equivalence relations are
11 internal:
12
13 - PRCInt: signed orbits identified by balanced orbit length,
14 a.pos + b.neg = b.pos + a.neg.
15 - PRCRat: ratio orbits identified by cross-multiplication of the
16 signed numerator by the denominator,
17 a.num · b.den ~ b.num · a.den (balanced equality of SignedOrbits).
18
19 The maps to verifier `ℤ` and `ℚ` are conservative displays, not
20 definitional.
21-/
22
23import Mathlib
24import IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.Orbit
25import IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.OrbitArithmetic
26
27namespace IndisputableMonolith
28namespace Foundation
29namespace PrimitiveRecognitionCalculus
30
31namespace DistinctionNat
32
33/-! ## Internal comparison support for signed-orbit order -/
34
35/-- Truncated subtraction on finite δ-orbit positions. -/
36def truncatedSub : DistinctionNat → DistinctionNat → DistinctionNat
37 | a, zero => a
38 | zero, succ _ => zero
39 | succ a, succ b => truncatedSub a b
40
41/-- Boolean `≤` on finite δ-orbit positions, by structural recursion only. -/
42def leq : DistinctionNat → DistinctionNat → Bool
43 | zero, _ => true
44 | succ _, zero => false
45 | succ a, succ b => leq a b
46
47/-- Absolute difference of two finite δ-orbit positions. -/
48def absDiff (a b : DistinctionNat) : DistinctionNat :=
49 truncatedSub a b + truncatedSub b a
50
51/-- Verifier display of internal truncated subtraction. -/
52theorem toNat_truncatedSub (a b : DistinctionNat) :
53 (truncatedSub a b).toNat = a.toNat - b.toNat := by
54 induction a generalizing b with
55 | zero =>
56 cases b with
57 | zero => rfl
58 | succ b => simp [truncatedSub]
59 | succ a ih =>
60 cases b with
61 | zero => rfl
62 | succ b =>
63 simp [truncatedSub, ih]
64
65/-- Internal Boolean order agrees with the verifier `Nat` order.
66 Choice-free: the proof uses only structural recursion and the successor
67 order lemma, so its axiom footprint is `[propext]` (audit tier FORCED). -/
68theorem leq_eq_true_iff (a b : DistinctionNat) :
69 leq a b = true ↔ a.toNat ≤ b.toNat := by
70 induction a generalizing b with
71 | zero =>
72 cases b with
73 | zero => exact ⟨fun _ => Nat.le_refl 0, fun _ => rfl⟩
74 | succ b => exact ⟨fun _ => Nat.zero_le _, fun _ => rfl⟩
75 | succ a ih =>
76 cases b with
77 | zero =>
78 show (false = true) ↔ (toNat a).succ ≤ (0 : Nat)
79 exact ⟨fun h => Bool.noConfusion h,
80 fun h => absurd h (Nat.not_succ_le_zero _)⟩
81 | succ b =>
82 show leq a b = true ↔ (toNat a).succ ≤ (toNat b).succ
83 rw [ih, Nat.succ_le_succ_iff]
84
85/-- Internal Boolean order is false exactly when verifier order is reversed. -/
86theorem leq_eq_false_iff (a b : DistinctionNat) :
87 leq a b = false ↔ b.toNat < a.toNat := by
88 rw [← Bool.not_eq_true, leq_eq_true_iff]
89 omega
90
91/-- Verifier display of internal absolute difference. -/
92theorem toNat_absDiff (a b : DistinctionNat) :
93 (absDiff a b).toNat =
94 Int.natAbs ((a.toNat : ℤ) - (b.toNat : ℤ)) := by
95 unfold absDiff
96 rw [toNat_add, toNat_truncatedSub, toNat_truncatedSub]
97 by_cases h : b.toNat ≤ a.toNat
98 · have hzero : b.toNat - a.toNat = 0 := Nat.sub_eq_zero_of_le h
99 rw [hzero, Nat.add_zero]
100 have hnonneg : 0 ≤ (a.toNat : ℤ) - (b.toNat : ℤ) := by
101 omega
102 have hcast : ((Int.natAbs ((a.toNat : ℤ) - (b.toNat : ℤ)) : ℤ) =
103 (a.toNat : ℤ) - (b.toNat : ℤ)) := by
104 rw [Int.natAbs_of_nonneg hnonneg]
105 apply Nat.cast_injective (R := ℤ)
106 rw [hcast]
107 omega
108 · have hle : a.toNat ≤ b.toNat := by omega
109 have hzero : a.toNat - b.toNat = 0 := Nat.sub_eq_zero_of_le hle
110 rw [hzero, Nat.zero_add]
111 have hnonpos : (a.toNat : ℤ) - (b.toNat : ℤ) ≤ 0 := by
112 omega
113 have hcast : ((Int.natAbs ((a.toNat : ℤ) - (b.toNat : ℤ)) : ℤ) =
114 -((a.toNat : ℤ) - (b.toNat : ℤ))) := by
115 have hneg_nonneg : 0 ≤ -((a.toNat : ℤ) - (b.toNat : ℤ)) := by
116 omega
117 have hneg_abs : ((Int.natAbs (-((a.toNat : ℤ) - (b.toNat : ℤ))) : ℤ) =
118 -((a.toNat : ℤ) - (b.toNat : ℤ))) := by
119 rw [Int.natAbs_of_nonneg hneg_nonneg]
120 rwa [Int.natAbs_neg] at hneg_abs
121 apply Nat.cast_injective (R := ℤ)
122 rw [hcast]
123 omega
124
125end DistinctionNat
126
127/-! ## Signed orbits and the balanced-length equivalence -/
128
129/-- K4.6. A signed orbit difference. Intended meaning: `pos - neg`. -/
130structure SignedOrbit where
131 pos : DistinctionNat
132 neg : DistinctionNat
133 deriving DecidableEq, Repr
134
135namespace SignedOrbit
136
137/-- A verifier display of a signed orbit as an integer. -/
138def toInt (z : SignedOrbit) : ℤ :=
139 (z.pos.toNat : ℤ) - (z.neg.toNat : ℤ)
140
141@[simp] theorem toInt_mk (a b : DistinctionNat) :
142 toInt ⟨a, b⟩ = (a.toNat : ℤ) - (b.toNat : ℤ) := by
143 rfl
144
145/-- The zero signed orbit. -/
146def zero : SignedOrbit :=
147 ⟨DistinctionNat.zero, DistinctionNat.zero⟩
148
149@[simp] theorem zero_toInt :
150 zero.toInt = 0 := by
151 rfl
152
153/-- The unit signed orbit. -/
154def one : SignedOrbit :=
155 ⟨DistinctionNat.succ DistinctionNat.zero, DistinctionNat.zero⟩
156
157@[simp] theorem one_toInt :
158 one.toInt = 1 := by
159 rfl
160
161/-- A nonnegative signed orbit built from a δ-orbit position. -/
162def ofOrbit (n : DistinctionNat) : SignedOrbit :=
163 ⟨n, DistinctionNat.zero⟩
164
165@[simp] theorem ofOrbit_toInt (n : DistinctionNat) :
166 (ofOrbit n).toInt = n.toNat := by
167 show (n.toNat : ℤ) - 0 = n.toNat
168 ring
169
170/-- Pointwise addition of signed orbits. -/
171def add (a b : SignedOrbit) : SignedOrbit where
172 pos := a.pos + b.pos
173 neg := a.neg + b.neg
174
175@[simp] theorem add_pos (a b : SignedOrbit) :
176 (add a b).pos = a.pos + b.pos := rfl
177
178@[simp] theorem add_neg (a b : SignedOrbit) :
179 (add a b).neg = a.neg + b.neg := rfl
180
181theorem add_toInt (a b : SignedOrbit) :
182 (add a b).toInt = a.toInt + b.toInt := by
183 show ((a.pos + b.pos).toNat : ℤ) - ((a.neg + b.neg).toNat : ℤ) =
184 ((a.pos.toNat : ℤ) - (a.neg.toNat : ℤ)) +
185 ((b.pos.toNat : ℤ) - (b.neg.toNat : ℤ))
186 rw [DistinctionNat.toNat_add, DistinctionNat.toNat_add]
187 push_cast
188 ring
189
190/-- Pointwise negation of signed orbits: swap pos and neg. Named
191`negate` rather than `neg` to avoid collision with the structure field. -/
192def negate (a : SignedOrbit) : SignedOrbit where
193 pos := a.neg
194 neg := a.pos
195
196@[simp] theorem negate_pos (a : SignedOrbit) :
197 (negate a).pos = a.neg := rfl
198
199@[simp] theorem negate_neg (a : SignedOrbit) :
200 (negate a).neg = a.pos := rfl
201
202theorem negate_toInt (a : SignedOrbit) :
203 (negate a).toInt = -a.toInt := by
204 show (a.neg.toNat : ℤ) - (a.pos.toNat : ℤ) =
205 -((a.pos.toNat : ℤ) - (a.neg.toNat : ℤ))
206 ring
207
208/-- Signed orbit multiplication:
209`(p₁ − n₁) · (p₂ − n₂) = (p₁p₂ + n₁n₂) − (p₁n₂ + n₁p₂)`. -/
210def mul (a b : SignedOrbit) : SignedOrbit where
211 pos := a.pos * b.pos + a.neg * b.neg
212 neg := a.pos * b.neg + a.neg * b.pos
213
214@[simp] theorem mul_pos (a b : SignedOrbit) :
215 (mul a b).pos = a.pos * b.pos + a.neg * b.neg := rfl
216
217@[simp] theorem mul_neg (a b : SignedOrbit) :
218 (mul a b).neg = a.pos * b.neg + a.neg * b.pos := rfl
219
220theorem mul_toInt (a b : SignedOrbit) :
221 (mul a b).toInt = a.toInt * b.toInt := by
222 show ((a.pos * b.pos + a.neg * b.neg).toNat : ℤ) -
223 ((a.pos * b.neg + a.neg * b.pos).toNat : ℤ) =
224 ((a.pos.toNat : ℤ) - (a.neg.toNat : ℤ)) *
225 ((b.pos.toNat : ℤ) - (b.neg.toNat : ℤ))
226 rw [DistinctionNat.toNat_add, DistinctionNat.toNat_add,
227 DistinctionNat.toNat_mul, DistinctionNat.toNat_mul,
228 DistinctionNat.toNat_mul, DistinctionNat.toNat_mul]
229 push_cast
230 ring
231
232/-- Subtraction on signed orbits via the negation. -/
233def sub (a b : SignedOrbit) : SignedOrbit :=
234 add a (negate b)
235
236theorem sub_toInt (a b : SignedOrbit) :
237 (sub a b).toInt = a.toInt - b.toInt := by
238 show (add a (negate b)).toInt = a.toInt - b.toInt
239 rw [add_toInt, negate_toInt]
240 ring
241
242/-- Scale a signed orbit by a (positive-only) orbit position. -/
243def scaleByNat (z : SignedOrbit) (d : DistinctionNat) : SignedOrbit where
244 pos := z.pos * d
245 neg := z.neg * d
246
247@[simp] theorem scaleByNat_pos (z : SignedOrbit) (d : DistinctionNat) :
248 (z.scaleByNat d).pos = z.pos * d := rfl
249
250@[simp] theorem scaleByNat_neg (z : SignedOrbit) (d : DistinctionNat) :
251 (z.scaleByNat d).neg = z.neg * d := rfl
252
253theorem scaleByNat_toInt (z : SignedOrbit) (d : DistinctionNat) :
254 (z.scaleByNat d).toInt = z.toInt * (d.toNat : ℤ) := by
255 show ((z.pos * d).toNat : ℤ) - ((z.neg * d).toNat : ℤ) =
256 ((z.pos.toNat : ℤ) - (z.neg.toNat : ℤ)) * (d.toNat : ℤ)
257 rw [DistinctionNat.toNat_mul, DistinctionNat.toNat_mul]
258 push_cast
259 ring
260
261/-! ### K4.9. Balanced-length equivalence -/
262
263/-- K4.9. Two signed orbits are equivalent when their orbit lengths balance:
264`a.pos + b.neg = b.pos + a.neg`. This is the internal PRC integer relation,
265defined entirely on δ-orbit positions. -/
266def balanced (a b : SignedOrbit) : Prop :=
267 a.pos + b.neg = b.pos + a.neg
268
269instance instDecidableBalanced (a b : SignedOrbit) :
270 Decidable (balanced a b) := by
271 unfold balanced
272 infer_instance
273
274/-- K4.9. Characterization of balanced length by Nat-level addition. -/
275theorem balanced_iff_toNat_eq (a b : SignedOrbit) :
276 balanced a b ↔
277 a.pos.toNat + b.neg.toNat = b.pos.toNat + a.neg.toNat := by
278 unfold balanced
279 constructor
280 · intro h
281 have := congrArg DistinctionNat.toNat h
282 rwa [DistinctionNat.toNat_add, DistinctionNat.toNat_add] at this
283 · intro h
284 apply DistinctionNat.toNat_inj
285 rw [DistinctionNat.toNat_add, DistinctionNat.toNat_add]
286 exact h
287
288/-- K4.9. The balanced characterization agrees with the verifier integer
289display. This is the bridge from the internal PRC relation to the
290conservative `ℤ` view. -/
291theorem balanced_iff_toInt_eq (a b : SignedOrbit) :
292 balanced a b ↔ a.toInt = b.toInt := by
293 rw [balanced_iff_toNat_eq]
294 unfold SignedOrbit.toInt
295 -- choice-free: split the iff into two implications, omega each direction
296 -- (omega on a bare iff goal pulls Classical.choice; per-direction it does not)
297 constructor
298 · intro h; omega
299 · intro h; omega
300
301theorem balanced_refl (a : SignedOrbit) : balanced a a := by
302 unfold balanced
303 rw [DistinctionNat.add_comm]
304
305theorem balanced_symm {a b : SignedOrbit} (h : balanced a b) :
306 balanced b a := by
307 unfold balanced at *
308 exact h.symm
309
310theorem balanced_trans {a b c : SignedOrbit}
311 (hab : balanced a b) (hbc : balanced b c) : balanced a c := by
312 rw [balanced_iff_toNat_eq] at hab hbc ⊢
313 omega
314
315theorem balanced_equivalence : Equivalence balanced := {
316 refl := balanced_refl
317 symm := balanced_symm
318 trans := balanced_trans
319}
320
321/-! ### K4.13. Signed-orbit order and absolute value -/
322
323/-- Internal nonnegativity: a signed orbit balances with a positive orbit. -/
324def nonneg (z : SignedOrbit) : Prop :=
325 ∃ k : DistinctionNat, SignedOrbit.balanced z (SignedOrbit.ofOrbit k)
326
327/-- Computable nonnegative flag from structural comparison of the two sides. -/
328def nonnegFlag (z : SignedOrbit) : Bool :=
329 DistinctionNat.leq z.neg z.pos
330
331/-- Strict negativity as failure of the structural nonnegative flag. -/
332def negativeFlag (z : SignedOrbit) : Bool :=
333 !z.nonnegFlag
334
335/-- Internal signed-orbit order: `a ≤ b` when `b - a` is nonnegative. -/
336def le (a b : SignedOrbit) : Prop :=
337 nonneg (SignedOrbit.sub b a)
338
339/-- Internal strict order: nonnegative difference with nonzero difference. -/
340def lt (a b : SignedOrbit) : Prop :=
341 le a b ∧ ¬ SignedOrbit.balanced a b
342
343/-- Absolute value of a signed orbit as an orbit position. -/
344def abs (z : SignedOrbit) : DistinctionNat :=
345 DistinctionNat.absDiff z.pos z.neg
346
347theorem nonnegFlag_eq_true_iff (z : SignedOrbit) :
348 z.nonnegFlag = true ↔ 0 ≤ z.toInt := by
349 unfold nonnegFlag SignedOrbit.toInt
350 rw [DistinctionNat.leq_eq_true_iff]
351 constructor
352 · intro h; omega
353 · intro h; omega
354
355theorem nonnegFlag_eq_false_iff (z : SignedOrbit) :
356 z.nonnegFlag = false ↔ z.toInt < 0 := by
357 rw [← Bool.not_eq_true, nonnegFlag_eq_true_iff]
358 constructor
359 · intro h; omega
360 · intro h; omega
361
362/-- Internal nonnegativity agrees with the verifier integer display. -/
363theorem nonneg_iff_toInt_nonneg (z : SignedOrbit) :
364 nonneg z ↔ 0 ≤ z.toInt := by
365 constructor
366 · intro h
367 rcases h with ⟨k, hk⟩
368 have hdisplay := (SignedOrbit.balanced_iff_toInt_eq z (SignedOrbit.ofOrbit k)).mp hk
369 rw [SignedOrbit.ofOrbit_toInt] at hdisplay
370 omega
371 · intro hz
372 refine ⟨DistinctionNat.ofNat z.toInt.toNat, ?_⟩
373 rw [SignedOrbit.balanced_iff_toInt_eq, SignedOrbit.ofOrbit_toInt,
374 DistinctionNat.toNat_ofNat]
375 omega
376
377/-- The structural nonnegative flag is equivalent to internal nonnegativity. -/
378theorem nonnegFlag_eq_true_iff_nonneg (z : SignedOrbit) :
379 z.nonnegFlag = true ↔ nonneg z := by
380 rw [nonnegFlag_eq_true_iff, nonneg_iff_toInt_nonneg]
381
382theorem negativeFlag_eq_true_iff_toInt_neg (z : SignedOrbit) :
383 z.negativeFlag = true ↔ z.toInt < 0 := by
384 unfold negativeFlag
385 by_cases h : z.nonnegFlag = true
386 · rw [h]
387 simp
388 rw [nonnegFlag_eq_true_iff] at h
389 omega
390 · have hf : z.nonnegFlag = false := by
391 cases hflag : z.nonnegFlag with
392 | false => rfl
393 | true =>
394 exfalso
395 exact h hflag
396 rw [hf]
397 simp
398 exact (nonnegFlag_eq_false_iff z).mp hf
399
400/-- Verifier display of internal absolute value. -/
401theorem abs_toNat (z : SignedOrbit) :
402 z.abs.toNat = Int.natAbs z.toInt := by
403 unfold abs SignedOrbit.toInt
404 exact DistinctionNat.toNat_absDiff z.pos z.neg
405
406theorem abs_eq_zero_iff_toInt_eq_zero (z : SignedOrbit) :
407 z.abs = DistinctionNat.zero ↔ z.toInt = 0 := by
408 constructor
409 · intro h
410 have hnat : z.abs.toNat = 0 := by
411 rw [h, DistinctionNat.toNat_zero]
412 rw [abs_toNat] at hnat
413 exact Int.natAbs_eq_zero.mp hnat
414 · intro h
415 apply DistinctionNat.toNat_inj
416 rw [abs_toNat, h, Int.natAbs_zero, DistinctionNat.toNat_zero]
417
418theorem abs_ne_zero_of_toInt_ne_zero {z : SignedOrbit}
419 (h : z.toInt ≠ 0) :
420 z.abs ≠ DistinctionNat.zero := by
421 intro hz
422 exact h ((abs_eq_zero_iff_toInt_eq_zero z).mp hz)
423
424theorem abs_ne_zero_of_not_balanced_zero {z : SignedOrbit}
425 (h : ¬ SignedOrbit.balanced z SignedOrbit.zero) :
426 z.abs ≠ DistinctionNat.zero := by
427 apply abs_ne_zero_of_toInt_ne_zero
428 intro hz
429 exact h ((SignedOrbit.balanced_iff_toInt_eq z SignedOrbit.zero).mpr (by
430 rw [hz, SignedOrbit.zero_toInt]))
431
432theorem le_iff_toInt_le (a b : SignedOrbit) :
433 le a b ↔ a.toInt ≤ b.toInt := by
434 unfold le
435 rw [nonneg_iff_toInt_nonneg, SignedOrbit.sub_toInt]
436 constructor <;> intro h <;> omega
437
438theorem lt_iff_toInt_lt (a b : SignedOrbit) :
439 lt a b ↔ a.toInt < b.toInt := by
440 unfold lt
441 rw [le_iff_toInt_le, SignedOrbit.balanced_iff_toInt_eq]
442 exact ⟨fun h => by omega, fun h => ⟨by omega, by omega⟩⟩
443
444end SignedOrbit
445
446/-- K4.9. Signed-orbit equivalence is the balanced-length relation. -/
447def signedOrbitEquiv (a b : SignedOrbit) : Prop :=
448 SignedOrbit.balanced a b
449
450theorem signedOrbitEquiv_equivalence :
451 Equivalence signedOrbitEquiv :=
452 SignedOrbit.balanced_equivalence
453
454theorem signedOrbitEquiv_iff_toInt_eq (a b : SignedOrbit) :
455 signedOrbitEquiv a b ↔ a.toInt = b.toInt :=
456 SignedOrbit.balanced_iff_toInt_eq a b
457
458/-- K4.8. Setoid for quotient-native PRC integers. -/
459def signedOrbitSetoid : Setoid SignedOrbit where
460 r := signedOrbitEquiv
461 iseqv := signedOrbitEquiv_equivalence
462
463/-- K4.8. PRC integers as signed-orbit quotient classes. The quotient is
464taken by the internal balanced-length relation; the verifier display into
465`ℤ` is a downstream theorem. -/
466def PRCInt : Type :=
467 Quot signedOrbitSetoid
468
469namespace PRCInt
470
471/-- K4.8. Constructor from a signed orbit display. -/
472def mk (z : SignedOrbit) : PRCInt :=
473 Quot.mk signedOrbitSetoid z
474
475/-- K4.8/A5. Conservative verifier display of a PRC integer as `ℤ`. -/
476def toInt : PRCInt → ℤ :=
477 Quot.lift SignedOrbit.toInt (by
478 intro a b h
479 exact (signedOrbitEquiv_iff_toInt_eq a b).mp h)
480
481@[simp] theorem toInt_mk (z : SignedOrbit) :
482 toInt (mk z) = z.toInt := by
483 rfl
484
485/-- K4.8. The zero PRC integer. -/
486def zero : PRCInt :=
487 mk SignedOrbit.zero
488
489@[simp] theorem zero_toInt :
490 zero.toInt = 0 := by
491 rfl
492
493/-- K4.8. The unit PRC integer. -/
494def one : PRCInt :=
495 mk SignedOrbit.one
496
497@[simp] theorem one_toInt :
498 one.toInt = 1 := by
499 rfl
500
501/-- K4.8. Equal balanced signed orbits determine equal PRC integers. -/
502theorem mk_eq_mk_of_balanced {a b : SignedOrbit}
503 (h : SignedOrbit.balanced a b) :
504 mk a = mk b :=
505 Quot.sound h
506
507/-! ### PRCInt operations -/
508
509/-- Addition respects balanced equivalence. -/
510private theorem add_respects_balanced {a₁ a₂ b₁ b₂ : SignedOrbit}
511 (ha : SignedOrbit.balanced a₁ a₂) (hb : SignedOrbit.balanced b₁ b₂) :
512 SignedOrbit.balanced (SignedOrbit.add a₁ b₁) (SignedOrbit.add a₂ b₂) := by
513 rw [SignedOrbit.balanced_iff_toInt_eq] at *
514 rw [SignedOrbit.add_toInt, SignedOrbit.add_toInt, ha, hb]
515
516/-- K4.8. Addition on PRC integers, lifted from signed-orbit addition. -/
517def add : PRCInt → PRCInt → PRCInt :=
518 Quot.lift₂
519 (fun a b => mk (SignedOrbit.add a b))
520 (by
521 intro a b₁ b₂ h
522 apply Quot.sound
523 exact add_respects_balanced (SignedOrbit.balanced_refl a) h)
524 (by
525 intro a₁ a₂ b h
526 apply Quot.sound
527 exact add_respects_balanced h (SignedOrbit.balanced_refl b))
528
529@[simp] theorem add_mk (a b : SignedOrbit) :
530 add (mk a) (mk b) = mk (SignedOrbit.add a b) := by
531 rfl
532
533@[simp] theorem toInt_add (a b : PRCInt) :
534 (add a b).toInt = a.toInt + b.toInt := by
535 refine Quot.induction_on a (fun a => ?_)
536 refine Quot.induction_on b (fun b => ?_)
537 show (SignedOrbit.add a b).toInt = a.toInt + b.toInt
538 exact SignedOrbit.add_toInt a b
539
540/-- Negation respects balanced equivalence. -/
541private theorem negate_respects_balanced {a₁ a₂ : SignedOrbit}
542 (h : SignedOrbit.balanced a₁ a₂) :
543 SignedOrbit.balanced (SignedOrbit.negate a₁) (SignedOrbit.negate a₂) := by
544 rw [SignedOrbit.balanced_iff_toInt_eq] at *
545 rw [SignedOrbit.negate_toInt, SignedOrbit.negate_toInt, h]
546
547/-- K4.8. Negation on PRC integers, lifted from signed-orbit swap. -/
548def negate : PRCInt → PRCInt :=
549 Quot.lift
550 (fun a => mk (SignedOrbit.negate a))
551 (by
552 intro a b h
553 apply Quot.sound
554 exact negate_respects_balanced h)
555
556@[simp] theorem negate_mk (a : SignedOrbit) :
557 negate (mk a) = mk (SignedOrbit.negate a) := by
558 rfl
559
560@[simp] theorem toInt_negate (a : PRCInt) :
561 (negate a).toInt = -a.toInt := by
562 refine Quot.induction_on a (fun a => ?_)
563 show (SignedOrbit.negate a).toInt = -a.toInt
564 exact SignedOrbit.negate_toInt a
565
566/-- K4.8. The toInt display is injective: distinct PRC integers have
567distinct verifier displays. -/
568theorem toInt_injective : Function.Injective toInt := by
569 intro a b h
570 induction a using Quot.ind with
571 | _ a =>
572 induction b using Quot.ind with
573 | _ b =>
574 apply Quot.sound
575 exact (signedOrbitEquiv_iff_toInt_eq a b).mpr h
576
577/-- Multiplication respects balanced equivalence. -/
578private theorem mul_respects_balanced {a₁ a₂ b₁ b₂ : SignedOrbit}
579 (ha : SignedOrbit.balanced a₁ a₂) (hb : SignedOrbit.balanced b₁ b₂) :
580 SignedOrbit.balanced (SignedOrbit.mul a₁ b₁) (SignedOrbit.mul a₂ b₂) := by
581 rw [SignedOrbit.balanced_iff_toInt_eq] at *
582 rw [SignedOrbit.mul_toInt, SignedOrbit.mul_toInt, ha, hb]
583
584/-- K4.8. Multiplication on PRC integers, lifted from signed-orbit
585multiplication. -/
586def mul : PRCInt → PRCInt → PRCInt :=
587 Quot.lift₂
588 (fun a b => mk (SignedOrbit.mul a b))
589 (by
590 intro a b₁ b₂ h
591 apply Quot.sound
592 exact mul_respects_balanced (SignedOrbit.balanced_refl a) h)
593 (by
594 intro a₁ a₂ b h
595 apply Quot.sound
596 exact mul_respects_balanced h (SignedOrbit.balanced_refl b))
597
598@[simp] theorem mul_mk (a b : SignedOrbit) :
599 mul (mk a) (mk b) = mk (SignedOrbit.mul a b) := by
600 rfl
601
602@[simp] theorem toInt_mul (a b : PRCInt) :
603 (mul a b).toInt = a.toInt * b.toInt := by
604 refine Quot.induction_on a (fun a => ?_)
605 refine Quot.induction_on b (fun b => ?_)
606 show (SignedOrbit.mul a b).toInt = a.toInt * b.toInt
607 exact SignedOrbit.mul_toInt a b
608
609/-- K4.8. Subtraction on PRC integers as add ∘ negate. -/
610def sub (a b : PRCInt) : PRCInt :=
611 add a (negate b)
612
613@[simp] theorem toInt_sub (a b : PRCInt) :
614 (sub a b).toInt = a.toInt - b.toInt := by
615 show (add a (negate b)).toInt = a.toInt - b.toInt
616 rw [toInt_add, toInt_negate]
617 ring
618
619/-! ### Ring axioms on PRC integers -/
620
621theorem add_comm (a b : PRCInt) : add a b = add b a := by
622 apply toInt_injective
623 simp [Int.add_comm]
624
625theorem add_assoc (a b c : PRCInt) :
626 add (add a b) c = add a (add b c) := by
627 apply toInt_injective
628 simp [Int.add_assoc]
629
630theorem zero_add (a : PRCInt) : add zero a = a := by
631 apply toInt_injective
632 simp
633
634theorem add_zero (a : PRCInt) : add a zero = a := by
635 apply toInt_injective
636 simp
637
638theorem add_negate (a : PRCInt) : add a (negate a) = zero := by
639 apply toInt_injective
640 simp
641
642theorem negate_add (a : PRCInt) : add (negate a) a = zero := by
643 apply toInt_injective
644 simp
645
646theorem mul_comm (a b : PRCInt) : mul a b = mul b a := by
647 apply toInt_injective
648 simp [Int.mul_comm]
649
650theorem mul_assoc (a b c : PRCInt) :
651 mul (mul a b) c = mul a (mul b c) := by
652 apply toInt_injective
653 simp [Int.mul_assoc]
654
655theorem one_mul (a : PRCInt) : mul one a = a := by
656 apply toInt_injective
657 simp
658
659theorem mul_one (a : PRCInt) : mul a one = a := by
660 apply toInt_injective
661 simp
662
663theorem zero_mul (a : PRCInt) : mul zero a = zero := by
664 apply toInt_injective
665 simp
666
667theorem mul_zero (a : PRCInt) : mul a zero = zero := by
668 apply toInt_injective
669 simp
670
671theorem left_distrib (a b c : PRCInt) :
672 mul a (add b c) = add (mul a b) (mul a c) := by
673 apply toInt_injective
674 simp [Int.mul_add]
675
676theorem right_distrib (a b c : PRCInt) :
677 mul (add a b) c = add (mul a c) (mul b c) := by
678 apply toInt_injective
679 simp [Int.add_mul]
680
681/-! ### PRCInt is isomorphic to ℤ -/
682
683/-- Construct a PRC integer from a verifier Int by routing the positive
684and negative parts through the δ-orbit. -/
685def ofInt (n : ℤ) : PRCInt :=
686 mk ⟨DistinctionNat.ofNat n.toNat, DistinctionNat.ofNat (-n).toNat⟩
687
688@[simp] theorem toInt_ofInt (n : ℤ) :
689 (ofInt n).toInt = n := by
690 show ((DistinctionNat.ofNat n.toNat).toNat : ℤ) -
691 ((DistinctionNat.ofNat (-n).toNat).toNat : ℤ) = n
692 rw [DistinctionNat.toNat_ofNat, DistinctionNat.toNat_ofNat]
693 omega
694
695@[simp] theorem ofInt_toInt (a : PRCInt) :
696 ofInt a.toInt = a := by
697 apply toInt_injective
698 rw [toInt_ofInt]
699
700/-- K4.8. The PRC integer surface is literally isomorphic to verifier `ℤ`.
701The verifier `ℤ` is therefore not assumed; it is a downstream display the
702PRC quotient happens to reproduce. -/
703def equivInt : PRCInt ≃ ℤ where
704 toFun := toInt
705 invFun := ofInt
706 left_inv := ofInt_toInt
707 right_inv := toInt_ofInt
708
709@[simp] theorem ofInt_add (m n : ℤ) :
710 ofInt (m + n) = add (ofInt m) (ofInt n) := by
711 apply toInt_injective
712 simp
713
714@[simp] theorem ofInt_mul (m n : ℤ) :
715 ofInt (m * n) = mul (ofInt m) (ofInt n) := by
716 apply toInt_injective
717 simp
718
719@[simp] theorem ofInt_neg (n : ℤ) :
720 ofInt (-n) = negate (ofInt n) := by
721 apply toInt_injective
722 simp
723
724@[simp] theorem ofInt_zero : ofInt 0 = zero := by
725 apply toInt_injective
726 simp
727
728@[simp] theorem ofInt_one : ofInt 1 = one := by
729 apply toInt_injective
730 simp
731
732end PRCInt
733
734/-! ## Operation instances on PRCInt -/
735
736namespace PRCInt
737
738instance instZero : Zero PRCInt := ⟨zero⟩
739instance instOne : One PRCInt := ⟨one⟩
740instance instAdd : Add PRCInt := ⟨add⟩
741instance instMul : Mul PRCInt := ⟨mul⟩
742instance instNeg : Neg PRCInt := ⟨negate⟩
743instance instSub : Sub PRCInt := ⟨sub⟩
744
745@[simp] theorem add_eq (a b : PRCInt) : a + b = add a b := rfl
746@[simp] theorem mul_eq (a b : PRCInt) : a * b = mul a b := rfl
747@[simp] theorem neg_eq (a : PRCInt) : -a = negate a := rfl
748@[simp] theorem sub_eq (a b : PRCInt) : a - b = sub a b := rfl
749@[simp] theorem zero_eq : (0 : PRCInt) = zero := rfl
750@[simp] theorem one_eq : (1 : PRCInt) = one := rfl
751
752/-- K4.8. The toInt display is a ring homomorphism (additive). -/
753theorem toInt_add' (a b : PRCInt) :
754 (a + b).toInt = a.toInt + b.toInt := by
755 simp
756
757/-- K4.8. The toInt display is a ring homomorphism (multiplicative). -/
758theorem toInt_mul' (a b : PRCInt) :
759 (a * b).toInt = a.toInt * b.toInt := by
760 simp
761
762/-- K4.8. The toInt display preserves negation. -/
763theorem toInt_neg' (a : PRCInt) :
764 (-a).toInt = -a.toInt := by
765 simp
766
767/-- K4.8. The toInt display preserves zero. -/
768theorem toInt_zero' : (0 : PRCInt).toInt = 0 := by
769 simp
770
771/-- K4.8. The toInt display preserves one. -/
772theorem toInt_one' : (1 : PRCInt).toInt = 1 := by
773 simp
774
775end PRCInt
776
777/-! ## Ratio orbits and cross-multiplication -/
778
779/-- K4.7. A rational orbit display: integer numerator over nonzero orbit
780denominator. -/
781structure RatioOrbit where
782 num : SignedOrbit
783 den : DistinctionNat
784 den_ne_zero : den ≠ DistinctionNat.zero
785
786namespace RatioOrbit
787
788/-- The denominator's verifier Nat is nonzero. -/
789theorem den_toNat_ne_zero (q : RatioOrbit) :
790 q.den.toNat ≠ 0 := by
791 intro h
792 have hden : DistinctionNat.ofNat q.den.toNat = DistinctionNat.ofNat 0 := by
793 rw [h]
794 rw [DistinctionNat.ofNat_toNat, DistinctionNat.ofNat_zero] at hden
795 exact q.den_ne_zero hden
796
797/-- A verifier display of a ratio orbit as a rational number.
798Spec tag A5: this is a transport wrapper. The internal characterization
799is cross-multiplication. -/
800def toRat (q : RatioOrbit) : ℚ :=
801 (q.num.toInt : ℚ) / (q.den.toNat : ℚ)
802
803/-- The denominator used by `toRat` is nonzero in the verifier rationals. -/
804theorem den_cast_ne_zero (q : RatioOrbit) :
805 (q.den.toNat : ℚ) ≠ 0 := by
806 exact_mod_cast q.den_toNat_ne_zero
807
808/-! ### Ratio-orbit arithmetic -/
809
810/-- K4.11. Zero ratio orbit. -/
811def zero : RatioOrbit where
812 num := SignedOrbit.zero
813 den := DistinctionNat.succ DistinctionNat.zero
814 den_ne_zero := by
815 intro h
816 exact DistinctionNat.zero_ne_succ DistinctionNat.zero h.symm
817
818@[simp] theorem zero_toRat :
819 zero.toRat = 0 := by
820 unfold zero toRat
821 simp
822
823/-- K4.11. Unit ratio orbit. -/
824def one : RatioOrbit where
825 num := SignedOrbit.one
826 den := DistinctionNat.succ DistinctionNat.zero
827 den_ne_zero := by
828 intro h
829 exact DistinctionNat.zero_ne_succ DistinctionNat.zero h.symm
830
831@[simp] theorem one_toRat :
832 one.toRat = 1 := by
833 unfold one toRat
834 simp
835
836/-- K4.11. Addition of ratio orbits:
837`a/b + c/d = (ad + cb)/(bd)`. -/
838def add (a b : RatioOrbit) : RatioOrbit where
839 num := SignedOrbit.add (a.num.scaleByNat b.den) (b.num.scaleByNat a.den)
840 den := a.den * b.den
841 den_ne_zero := DistinctionNat.mul_ne_zero a.den_ne_zero b.den_ne_zero
842
843theorem add_toRat (a b : RatioOrbit) :
844 (add a b).toRat = a.toRat + b.toRat := by
845 unfold add toRat
846 rw [SignedOrbit.add_toInt, SignedOrbit.scaleByNat_toInt,
847 SignedOrbit.scaleByNat_toInt, DistinctionNat.toNat_mul]
848 have hA : (a.den.toNat : ℚ) ≠ 0 := a.den_cast_ne_zero
849 have hB : (b.den.toNat : ℚ) ≠ 0 := b.den_cast_ne_zero
850 field_simp [hA, hB]
851 push_cast
852 ring_nf
853
854/-- K4.11. Negation of ratio orbits. -/
855def negate (a : RatioOrbit) : RatioOrbit where
856 num := SignedOrbit.negate a.num
857 den := a.den
858 den_ne_zero := a.den_ne_zero
859
860theorem negate_toRat (a : RatioOrbit) :
861 (negate a).toRat = -a.toRat := by
862 unfold negate toRat
863 rw [SignedOrbit.negate_toInt]
864 have hA : (a.den.toNat : ℚ) ≠ 0 := a.den_cast_ne_zero
865 field_simp [hA]
866 push_cast
867 ring_nf
868
869/-- K4.11. Subtraction of ratio orbits. -/
870def sub (a b : RatioOrbit) : RatioOrbit :=
871 add a (negate b)
872
873theorem sub_toRat (a b : RatioOrbit) :
874 (sub a b).toRat = a.toRat - b.toRat := by
875 unfold sub
876 rw [add_toRat, negate_toRat]
877 ring
878
879/-- K4.11. Multiplication of ratio orbits:
880`a/b * c/d = (ac)/(bd)`. -/
881def mul (a b : RatioOrbit) : RatioOrbit where
882 num := SignedOrbit.mul a.num b.num
883 den := a.den * b.den
884 den_ne_zero := DistinctionNat.mul_ne_zero a.den_ne_zero b.den_ne_zero
885
886theorem mul_toRat (a b : RatioOrbit) :
887 (mul a b).toRat = a.toRat * b.toRat := by
888 unfold mul toRat
889 rw [SignedOrbit.mul_toInt, DistinctionNat.toNat_mul]
890 have hA : (a.den.toNat : ℚ) ≠ 0 := a.den_cast_ne_zero
891 have hB : (b.den.toNat : ℚ) ≠ 0 := b.den_cast_ne_zero
892 field_simp [hA, hB]
893 push_cast
894 ring_nf
895
896/-- K4.12. Reciprocal of a nonzero ratio orbit.
897
898The numerator sign is selected by the structural signed-orbit comparison
899`nonnegFlag`, and the denominator is the internal signed-orbit absolute value.
900The verifier integer display is used only in the transport theorem below. -/
901def recipNonzero (a : RatioOrbit)
902 (h : ¬ SignedOrbit.balanced a.num SignedOrbit.zero) : RatioOrbit where
903 num :=
904 if a.num.nonnegFlag then
905 SignedOrbit.ofOrbit a.den
906 else
907 SignedOrbit.negate (SignedOrbit.ofOrbit a.den)
908 den := a.num.abs
909 den_ne_zero := SignedOrbit.abs_ne_zero_of_not_balanced_zero h
910
911theorem recipNonzero_toRat (a : RatioOrbit)
912 (h : ¬ SignedOrbit.balanced a.num SignedOrbit.zero) :
913 (recipNonzero a h).toRat = (a.toRat)⁻¹ := by
914 unfold recipNonzero toRat
915 have hDen : (a.den.toNat : ℚ) ≠ 0 := a.den_cast_ne_zero
916 have hNumInt : a.num.toInt ≠ 0 := by
917 intro hz
918 exact h ((SignedOrbit.balanced_iff_toInt_eq a.num SignedOrbit.zero).mpr (by
919 rw [hz, SignedOrbit.zero_toInt]))
920 have hNum : (a.num.toInt : ℚ) ≠ 0 := by exact_mod_cast hNumInt
921 by_cases hflag : a.num.nonnegFlag = true
922 · have hnonneg : 0 ≤ a.num.toInt :=
923 (SignedOrbit.nonnegFlag_eq_true_iff a.num).mp hflag
924 have hpos : 0 < a.num.toInt := by omega
925 simp [hflag, SignedOrbit.ofOrbit_toInt, SignedOrbit.abs_toNat]
926 have habs : |(a.num.toInt : ℚ)| = (a.num.toInt : ℚ) := by
927 exact abs_of_pos (by exact_mod_cast hpos)
928 rw [habs]
929 · have hflagFalse : a.num.nonnegFlag = false := by
930 cases hflag' : a.num.nonnegFlag with
931 | false => rfl
932 | true =>
933 exfalso
934 exact hflag hflag'
935 have hneg : a.num.toInt < 0 :=
936 (SignedOrbit.nonnegFlag_eq_false_iff a.num).mp hflagFalse
937 simp [hflagFalse, SignedOrbit.ofOrbit_toInt, SignedOrbit.negate_toInt,
938 SignedOrbit.abs_toNat]
939 have habs : |(a.num.toInt : ℚ)| = -(a.num.toInt : ℚ) := by
940 exact abs_of_neg (by exact_mod_cast hneg)
941 rw [habs]
942 field_simp [hDen, hNum]
943
944/-- K4.12. Total reciprocal of ratio orbits, sending zero to zero as in `ℚ`. -/
945def recip (a : RatioOrbit) : RatioOrbit :=
946 if h : SignedOrbit.balanced a.num SignedOrbit.zero then
947 zero
948 else
949 recipNonzero a h
950
951theorem recip_toRat (a : RatioOrbit) :
952 (recip a).toRat = (a.toRat)⁻¹ := by
953 unfold recip
954 by_cases h : SignedOrbit.balanced a.num SignedOrbit.zero
955 · have hzero := (SignedOrbit.balanced_iff_toInt_eq a.num SignedOrbit.zero).mp h
956 simp [h, hzero, toRat, zero]
957 · simp [h, recipNonzero_toRat]
958
959/-! ### K4.10. Cross-multiplication equivalence -/
960
961/-- K4.10. Two ratio orbits are equivalent under cross-multiplication when
962`a.num · b.den` balances `b.num · a.den` as signed orbits. This is the
963internal PRC rational relation, defined entirely on δ-orbit positions. -/
964def crossEq (a b : RatioOrbit) : Prop :=
965 SignedOrbit.balanced (a.num.scaleByNat b.den) (b.num.scaleByNat a.den)
966
967/-- K4.10. Cross-multiplication agrees with rational equality of the
968verifier displays. -/
969theorem crossEq_iff_toRat_eq (a b : RatioOrbit) :
970 crossEq a b ↔ a.toRat = b.toRat := by
971 unfold crossEq toRat
972 rw [SignedOrbit.balanced_iff_toInt_eq]
973 rw [SignedOrbit.scaleByNat_toInt, SignedOrbit.scaleByNat_toInt]
974 have hA : (a.den.toNat : ℚ) ≠ 0 := a.den_cast_ne_zero
975 have hB : (b.den.toNat : ℚ) ≠ 0 := b.den_cast_ne_zero
976 constructor
977 · intro h
978 field_simp
979 have hQ : (a.num.toInt : ℚ) * (b.den.toNat : ℚ) =
980 (b.num.toInt : ℚ) * (a.den.toNat : ℚ) := by exact_mod_cast h
981 linarith
982 · intro h
983 have : (a.num.toInt : ℚ) * (b.den.toNat : ℚ) =
984 (b.num.toInt : ℚ) * (a.den.toNat : ℚ) := by
985 field_simp at h
986 linarith
987 have hZ : (a.num.toInt * b.den.toNat : ℤ) =
988 (b.num.toInt * a.den.toNat : ℤ) := by exact_mod_cast this
989 exact hZ
990
991/-- K4.10. Choice-free integer-level characterization of cross-multiplication:
992`crossEq a b` holds iff the integer cross products agree. Unlike the ℚ-display
993bridge `crossEq_iff_toRat_eq` (which routes through Mathlib's rational field and
994so consumes `Classical.choice`), this stays in ℤ and depends only on
995`{propext, Quot.sound}`. It is the choice-free hub the PRC-rational operations
996prove respect-of-equivalence through. -/
997theorem crossEq_iff_toIntCross (a b : RatioOrbit) :
998 crossEq a b ↔
999 a.num.toInt * (b.den.toNat : ℤ) = b.num.toInt * (a.den.toNat : ℤ) := by
1000 unfold crossEq
1001 rw [SignedOrbit.balanced_iff_toInt_eq, SignedOrbit.scaleByNat_toInt,
1002 SignedOrbit.scaleByNat_toInt]
1003
1004theorem crossEq_refl (a : RatioOrbit) : crossEq a a := by
1005 unfold crossEq
1006 exact SignedOrbit.balanced_refl _
1007
1008theorem crossEq_symm {a b : RatioOrbit} (h : crossEq a b) : crossEq b a := by
1009 unfold crossEq at *
1010 exact SignedOrbit.balanced_symm h
1011
1012theorem crossEq_trans {a b c : RatioOrbit}
1013 (hab : crossEq a b) (hbc : crossEq b c) : crossEq a c := by
1014 -- choice-free: route through the integer bridge, cancel the (nonzero) middle
1015 -- denominator with the Int-specific lemma, close the polynomial identity with
1016 -- linear_combination. (The ℚ-display route uses Classical.choice.)
1017 rw [crossEq_iff_toIntCross] at hab hbc ⊢
1018 have hdb : (b.den.toNat : ℤ) ≠ 0 := by have := b.den_toNat_ne_zero; omega
1019 apply Int.eq_of_mul_eq_mul_right hdb
1020 linear_combination (c.den.toNat : ℤ) * hab + (a.den.toNat : ℤ) * hbc
1021
1022theorem crossEq_equivalence : Equivalence crossEq := {
1023 refl := crossEq_refl
1024 symm := crossEq_symm
1025 trans := crossEq_trans
1026}
1027
1028end RatioOrbit
1029
1030/-- K4.8. Ratio-orbit equivalence is cross-multiplication. -/
1031def ratioOrbitEquiv (a b : RatioOrbit) : Prop :=
1032 RatioOrbit.crossEq a b
1033
1034theorem ratioOrbitEquiv_equivalence :
1035 Equivalence ratioOrbitEquiv :=
1036 RatioOrbit.crossEq_equivalence
1037
1038theorem ratioOrbitEquiv_iff_toRat_eq (a b : RatioOrbit) :
1039 ratioOrbitEquiv a b ↔ a.toRat = b.toRat :=
1040 RatioOrbit.crossEq_iff_toRat_eq a b
1041
1042/-- K4.8. Setoid for quotient-native PRC rationals. -/
1043def ratioOrbitSetoid : Setoid RatioOrbit where
1044 r := ratioOrbitEquiv
1045 iseqv := ratioOrbitEquiv_equivalence
1046
1047/-- K4.8. PRC rationals as nonzero-denominator ratio-orbit quotient classes,
1048identified by cross-multiplication of orbit-level numerator and denominator. -/
1049def PRCRat : Type :=
1050 Quot ratioOrbitSetoid
1051
1052namespace PRCRat
1053
1054/-- K4.8. Constructor from a ratio orbit display. -/
1055def mk (q : RatioOrbit) : PRCRat :=
1056 Quot.mk ratioOrbitSetoid q
1057
1058/-- K4.8/A5. Conservative verifier display of a PRC rational as `ℚ`. -/
1059def toRat : PRCRat → ℚ :=
1060 Quot.lift RatioOrbit.toRat (by
1061 intro a b h
1062 exact (ratioOrbitEquiv_iff_toRat_eq a b).mp h)
1063
1064@[simp] theorem toRat_mk (q : RatioOrbit) :
1065 toRat (mk q) = q.toRat := by
1066 rfl
1067
1068/-- K4.8. Equal cross-multiplied ratio orbits determine equal PRC rationals. -/
1069theorem mk_eq_mk_of_crossEq {a b : RatioOrbit}
1070 (h : RatioOrbit.crossEq a b) :
1071 mk a = mk b :=
1072 Quot.sound h
1073
1074/-- K4.8. The toRat display is injective on the quotient. -/
1075theorem toRat_injective : Function.Injective toRat := by
1076 intro a b h
1077 induction a using Quot.ind with
1078 | _ a =>
1079 induction b using Quot.ind with
1080 | _ b =>
1081 apply Quot.sound
1082 exact (ratioOrbitEquiv_iff_toRat_eq a b).mpr h
1083
1084/-! ### PRCRat operations -/
1085
1086/-- K4.11. Zero PRC rational. -/
1087def zero : PRCRat :=
1088 mk RatioOrbit.zero
1089
1090@[simp] theorem zero_toRat :
1091 zero.toRat = 0 := by
1092 exact RatioOrbit.zero_toRat
1093
1094/-- K4.11. Unit PRC rational. -/
1095def one : PRCRat :=
1096 mk RatioOrbit.one
1097
1098@[simp] theorem one_toRat :
1099 one.toRat = 1 := by
1100 exact RatioOrbit.one_toRat
1101
1102private theorem add_respects_cross {a₁ a₂ b₁ b₂ : RatioOrbit}
1103 (ha : RatioOrbit.crossEq a₁ a₂) (hb : RatioOrbit.crossEq b₁ b₂) :
1104 RatioOrbit.crossEq (RatioOrbit.add a₁ b₁) (RatioOrbit.add a₂ b₂) := by
1105 rw [RatioOrbit.crossEq_iff_toIntCross] at ha hb ⊢
1106 unfold RatioOrbit.add
1107 simp only [SignedOrbit.add_toInt, SignedOrbit.scaleByNat_toInt, DistinctionNat.toNat_mul]
1108 push_cast
1109 linear_combination (b₁.den.toNat : ℤ) * (b₂.den.toNat : ℤ) * ha
1110 + (a₁.den.toNat : ℤ) * (a₂.den.toNat : ℤ) * hb
1111
1112/-- K4.11. Addition on PRC rationals, lifted from ratio-orbit addition. -/
1113def add : PRCRat → PRCRat → PRCRat :=
1114 Quot.lift₂
1115 (fun a b => mk (RatioOrbit.add a b))
1116 (by
1117 intro a b₁ b₂ h
1118 apply Quot.sound
1119 exact add_respects_cross (RatioOrbit.crossEq_refl a) h)
1120 (by
1121 intro a₁ a₂ b h
1122 apply Quot.sound
1123 exact add_respects_cross h (RatioOrbit.crossEq_refl b))
1124
1125@[simp] theorem add_mk (a b : RatioOrbit) :
1126 add (mk a) (mk b) = mk (RatioOrbit.add a b) := by
1127 rfl
1128
1129@[simp] theorem toRat_add (a b : PRCRat) :
1130 (add a b).toRat = a.toRat + b.toRat := by
1131 refine Quot.induction_on a (fun a => ?_)
1132 refine Quot.induction_on b (fun b => ?_)
1133 show (RatioOrbit.add a b).toRat = a.toRat + b.toRat
1134 exact RatioOrbit.add_toRat a b
1135
1136private theorem negate_respects_cross {a b : RatioOrbit}
1137 (h : RatioOrbit.crossEq a b) :
1138 RatioOrbit.crossEq (RatioOrbit.negate a) (RatioOrbit.negate b) := by
1139 rw [RatioOrbit.crossEq_iff_toIntCross] at h ⊢
1140 unfold RatioOrbit.negate
1141 simp only [SignedOrbit.negate_toInt]
1142 linear_combination -h
1143
1144/-- K4.11. Negation on PRC rationals. -/
1145def negate : PRCRat → PRCRat :=
1146 Quot.lift
1147 (fun a => mk (RatioOrbit.negate a))
1148 (by
1149 intro a b h
1150 apply Quot.sound
1151 exact negate_respects_cross h)
1152
1153@[simp] theorem negate_mk (a : RatioOrbit) :
1154 negate (mk a) = mk (RatioOrbit.negate a) := by
1155 rfl
1156
1157@[simp] theorem toRat_negate (a : PRCRat) :
1158 (negate a).toRat = -a.toRat := by
1159 refine Quot.induction_on a (fun a => ?_)
1160 show (RatioOrbit.negate a).toRat = -a.toRat
1161 exact RatioOrbit.negate_toRat a
1162
1163/-- K4.11. Subtraction on PRC rationals. -/
1164def sub (a b : PRCRat) : PRCRat :=
1165 add a (negate b)
1166
1167@[simp] theorem toRat_sub (a b : PRCRat) :
1168 (sub a b).toRat = a.toRat - b.toRat := by
1169 show (add a (negate b)).toRat = a.toRat - b.toRat
1170 rw [toRat_add, toRat_negate]
1171 ring
1172
1173private theorem mul_respects_cross {a₁ a₂ b₁ b₂ : RatioOrbit}
1174 (ha : RatioOrbit.crossEq a₁ a₂) (hb : RatioOrbit.crossEq b₁ b₂) :
1175 RatioOrbit.crossEq (RatioOrbit.mul a₁ b₁) (RatioOrbit.mul a₂ b₂) := by
1176 rw [RatioOrbit.crossEq_iff_toIntCross] at ha hb ⊢
1177 unfold RatioOrbit.mul
1178 simp only [SignedOrbit.mul_toInt, DistinctionNat.toNat_mul]
1179 push_cast
1180 linear_combination (b₁.num.toInt * (b₂.den.toNat : ℤ)) * ha
1181 + (a₂.num.toInt * (a₁.den.toNat : ℤ)) * hb
1182
1183/-- K4.11. Multiplication on PRC rationals, lifted from ratio-orbit multiplication. -/
1184def mul : PRCRat → PRCRat → PRCRat :=
1185 Quot.lift₂
1186 (fun a b => mk (RatioOrbit.mul a b))
1187 (by
1188 intro a b₁ b₂ h
1189 apply Quot.sound
1190 exact mul_respects_cross (RatioOrbit.crossEq_refl a) h)
1191 (by
1192 intro a₁ a₂ b h
1193 apply Quot.sound
1194 exact mul_respects_cross h (RatioOrbit.crossEq_refl b))
1195
1196@[simp] theorem mul_mk (a b : RatioOrbit) :
1197 mul (mk a) (mk b) = mk (RatioOrbit.mul a b) := by
1198 rfl
1199
1200@[simp] theorem toRat_mul (a b : PRCRat) :
1201 (mul a b).toRat = a.toRat * b.toRat := by
1202 refine Quot.induction_on a (fun a => ?_)
1203 refine Quot.induction_on b (fun b => ?_)
1204 show (RatioOrbit.mul a b).toRat = a.toRat * b.toRat
1205 exact RatioOrbit.mul_toRat a b
1206
1207private theorem recip_respects_cross {a b : RatioOrbit}
1208 (h : RatioOrbit.crossEq a b) :
1209 RatioOrbit.crossEq (RatioOrbit.recip a) (RatioOrbit.recip b) := by
1210 -- Choice-free: route through the integer cross-multiplication hub,
1211 -- never through the classical ℚ display.
1212 rw [RatioOrbit.crossEq_iff_toIntCross] at h
1213 have hda : 0 < (a.den.toNat : ℤ) := by
1214 have := a.den_toNat_ne_zero
1215 omega
1216 have hdb : 0 < (b.den.toNat : ℤ) := by
1217 have := b.den_toNat_ne_zero
1218 omega
1219 by_cases hza : SignedOrbit.balanced a.num SignedOrbit.zero
1220 · -- Zero numerators propagate across crossEq; both reciprocals are zero.
1221 have hza' : a.num.toInt = 0 := by
1222 have h0 := (SignedOrbit.balanced_iff_toInt_eq a.num SignedOrbit.zero).mp hza
1223 rwa [SignedOrbit.zero_toInt] at h0
1224 have hzb' : b.num.toInt = 0 := by
1225 have h0 : b.num.toInt * (a.den.toNat : ℤ) = 0 := by
1226 rw [← h, hza', Int.zero_mul]
1227 have hda' : (a.den.toNat : ℤ) ≠ 0 := by omega
1228 have h1 : b.num.toInt * (a.den.toNat : ℤ) = 0 * (a.den.toNat : ℤ) := by
1229 rw [h0, Int.zero_mul]
1230 exact Int.eq_of_mul_eq_mul_right hda' h1
1231 have hzb : SignedOrbit.balanced b.num SignedOrbit.zero := by
1232 rw [SignedOrbit.balanced_iff_toInt_eq, SignedOrbit.zero_toInt]
1233 exact hzb'
1234 unfold RatioOrbit.recip
1235 rw [dif_pos hza, dif_pos hzb]
1236 exact RatioOrbit.crossEq_refl RatioOrbit.zero
1237 · -- Nonzero numerators: signs must agree across the cross-equality.
1238 have hna : a.num.toInt ≠ 0 := by
1239 intro hz
1240 apply hza
1241 rw [SignedOrbit.balanced_iff_toInt_eq, SignedOrbit.zero_toInt]
1242 exact hz
1243 have hnb : b.num.toInt ≠ 0 := by
1244 intro hz
1245 apply hna
1246 have h0 : a.num.toInt * (b.den.toNat : ℤ) = 0 := by
1247 rw [h, hz, Int.zero_mul]
1248 have hdb' : (b.den.toNat : ℤ) ≠ 0 := by omega
1249 have h1 : a.num.toInt * (b.den.toNat : ℤ) = 0 * (b.den.toNat : ℤ) := by
1250 rw [h0, Int.zero_mul]
1251 exact Int.eq_of_mul_eq_mul_right hdb' h1
1252 have hzb : ¬ SignedOrbit.balanced b.num SignedOrbit.zero := by
1253 intro hb
1254 apply hnb
1255 have h0 := (SignedOrbit.balanced_iff_toInt_eq b.num SignedOrbit.zero).mp hb
1256 rwa [SignedOrbit.zero_toInt] at h0
1257 unfold RatioOrbit.recip
1258 rw [dif_neg hza, dif_neg hzb]
1259 rw [RatioOrbit.crossEq_iff_toIntCross]
1260 simp only [RatioOrbit.recipNonzero]
1261 by_cases hfa : a.num.nonnegFlag = true
1262 · have hpa : 0 < a.num.toInt := by
1263 have := (SignedOrbit.nonnegFlag_eq_true_iff a.num).mp hfa
1264 omega
1265 by_cases hfb : b.num.nonnegFlag = true
1266 · -- Both positive: cross identity is the hypothesis, transposed.
1267 have hpb : 0 < b.num.toInt := by
1268 have := (SignedOrbit.nonnegFlag_eq_true_iff b.num).mp hfb
1269 omega
1270 rw [if_pos hfa, if_pos hfb, SignedOrbit.ofOrbit_toInt,
1271 SignedOrbit.ofOrbit_toInt, SignedOrbit.abs_toNat,
1272 SignedOrbit.abs_toNat]
1273 have haa : ((a.num.toInt.natAbs : ℕ) : ℤ) = a.num.toInt := by omega
1274 have hbb : ((b.num.toInt.natAbs : ℕ) : ℤ) = b.num.toInt := by omega
1275 rw [haa, hbb]
1276 linear_combination -h
1277 · -- a positive, b negative: contradicts crossEq.
1278 exfalso
1279 have hfb' : b.num.nonnegFlag = false := by
1280 cases hv : b.num.nonnegFlag with
1281 | false => rfl
1282 | true => exact absurd hv hfb
1283 have hqb : b.num.toInt < 0 :=
1284 (SignedOrbit.nonnegFlag_eq_false_iff b.num).mp hfb'
1285 have h1 : (0 : ℤ) < a.num.toInt * (b.den.toNat : ℤ) := Int.mul_pos hpa hdb
1286 have h2 : (0 : ℤ) < (-b.num.toInt) * (a.den.toNat : ℤ) :=
1287 Int.mul_pos (by omega) hda
1288 have h3 : (-b.num.toInt) * (a.den.toNat : ℤ) =
1289 -(b.num.toInt * (a.den.toNat : ℤ)) := by ring
1290 rw [h] at h1
1291 omega
1292 · have hfa' : a.num.nonnegFlag = false := by
1293 cases hv : a.num.nonnegFlag with
1294 | false => rfl
1295 | true => exact absurd hv hfa
1296 have hqa : a.num.toInt < 0 :=
1297 (SignedOrbit.nonnegFlag_eq_false_iff a.num).mp hfa'
1298 by_cases hfb : b.num.nonnegFlag = true
1299 · -- a negative, b positive: contradicts crossEq.
1300 exfalso
1301 have hpb : 0 < b.num.toInt := by
1302 have := (SignedOrbit.nonnegFlag_eq_true_iff b.num).mp hfb
1303 omega
1304 have h1 : (0 : ℤ) < (-a.num.toInt) * (b.den.toNat : ℤ) :=
1305 Int.mul_pos (by omega) hdb
1306 have h1' : (-a.num.toInt) * (b.den.toNat : ℤ) =
1307 -(a.num.toInt * (b.den.toNat : ℤ)) := by ring
1308 have h2 : (0 : ℤ) < b.num.toInt * (a.den.toNat : ℤ) := Int.mul_pos hpb hda
1309 rw [h] at h1'
1310 omega
1311 · -- Both negative: signs cancel, cross identity again the hypothesis.
1312 have hfb' : b.num.nonnegFlag = false := by
1313 cases hv : b.num.nonnegFlag with
1314 | false => rfl
1315 | true => exact absurd hv hfb
1316 have hqb : b.num.toInt < 0 :=
1317 (SignedOrbit.nonnegFlag_eq_false_iff b.num).mp hfb'
1318 rw [if_neg hfa, if_neg hfb, SignedOrbit.negate_toInt,
1319 SignedOrbit.negate_toInt, SignedOrbit.ofOrbit_toInt,
1320 SignedOrbit.ofOrbit_toInt, SignedOrbit.abs_toNat,
1321 SignedOrbit.abs_toNat]
1322 have haa : ((a.num.toInt.natAbs : ℕ) : ℤ) = -a.num.toInt := by omega
1323 have hbb : ((b.num.toInt.natAbs : ℕ) : ℤ) = -b.num.toInt := by omega
1324 rw [haa, hbb]
1325 linear_combination -h
1326
1327/-- K4.12. Total reciprocal on PRC rationals, lifted from ratio-orbit
1328reciprocal and sending zero to zero. -/
1329def recip : PRCRat → PRCRat :=
1330 Quot.lift
1331 (fun a => mk (RatioOrbit.recip a))
1332 (by
1333 intro a b h
1334 apply Quot.sound
1335 exact recip_respects_cross h)
1336
1337@[simp] theorem recip_mk (a : RatioOrbit) :
1338 recip (mk a) = mk (RatioOrbit.recip a) := by
1339 rfl
1340
1341@[simp] theorem toRat_recip (a : PRCRat) :
1342 (recip a).toRat = (a.toRat)⁻¹ := by
1343 refine Quot.induction_on a (fun a => ?_)
1344 show (RatioOrbit.recip a).toRat = (a.toRat)⁻¹
1345 exact RatioOrbit.recip_toRat a
1346
1347/-! ### PRCRat field-style laws, proved choice-free through the integer
1348cross-multiplication hub
1349
1350Each law is proved directly on the quotient: `Quot.induction_on` exposes
1351representatives, `mk_eq_mk_of_crossEq` (a `Quot.sound` wrapper) reduces the
1352goal to `RatioOrbit.crossEq`, and `crossEq_iff_toIntCross` turns that into an
1353integer polynomial identity closed by `ring`. None of these proofs routes
1354through the classical `ℚ` display (`toRat`), so the laws stay on the
1355`{propext, Quot.sound}` axiom basis. -/
1356
1357private theorem zero_num_toInt : (RatioOrbit.zero).num.toInt = 0 :=
1358 SignedOrbit.zero_toInt
1359
1360private theorem zero_den_toNat : (RatioOrbit.zero).den.toNat = 1 := by
1361 show (DistinctionNat.succ DistinctionNat.zero).toNat = 1
1362 rw [DistinctionNat.toNat_succ, DistinctionNat.toNat_zero]
1363
1364private theorem one_num_toInt : (RatioOrbit.one).num.toInt = 1 :=
1365 SignedOrbit.one_toInt
1366
1367private theorem one_den_toNat : (RatioOrbit.one).den.toNat = 1 := by
1368 show (DistinctionNat.succ DistinctionNat.zero).toNat = 1
1369 rw [DistinctionNat.toNat_succ, DistinctionNat.toNat_zero]
1370
1371/-- K4.8. Choice-free structural zero test: a PRC rational is in the zero
1372class iff its representative's numerator balances the zero signed orbit.
1373Well-definedness routes through the integer cross-multiplication hub (no `ℚ`
1374display), so the definition depends only on `{propext, Quot.sound}`. -/
1375def isZero : PRCRat → Prop :=
1376 Quot.lift
1377 (fun q => SignedOrbit.balanced q.num SignedOrbit.zero)
1378 (by
1379 intro a b h
1380 have h' := (RatioOrbit.crossEq_iff_toIntCross a b).mp h
1381 have hda : (a.den.toNat : ℤ) ≠ 0 := by
1382 have := a.den_toNat_ne_zero
1383 omega
1384 have hdb : (b.den.toNat : ℤ) ≠ 0 := by
1385 have := b.den_toNat_ne_zero
1386 omega
1387 apply propext
1388 show SignedOrbit.balanced a.num SignedOrbit.zero
1389 ↔ SignedOrbit.balanced b.num SignedOrbit.zero
1390 rw [SignedOrbit.balanced_iff_toInt_eq, SignedOrbit.balanced_iff_toInt_eq,
1391 SignedOrbit.zero_toInt]
1392 constructor
1393 · intro ha0
1394 have h0 : b.num.toInt * (a.den.toNat : ℤ) = 0 * (a.den.toNat : ℤ) := by
1395 rw [← h', ha0, Int.zero_mul, Int.zero_mul]
1396 exact Int.eq_of_mul_eq_mul_right hda h0
1397 · intro hb0
1398 have h0 : a.num.toInt * (b.den.toNat : ℤ) = 0 * (b.den.toNat : ℤ) := by
1399 rw [h', hb0, Int.zero_mul, Int.zero_mul]
1400 exact Int.eq_of_mul_eq_mul_right hdb h0)
1401
1402@[simp] theorem isZero_mk (q : RatioOrbit) :
1403 isZero (mk q) ↔ SignedOrbit.balanced q.num SignedOrbit.zero :=
1404 Iff.rfl
1405
1406theorem isZero_zero : isZero zero :=
1407 SignedOrbit.balanced_refl SignedOrbit.zero
1408
1409theorem not_isZero_one : ¬ isZero one := by
1410 intro h1
1411 have h2 := (SignedOrbit.balanced_iff_toInt_eq
1412 SignedOrbit.one SignedOrbit.zero).mp h1
1413 rw [SignedOrbit.one_toInt, SignedOrbit.zero_toInt] at h2
1414 omega
1415
1416/-- K4.8. Structural nontriviality: the zero and one classes are distinct.
1417Proved by the choice-free `isZero` discriminator (no `ℚ` display). -/
1418theorem zero_ne_one : (zero : PRCRat) ≠ one := by
1419 intro h
1420 exact not_isZero_one (h ▸ isZero_zero)
1421
1422theorem add_comm (a b : PRCRat) : add a b = add b a := by
1423 refine Quot.induction_on a (fun a => ?_)
1424 refine Quot.induction_on b (fun b => ?_)
1425 show mk (RatioOrbit.add a b) = mk (RatioOrbit.add b a)
1426 apply mk_eq_mk_of_crossEq
1427 rw [RatioOrbit.crossEq_iff_toIntCross]
1428 unfold RatioOrbit.add
1429 simp only [SignedOrbit.add_toInt, SignedOrbit.scaleByNat_toInt,
1430 DistinctionNat.toNat_mul]
1431 push_cast
1432 ring
1433
1434theorem add_assoc (a b c : PRCRat) :
1435 add (add a b) c = add a (add b c) := by
1436 refine Quot.induction_on a (fun a => ?_)
1437 refine Quot.induction_on b (fun b => ?_)
1438 refine Quot.induction_on c (fun c => ?_)
1439 show mk (RatioOrbit.add (RatioOrbit.add a b) c)
1440 = mk (RatioOrbit.add a (RatioOrbit.add b c))
1441 apply mk_eq_mk_of_crossEq
1442 rw [RatioOrbit.crossEq_iff_toIntCross]
1443 unfold RatioOrbit.add
1444 simp only [SignedOrbit.add_toInt, SignedOrbit.scaleByNat_toInt,
1445 DistinctionNat.toNat_mul]
1446 push_cast
1447 ring
1448
1449theorem zero_add (a : PRCRat) : add zero a = a := by
1450 refine Quot.induction_on a (fun a => ?_)
1451 show mk (RatioOrbit.add RatioOrbit.zero a) = mk a
1452 apply mk_eq_mk_of_crossEq
1453 rw [RatioOrbit.crossEq_iff_toIntCross]
1454 unfold RatioOrbit.add
1455 simp only [SignedOrbit.add_toInt, SignedOrbit.scaleByNat_toInt,
1456 DistinctionNat.toNat_mul, zero_num_toInt, zero_den_toNat]
1457 push_cast
1458 ring
1459
1460theorem add_zero (a : PRCRat) : add a zero = a := by
1461 refine Quot.induction_on a (fun a => ?_)
1462 show mk (RatioOrbit.add a RatioOrbit.zero) = mk a
1463 apply mk_eq_mk_of_crossEq
1464 rw [RatioOrbit.crossEq_iff_toIntCross]
1465 unfold RatioOrbit.add
1466 simp only [SignedOrbit.add_toInt, SignedOrbit.scaleByNat_toInt,
1467 DistinctionNat.toNat_mul, zero_num_toInt, zero_den_toNat]
1468 push_cast
1469 ring
1470
1471theorem add_negate (a : PRCRat) : add a (negate a) = zero := by
1472 refine Quot.induction_on a (fun a => ?_)
1473 show mk (RatioOrbit.add a (RatioOrbit.negate a)) = mk RatioOrbit.zero
1474 apply mk_eq_mk_of_crossEq
1475 rw [RatioOrbit.crossEq_iff_toIntCross]
1476 unfold RatioOrbit.add RatioOrbit.negate
1477 simp only [SignedOrbit.add_toInt, SignedOrbit.negate_toInt,
1478 SignedOrbit.scaleByNat_toInt, DistinctionNat.toNat_mul,
1479 zero_num_toInt, zero_den_toNat]
1480 push_cast
1481 ring
1482
1483theorem negate_add (a : PRCRat) : add (negate a) a = zero := by
1484 refine Quot.induction_on a (fun a => ?_)
1485 show mk (RatioOrbit.add (RatioOrbit.negate a) a) = mk RatioOrbit.zero
1486 apply mk_eq_mk_of_crossEq
1487 rw [RatioOrbit.crossEq_iff_toIntCross]
1488 unfold RatioOrbit.add RatioOrbit.negate
1489 simp only [SignedOrbit.add_toInt, SignedOrbit.negate_toInt,
1490 SignedOrbit.scaleByNat_toInt, DistinctionNat.toNat_mul,
1491 zero_num_toInt, zero_den_toNat]
1492 push_cast
1493 ring
1494
1495theorem mul_comm (a b : PRCRat) : mul a b = mul b a := by
1496 refine Quot.induction_on a (fun a => ?_)
1497 refine Quot.induction_on b (fun b => ?_)
1498 show mk (RatioOrbit.mul a b) = mk (RatioOrbit.mul b a)
1499 apply mk_eq_mk_of_crossEq
1500 rw [RatioOrbit.crossEq_iff_toIntCross]
1501 unfold RatioOrbit.mul
1502 simp only [SignedOrbit.mul_toInt, DistinctionNat.toNat_mul]
1503 push_cast
1504 ring
1505
1506theorem mul_assoc (a b c : PRCRat) :
1507 mul (mul a b) c = mul a (mul b c) := by
1508 refine Quot.induction_on a (fun a => ?_)
1509 refine Quot.induction_on b (fun b => ?_)
1510 refine Quot.induction_on c (fun c => ?_)
1511 show mk (RatioOrbit.mul (RatioOrbit.mul a b) c)
1512 = mk (RatioOrbit.mul a (RatioOrbit.mul b c))
1513 apply mk_eq_mk_of_crossEq
1514 rw [RatioOrbit.crossEq_iff_toIntCross]
1515 unfold RatioOrbit.mul
1516 simp only [SignedOrbit.mul_toInt, DistinctionNat.toNat_mul]
1517 push_cast
1518 ring
1519
1520theorem one_mul (a : PRCRat) : mul one a = a := by
1521 refine Quot.induction_on a (fun a => ?_)
1522 show mk (RatioOrbit.mul RatioOrbit.one a) = mk a
1523 apply mk_eq_mk_of_crossEq
1524 rw [RatioOrbit.crossEq_iff_toIntCross]
1525 unfold RatioOrbit.mul
1526 simp only [SignedOrbit.mul_toInt, DistinctionNat.toNat_mul,
1527 one_num_toInt, one_den_toNat]
1528 push_cast
1529 ring
1530
1531theorem mul_one (a : PRCRat) : mul a one = a := by
1532 refine Quot.induction_on a (fun a => ?_)
1533 show mk (RatioOrbit.mul a RatioOrbit.one) = mk a
1534 apply mk_eq_mk_of_crossEq
1535 rw [RatioOrbit.crossEq_iff_toIntCross]
1536 unfold RatioOrbit.mul
1537 simp only [SignedOrbit.mul_toInt, DistinctionNat.toNat_mul,
1538 one_num_toInt, one_den_toNat]
1539 push_cast
1540 ring
1541
1542theorem zero_mul (a : PRCRat) : mul zero a = zero := by
1543 refine Quot.induction_on a (fun a => ?_)
1544 show mk (RatioOrbit.mul RatioOrbit.zero a) = mk RatioOrbit.zero
1545 apply mk_eq_mk_of_crossEq
1546 rw [RatioOrbit.crossEq_iff_toIntCross]
1547 unfold RatioOrbit.mul
1548 simp only [SignedOrbit.mul_toInt, DistinctionNat.toNat_mul,
1549 zero_num_toInt, zero_den_toNat]
1550 push_cast
1551 ring
1552
1553theorem mul_zero (a : PRCRat) : mul a zero = zero := by
1554 refine Quot.induction_on a (fun a => ?_)
1555 show mk (RatioOrbit.mul a RatioOrbit.zero) = mk RatioOrbit.zero
1556 apply mk_eq_mk_of_crossEq
1557 rw [RatioOrbit.crossEq_iff_toIntCross]
1558 unfold RatioOrbit.mul
1559 simp only [SignedOrbit.mul_toInt, DistinctionNat.toNat_mul,
1560 zero_num_toInt, zero_den_toNat]
1561 push_cast
1562 ring
1563
1564theorem left_distrib (a b c : PRCRat) :
1565 mul a (add b c) = add (mul a b) (mul a c) := by
1566 refine Quot.induction_on a (fun a => ?_)
1567 refine Quot.induction_on b (fun b => ?_)
1568 refine Quot.induction_on c (fun c => ?_)
1569 show mk (RatioOrbit.mul a (RatioOrbit.add b c))
1570 = mk (RatioOrbit.add (RatioOrbit.mul a b) (RatioOrbit.mul a c))
1571 apply mk_eq_mk_of_crossEq
1572 rw [RatioOrbit.crossEq_iff_toIntCross]
1573 unfold RatioOrbit.mul RatioOrbit.add
1574 simp only [SignedOrbit.add_toInt, SignedOrbit.mul_toInt,
1575 SignedOrbit.scaleByNat_toInt, DistinctionNat.toNat_mul]
1576 push_cast
1577 ring
1578
1579theorem right_distrib (a b c : PRCRat) :
1580 mul (add a b) c = add (mul a c) (mul b c) := by
1581 refine Quot.induction_on a (fun a => ?_)
1582 refine Quot.induction_on b (fun b => ?_)
1583 refine Quot.induction_on c (fun c => ?_)
1584 show mk (RatioOrbit.mul (RatioOrbit.add a b) c)
1585 = mk (RatioOrbit.add (RatioOrbit.mul a c) (RatioOrbit.mul b c))
1586 apply mk_eq_mk_of_crossEq
1587 rw [RatioOrbit.crossEq_iff_toIntCross]
1588 unfold RatioOrbit.mul RatioOrbit.add
1589 simp only [SignedOrbit.add_toInt, SignedOrbit.mul_toInt,
1590 SignedOrbit.scaleByNat_toInt, DistinctionNat.toNat_mul]
1591 push_cast
1592 ring
1593
1594/-- K4.12. Structural reciprocal cancellation: any PRC rational outside the
1595zero class satisfies `a * a⁻¹ = 1`. The nonzero hypothesis is the structural
1596disequality `a ≠ zero` (not the `ℚ` display), so both the statement and the
1597proof are choice-free. -/
1598theorem mul_recip_cancel₀ {a : PRCRat} (h : a ≠ zero) :
1599 mul a (recip a) = one := by
1600 revert h
1601 refine Quot.induction_on a (fun q => ?_)
1602 intro h
1603 -- The structural hypothesis descends to the representative: a balanced
1604 -- (zero) numerator would place the class in the zero class.
1605 have hz : ¬ SignedOrbit.balanced q.num SignedOrbit.zero := by
1606 intro hb
1607 apply h
1608 show mk q = mk RatioOrbit.zero
1609 apply mk_eq_mk_of_crossEq
1610 rw [RatioOrbit.crossEq_iff_toIntCross]
1611 have h0 : q.num.toInt = 0 := by
1612 have h1 := (SignedOrbit.balanced_iff_toInt_eq
1613 q.num SignedOrbit.zero).mp hb
1614 rwa [SignedOrbit.zero_toInt] at h1
1615 rw [h0, zero_num_toInt, Int.zero_mul, Int.zero_mul]
1616 have hne : q.num.toInt ≠ 0 := by
1617 intro h0
1618 apply hz
1619 rw [SignedOrbit.balanced_iff_toInt_eq, SignedOrbit.zero_toInt]
1620 exact h0
1621 show mk (RatioOrbit.mul q (RatioOrbit.recip q)) = mk RatioOrbit.one
1622 apply mk_eq_mk_of_crossEq
1623 rw [RatioOrbit.crossEq_iff_toIntCross]
1624 unfold RatioOrbit.mul RatioOrbit.recip
1625 rw [dif_neg hz]
1626 simp only [RatioOrbit.recipNonzero, SignedOrbit.mul_toInt,
1627 DistinctionNat.toNat_mul, one_num_toInt, one_den_toNat]
1628 by_cases hf : q.num.nonnegFlag = true
1629 · -- Positive numerator: the reciprocal numerator is the promoted denominator.
1630 have hpos : 0 < q.num.toInt := by
1631 have := (SignedOrbit.nonnegFlag_eq_true_iff q.num).mp hf
1632 omega
1633 rw [if_pos hf, SignedOrbit.ofOrbit_toInt]
1634 push_cast
1635 have haa : ((q.num.abs.toNat : ℕ) : ℤ) = q.num.toInt := by
1636 rw [SignedOrbit.abs_toNat]
1637 omega
1638 rw [haa]
1639 ring
1640 · -- Negative numerator: the reciprocal numerator is the negated denominator.
1641 have hf' : q.num.nonnegFlag = false := by
1642 cases hv : q.num.nonnegFlag with
1643 | false => rfl
1644 | true => exact absurd hv hf
1645 have hneg : q.num.toInt < 0 :=
1646 (SignedOrbit.nonnegFlag_eq_false_iff q.num).mp hf'
1647 rw [if_neg hf, SignedOrbit.negate_toInt, SignedOrbit.ofOrbit_toInt]
1648 push_cast
1649 have haa : ((q.num.abs.toNat : ℕ) : ℤ) = -q.num.toInt := by
1650 rw [SignedOrbit.abs_toNat]
1651 omega
1652 rw [haa]
1653 ring
1654
1655/-- K4.12. Structural reciprocal cancellation, inverse side. -/
1656theorem recip_mul_cancel₀ {a : PRCRat} (h : a ≠ zero) :
1657 mul (recip a) a = one := by
1658 rw [mul_comm]
1659 exact mul_recip_cancel₀ h
1660
1661/-- K4.12. The reciprocal fixes the zero class (the `ℚ` convention
1662`0⁻¹ = 0`), proved structurally: the zero representative's numerator
1663balances the zero orbit, so `RatioOrbit.recip` takes its zero branch. -/
1664theorem recip_zero : recip zero = zero := by
1665 show mk (RatioOrbit.recip RatioOrbit.zero) = mk RatioOrbit.zero
1666 have h : SignedOrbit.balanced (RatioOrbit.zero).num SignedOrbit.zero :=
1667 SignedOrbit.balanced_refl SignedOrbit.zero
1668 unfold RatioOrbit.recip
1669 rw [dif_pos h]
1670
1671/-- K4.12. Display-form reciprocal cancellation, kept for `ℚ`-facing API
1672compatibility. The statement mentions `toRat`, so it is intrinsically
1673display-bound; the structural content is `mul_recip_cancel₀`. -/
1674theorem mul_recip_cancel {a : PRCRat} (h : a.toRat ≠ 0) :
1675 mul a (recip a) = one := by
1676 apply mul_recip_cancel₀
1677 intro hz
1678 apply h
1679 rw [hz, zero_toRat]
1680
1681/-! ### Operation instances on PRCRat -/
1682
1683instance instZero : Zero PRCRat := ⟨zero⟩
1684instance instOne : One PRCRat := ⟨one⟩
1685instance instAdd : Add PRCRat := ⟨add⟩
1686instance instMul : Mul PRCRat := ⟨mul⟩
1687instance instNeg : Neg PRCRat := ⟨negate⟩
1688instance instSub : Sub PRCRat := ⟨sub⟩
1689instance instInv : Inv PRCRat := ⟨recip⟩
1690
1691@[simp] theorem add_eq (a b : PRCRat) : a + b = add a b := rfl
1692@[simp] theorem mul_eq (a b : PRCRat) : a * b = mul a b := rfl
1693@[simp] theorem neg_eq (a : PRCRat) : -a = negate a := rfl
1694@[simp] theorem sub_eq (a b : PRCRat) : a - b = sub a b := rfl
1695@[simp] theorem inv_eq (a : PRCRat) : a⁻¹ = recip a := rfl
1696@[simp] theorem zero_eq : (0 : PRCRat) = zero := rfl
1697@[simp] theorem one_eq : (1 : PRCRat) = one := rfl
1698
1699theorem toRat_add' (a b : PRCRat) :
1700 (a + b).toRat = a.toRat + b.toRat := by
1701 simp
1702
1703theorem toRat_mul' (a b : PRCRat) :
1704 (a * b).toRat = a.toRat * b.toRat := by
1705 simp
1706
1707theorem toRat_neg' (a : PRCRat) :
1708 (-a).toRat = -a.toRat := by
1709 simp
1710
1711theorem toRat_inv' (a : PRCRat) :
1712 (a⁻¹).toRat = (a.toRat)⁻¹ := by
1713 simp
1714
1715end PRCRat
1716
1717end PrimitiveRecognitionCalculus
1718end Foundation
1719end IndisputableMonolith
1720