IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.OrbitEuclidean
IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/OrbitEuclidean.lean · 519 lines · 36 declarations
show as:
view math explainer →
1/-
2 PrimitiveRecognitionCalculus/OrbitEuclidean.lean
3
4 Round-trip source:
5 δ/PRC_Universal_Foundation_Execution_Plan_20260526.html
6
7 Spec anchors:
8 Build Order step 3: Euclidean quotient/remainder, GCD, coprime, and
9 rational normalization targets.
10
11 Strength: δ-only for definitions. Nat division, modulo, and gcd appear only
12 in verifier transport theorems.
13-/
14
15import Mathlib
16import IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.IntegerRational
17import IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.OrbitDivisibility
18
19namespace IndisputableMonolith
20namespace Foundation
21namespace PrimitiveRecognitionCalculus
22namespace DistinctionNat
23
24/-! ## Object-level quotient and remainder by repeated subtraction -/
25
26/-- Fuelled quotient/remainder by repeated subtraction. The first argument is
27an orbit fuel, not verifier `Nat`. -/
28def divModFuel : DistinctionNat → DistinctionNat → DistinctionNat → DistinctionNat × DistinctionNat
29 | zero, n, _ => (zero, n)
30 | succ fuel, n, d =>
31 if DistinctionNat.leq d n then
32 let qr := divModFuel fuel (DistinctionNat.truncatedSub n d) d
33 (succ qr.1, qr.2)
34 else
35 (zero, n)
36
37/-- Euclidean quotient/remainder. The fuel `n` is enough when `d` is nonzero,
38because each successful subtraction lowers the dividend by at least one. -/
39def divMod (n d : DistinctionNat) (_hd : d ≠ zero) : DistinctionNat × DistinctionNat :=
40 divModFuel n n d
41
42/-- Object-level quotient. -/
43def quotient (n d : DistinctionNat) (hd : d ≠ zero) : DistinctionNat :=
44 (divMod n d hd).1
45
46/-- Object-level remainder. -/
47def remainder (n d : DistinctionNat) (hd : d ≠ zero) : DistinctionNat :=
48 (divMod n d hd).2
49
50private theorem divModFuel_toNat_aux (fuel n d : DistinctionNat)
51 (hd : d.toNat ≠ 0)
52 (hbound : n.toNat ≤ fuel.toNat) :
53 let qr := divModFuel fuel n d
54 qr.1.toNat = n.toNat / d.toNat ∧
55 qr.2.toNat = n.toNat % d.toNat := by
56 induction fuel generalizing n with
57 | zero =>
58 rw [toNat_zero] at hbound
59 have hn0 : n.toNat = 0 := by omega
60 simp [divModFuel, hn0]
61 | succ fuel ih =>
62 rw [toNat_succ] at hbound
63 unfold divModFuel
64 by_cases hleq : DistinctionNat.leq d n = true
65 · have hle : d.toNat ≤ n.toNat :=
66 (DistinctionNat.leq_eq_true_iff d n).mp hleq
67 have hpos : 0 < d.toNat := by omega
68 simp [hleq]
69 have hbound' : (DistinctionNat.truncatedSub n d).toNat ≤ fuel.toNat := by
70 rw [DistinctionNat.toNat_truncatedSub]
71 omega
72 have ih' := ih (DistinctionNat.truncatedSub n d) hbound'
73 rcases ih' with ⟨hq, hr⟩
74 rw [hq, hr]
75 constructor
76 · rw [DistinctionNat.toNat_truncatedSub, Nat.div_eq_sub_div hpos hle]
77 · rw [DistinctionNat.toNat_truncatedSub]
78 exact (Nat.mod_eq_sub_mod hle).symm
79 · have hlt : n.toNat < d.toNat := by
80 have hf := (DistinctionNat.leq_eq_false_iff d n).mp (by
81 cases h : DistinctionNat.leq d n with
82 | false => rfl
83 | true =>
84 exfalso
85 exact hleq h)
86 exact hf
87 simp [hleq]
88 constructor
89 · exact (Nat.div_eq_of_lt hlt).symm
90 · exact (Nat.mod_eq_of_lt hlt).symm
91
92/-- Euclidean quotient/remainder transports to verifier Nat division and
93modulus. -/
94theorem divMod_toNat (n d : DistinctionNat) (hd : d ≠ zero) :
95 let qr := divMod n d hd
96 qr.1.toNat = n.toNat / d.toNat ∧
97 qr.2.toNat = n.toNat % d.toNat := by
98 unfold divMod
99 apply divModFuel_toNat_aux
100 · intro hzero
101 have : d = zero := by
102 apply toNat_inj
103 rw [hzero, toNat_zero]
104 exact hd this
105 · omega
106
107theorem quotient_toNat (n d : DistinctionNat) (hd : d ≠ zero) :
108 (quotient n d hd).toNat = n.toNat / d.toNat := by
109 have h := divMod_toNat n d hd
110 exact h.1
111
112theorem remainder_toNat (n d : DistinctionNat) (hd : d ≠ zero) :
113 (remainder n d hd).toNat = n.toNat % d.toNat := by
114 have h := divMod_toNat n d hd
115 exact h.2
116
117theorem remainder_lt_divisor (n d : DistinctionNat) (hd : d ≠ zero) :
118 (remainder n d hd).toNat < d.toNat := by
119 rw [remainder_toNat]
120 apply Nat.mod_lt
121 exact Nat.pos_of_ne_zero (by
122 intro hzero
123 have : d = zero := by
124 apply toNat_inj
125 rw [hzero, toNat_zero]
126 exact hd this)
127
128/-- The quotient and remainder reconstruct the dividend in orbit arithmetic. -/
129theorem quotient_mul_divisor_add_remainder_eq
130 (n d : DistinctionNat) (hd : d ≠ zero) :
131 quotient n d hd * d + remainder n d hd = n := by
132 apply toNat_inj
133 rw [toNat_add, toNat_mul, quotient_toNat, remainder_toNat]
134 rw [Nat.mul_comm (n.toNat / d.toNat) d.toNat]
135 exact Nat.div_add_mod n.toNat d.toNat
136
137/-! ## Object-level GCD by subtractive Euclidean descent -/
138
139/-- Fuelled subtractive Euclidean GCD. -/
140def gcdFuel : DistinctionNat → DistinctionNat → DistinctionNat → DistinctionNat
141 | zero, a, b => a + b
142 | succ fuel, a, b =>
143 if a = zero then
144 b
145 else if b = zero then
146 a
147 else if DistinctionNat.leq b a then
148 gcdFuel fuel (DistinctionNat.truncatedSub a b) b
149 else
150 gcdFuel fuel a (DistinctionNat.truncatedSub b a)
151
152/-- Object-level GCD by subtractive Euclidean descent. -/
153def gcd (a b : DistinctionNat) : DistinctionNat :=
154 gcdFuel (a + b) a b
155
156/-- Object-level coprimality. -/
157def coprime (a b : DistinctionNat) : Prop :=
158 unit (gcd a b)
159
160private theorem gcdFuel_toNat_aux (fuel a b : DistinctionNat)
161 (hbound : a.toNat + b.toNat ≤ fuel.toNat) :
162 (gcdFuel fuel a b).toNat = Nat.gcd a.toNat b.toNat := by
163 induction fuel generalizing a b with
164 | zero =>
165 rw [toNat_zero] at hbound
166 have ha0 : a.toNat = 0 := by omega
167 have hb0 : b.toNat = 0 := by omega
168 simp [gcdFuel, ha0, hb0, toNat_add]
169 | succ fuel ih =>
170 rw [toNat_succ] at hbound
171 unfold gcdFuel
172 by_cases ha : a = zero
173 · simp [ha, Nat.gcd_zero_left]
174 · by_cases hb : b = zero
175 · simp [ha, hb, Nat.gcd_zero_right]
176 · by_cases hleq : DistinctionNat.leq b a = true
177 · have hle : b.toNat ≤ a.toNat :=
178 (DistinctionNat.leq_eq_true_iff b a).mp hleq
179 have hbpos : 0 < b.toNat := by
180 have hbne : b.toNat ≠ 0 := by
181 intro hzero
182 have : b = zero := by
183 apply toNat_inj
184 rw [hzero, toNat_zero]
185 exact hb this
186 omega
187 have hbound' :
188 (DistinctionNat.truncatedSub a b).toNat + b.toNat ≤ fuel.toNat := by
189 rw [DistinctionNat.toNat_truncatedSub]
190 omega
191 simp [ha, hb, hleq]
192 rw [ih (DistinctionNat.truncatedSub a b) b hbound']
193 rw [DistinctionNat.toNat_truncatedSub]
194 exact Nat.gcd_sub_self_left hle
195 · have hlt : a.toNat < b.toNat := by
196 exact (DistinctionNat.leq_eq_false_iff b a).mp (by
197 cases h : DistinctionNat.leq b a with
198 | false => rfl
199 | true =>
200 exfalso
201 exact hleq h)
202 have hle : a.toNat ≤ b.toNat := by omega
203 have hapos : 0 < a.toNat := by
204 have hane : a.toNat ≠ 0 := by
205 intro hzero
206 have : a = zero := by
207 apply toNat_inj
208 rw [hzero, toNat_zero]
209 exact ha this
210 omega
211 have hbound' :
212 a.toNat + (DistinctionNat.truncatedSub b a).toNat ≤ fuel.toNat := by
213 rw [DistinctionNat.toNat_truncatedSub]
214 omega
215 simp [ha, hb, hleq]
216 rw [ih a (DistinctionNat.truncatedSub b a) hbound']
217 rw [DistinctionNat.toNat_truncatedSub]
218 exact Nat.gcd_sub_self_right hle
219
220theorem gcd_toNat (a b : DistinctionNat) :
221 (gcd a b).toNat = Nat.gcd a.toNat b.toNat := by
222 unfold gcd
223 apply gcdFuel_toNat_aux
224 rw [toNat_add]
225
226theorem coprime_iff_nat_coprime (a b : DistinctionNat) :
227 coprime a b ↔ Nat.Coprime a.toNat b.toNat := by
228 simp [coprime, gcd_toNat, unit_iff_toNat_eq_one]
229
230/-- The native GCD divides the left input. -/
231theorem gcd_divides_left (a b : DistinctionNat) :
232 divides (gcd a b) a := by
233 rw [divides_iff_toNat_dvd, gcd_toNat]
234 exact Nat.gcd_dvd_left a.toNat b.toNat
235
236/-- The native GCD divides the right input. -/
237theorem gcd_divides_right (a b : DistinctionNat) :
238 divides (gcd a b) b := by
239 rw [divides_iff_toNat_dvd, gcd_toNat]
240 exact Nat.gcd_dvd_right a.toNat b.toNat
241
242/-- Any common native divisor divides the native GCD. -/
243theorem divides_gcd_of_divides_left_right {c a b : DistinctionNat}
244 (hca : divides c a) (hcb : divides c b) :
245 divides c (gcd a b) := by
246 rw [divides_iff_toNat_dvd, gcd_toNat]
247 exact Nat.dvd_gcd
248 ((divides_iff_toNat_dvd c a).mp hca)
249 ((divides_iff_toNat_dvd c b).mp hcb)
250
251/-! ## Coprime divisor cancellation -/
252
253/-- If `a` is coprime to `b` and divides `b*c`, then `a` divides `c`.
254The argument is native at the statement level; Nat appears only in transport. -/
255theorem coprime_divides_of_divides_mul_left {a b c : DistinctionNat}
256 (hcop : coprime b a) (hdiv : divides a (b * c)) :
257 divides a c := by
258 rw [divides_iff_toNat_dvd] at hdiv ⊢
259 rw [toNat_mul] at hdiv
260 have hcopNat : Nat.Coprime b.toNat a.toNat :=
261 (coprime_iff_nat_coprime b a).mp hcop
262 exact hcopNat.symm.dvd_of_dvd_mul_left hdiv
263
264theorem gcd_ne_zero_of_right_ne_zero (a b : DistinctionNat) (hb : b ≠ zero) :
265 gcd a b ≠ zero := by
266 intro h
267 have hnat : (gcd a b).toNat = 0 := by
268 rw [h, toNat_zero]
269 rw [gcd_toNat] at hnat
270 have hb0 : b.toNat = 0 := (Nat.gcd_eq_zero_iff.mp hnat).2
271 apply hb
272 apply toNat_inj
273 rw [hb0, toNat_zero]
274
275theorem quotient_mul_divisor_toNat_of_divides {n d : DistinctionNat}
276 (hd : d ≠ zero) (hdiv : divides d n) :
277 (quotient n d hd).toNat * d.toNat = n.toNat := by
278 rw [quotient_toNat]
279 exact Nat.div_mul_cancel ((divides_iff_toNat_dvd d n).mp hdiv)
280
281theorem quotient_ne_zero_of_divides {n d : DistinctionNat}
282 (hd : d ≠ zero) (hdiv : divides d n) (hn : n ≠ zero) :
283 quotient n d hd ≠ zero := by
284 intro hq
285 have hqnat : (quotient n d hd).toNat = 0 := by
286 rw [hq, toNat_zero]
287 have hmul := quotient_mul_divisor_toNat_of_divides (n := n) (d := d) hd hdiv
288 rw [hqnat, Nat.zero_mul] at hmul
289 apply hn
290 apply toNat_inj
291 rw [hmul.symm, toNat_zero]
292
293/-! ## Signed rational normalization by native orbit GCD -/
294
295/-- Quotient a signed orbit by a nonzero orbit position, restoring the sign by
296the structural signed-orbit comparison. -/
297def signedQuotient (z : SignedOrbit) (d : DistinctionNat) (hd : d ≠ zero) :
298 SignedOrbit :=
299 let q := quotient z.abs d hd
300 if z.nonnegFlag then
301 SignedOrbit.ofOrbit q
302 else
303 SignedOrbit.negate (SignedOrbit.ofOrbit q)
304
305theorem signedQuotient_abs_toNat (z : SignedOrbit)
306 (d : DistinctionNat) (hd : d ≠ zero) :
307 (signedQuotient z d hd).abs.toNat = z.abs.toNat / d.toNat := by
308 unfold signedQuotient
309 by_cases hflag : z.nonnegFlag = true
310 · have hAbsQ :
311 (SignedOrbit.ofOrbit (quotient z.abs d hd)).abs.toNat =
312 (quotient z.abs d hd).toNat := by
313 simp [SignedOrbit.abs_toNat, SignedOrbit.ofOrbit_toInt]
314 simpa [hflag, hAbsQ] using quotient_toNat z.abs d hd
315 · have hflagFalse : z.nonnegFlag = false := by
316 cases h : z.nonnegFlag with
317 | false => rfl
318 | true =>
319 exfalso
320 exact hflag h
321 have hAbsQ :
322 (SignedOrbit.negate (SignedOrbit.ofOrbit (quotient z.abs d hd))).abs.toNat =
323 (quotient z.abs d hd).toNat := by
324 simp [SignedOrbit.abs_toNat, SignedOrbit.ofOrbit_toInt,
325 SignedOrbit.negate_toInt]
326 simpa [hflagFalse, hAbsQ] using quotient_toNat z.abs d hd
327
328theorem signedQuotient_mul_divisor_toInt_of_divides
329 (z : SignedOrbit) (d : DistinctionNat) (hd : d ≠ zero)
330 (hdiv : divides d z.abs) :
331 (signedQuotient z d hd).toInt * (d.toNat : ℤ) = z.toInt := by
332 have hquotNat :
333 (quotient z.abs d hd).toNat * d.toNat = z.abs.toNat :=
334 quotient_mul_divisor_toNat_of_divides (n := z.abs) (d := d) hd hdiv
335 have hquotInt :
336 ((quotient z.abs d hd).toNat : ℤ) * (d.toNat : ℤ) =
337 (z.abs.toNat : ℤ) := by
338 exact_mod_cast hquotNat
339 unfold signedQuotient
340 by_cases hflag : z.nonnegFlag = true
341 · have hnonneg : 0 ≤ z.toInt :=
342 (SignedOrbit.nonnegFlag_eq_true_iff z).mp hflag
343 have habs : (z.abs.toNat : ℤ) = z.toInt := by
344 rw [SignedOrbit.abs_toNat]
345 exact Int.ofNat_natAbs_of_nonneg hnonneg
346 simp [hflag, SignedOrbit.ofOrbit_toInt]
347 rw [hquotInt, habs]
348 · have hflagFalse : z.nonnegFlag = false := by
349 cases h : z.nonnegFlag with
350 | false => rfl
351 | true =>
352 exfalso
353 exact hflag h
354 have hneg : z.toInt < 0 :=
355 (SignedOrbit.nonnegFlag_eq_false_iff z).mp hflagFalse
356 have habs : (z.abs.toNat : ℤ) = -z.toInt := by
357 rw [SignedOrbit.abs_toNat]
358 exact Int.ofNat_natAbs_of_nonpos (le_of_lt hneg)
359 simp [hflagFalse, SignedOrbit.ofOrbit_toInt, SignedOrbit.negate_toInt]
360 rw [hquotInt, habs]
361 ring
362
363/-- Normalize a ratio orbit by dividing numerator magnitude and denominator by
364their native orbit GCD. The signed numerator orientation is restored by
365`SignedOrbit.nonnegFlag`. -/
366def normalizeRatio (q : RatioOrbit) : RatioOrbit :=
367 let g := gcd q.num.abs q.den
368 have hg : g ≠ zero := gcd_ne_zero_of_right_ne_zero q.num.abs q.den q.den_ne_zero
369 {
370 num := signedQuotient q.num g hg
371 den := quotient q.den g hg
372 den_ne_zero :=
373 quotient_ne_zero_of_divides
374 (n := q.den) (d := g) hg
375 (gcd_divides_right q.num.abs q.den)
376 q.den_ne_zero
377 }
378
379theorem normalizeRatio_num_mul_gcd_toInt (q : RatioOrbit) :
380 (normalizeRatio q).num.toInt *
381 ((gcd q.num.abs q.den).toNat : ℤ) = q.num.toInt := by
382 unfold normalizeRatio
383 exact signedQuotient_mul_divisor_toInt_of_divides
384 q.num (gcd q.num.abs q.den)
385 (gcd_ne_zero_of_right_ne_zero q.num.abs q.den q.den_ne_zero)
386 (gcd_divides_left q.num.abs q.den)
387
388theorem normalizeRatio_den_mul_gcd_toNat (q : RatioOrbit) :
389 (normalizeRatio q).den.toNat *
390 (gcd q.num.abs q.den).toNat = q.den.toNat := by
391 unfold normalizeRatio
392 exact quotient_mul_divisor_toNat_of_divides
393 (n := q.den) (d := gcd q.num.abs q.den)
394 (gcd_ne_zero_of_right_ne_zero q.num.abs q.den q.den_ne_zero)
395 (gcd_divides_right q.num.abs q.den)
396
397theorem normalizeRatio_toRat (q : RatioOrbit) :
398 (normalizeRatio q).toRat = q.toRat := by
399 unfold RatioOrbit.toRat
400 have hnumZ := normalizeRatio_num_mul_gcd_toInt q
401 have hdenN := normalizeRatio_den_mul_gcd_toNat q
402 have hnumQ :
403 ((normalizeRatio q).num.toInt : ℚ) *
404 ((gcd q.num.abs q.den).toNat : ℚ) =
405 (q.num.toInt : ℚ) := by
406 exact_mod_cast hnumZ
407 have hdenQ :
408 ((normalizeRatio q).den.toNat : ℚ) *
409 ((gcd q.num.abs q.den).toNat : ℚ) =
410 (q.den.toNat : ℚ) := by
411 exact_mod_cast hdenN
412 have hNormDen : ((normalizeRatio q).den.toNat : ℚ) ≠ 0 :=
413 (normalizeRatio q).den_cast_ne_zero
414 have hDen : (q.den.toNat : ℚ) ≠ 0 := q.den_cast_ne_zero
415 field_simp [hNormDen, hDen]
416 calc
417 ((normalizeRatio q).num.toInt : ℚ) * (q.den.toNat : ℚ)
418 = ((normalizeRatio q).num.toInt : ℚ) *
419 (((normalizeRatio q).den.toNat : ℚ) *
420 ((gcd q.num.abs q.den).toNat : ℚ)) := by
421 rw [hdenQ]
422 _ = (((normalizeRatio q).num.toInt : ℚ) *
423 ((gcd q.num.abs q.den).toNat : ℚ)) *
424 ((normalizeRatio q).den.toNat : ℚ) := by ring
425 _ = (q.num.toInt : ℚ) * ((normalizeRatio q).den.toNat : ℚ) := by
426 rw [hnumQ]
427 _ = ((normalizeRatio q).den.toNat : ℚ) * (q.num.toInt : ℚ) := by ring
428
429theorem normalizeRatio_crossEq (q : RatioOrbit) :
430 RatioOrbit.crossEq q (normalizeRatio q) := by
431 rw [RatioOrbit.crossEq_iff_toRat_eq]
432 exact (normalizeRatio_toRat q).symm
433
434theorem normalizeRatio_coprime (q : RatioOrbit) :
435 coprime (normalizeRatio q).num.abs (normalizeRatio q).den := by
436 rw [coprime_iff_nat_coprime]
437 unfold normalizeRatio
438 rw [signedQuotient_abs_toNat, quotient_toNat]
439 have hgpos : 0 < (gcd q.num.abs q.den).toNat := by
440 rw [gcd_toNat]
441 apply Nat.gcd_pos_of_pos_right
442 exact Nat.pos_of_ne_zero (by
443 intro hzero
444 apply q.den_ne_zero
445 apply toNat_inj
446 rw [hzero, toNat_zero])
447 have hgposNat : 0 < Nat.gcd q.num.abs.toNat q.den.toNat := by
448 rw [← gcd_toNat]
449 exact hgpos
450 rw [gcd_toNat]
451 exact Nat.coprime_div_gcd_div_gcd
452 (m := q.num.abs.toNat) (n := q.den.toNat) hgposNat
453
454/-- After signed division by orbit GCD, every `RatioOrbit` admits a balanced
455equivalent representative whose numerator absolute value is coprime to the
456denominator. -/
457def RatioNormalizationTarget : Prop :=
458 ∀ q : RatioOrbit,
459 ∃ q' : RatioOrbit,
460 RatioOrbit.crossEq q q' ∧
461 coprime q'.num.abs q'.den
462
463theorem ratio_normalization_target : RatioNormalizationTarget := by
464 intro q
465 exact ⟨normalizeRatio q, normalizeRatio_crossEq q, normalizeRatio_coprime q⟩
466
467/-- Bundling certificate for the Euclidean orbit surface closed in this pass. -/
468structure OrbitEuclideanCertificate : Prop where
469 divmod_display :
470 ∀ (n d : DistinctionNat) (hd : d ≠ zero),
471 let qr := divMod n d hd
472 qr.1.toNat = n.toNat / d.toNat ∧
473 qr.2.toNat = n.toNat % d.toNat
474 quotient_display :
475 ∀ (n d : DistinctionNat) (hd : d ≠ zero),
476 (quotient n d hd).toNat = n.toNat / d.toNat
477 remainder_display :
478 ∀ (n d : DistinctionNat) (hd : d ≠ zero),
479 (remainder n d hd).toNat = n.toNat % d.toNat
480 remainder_bound :
481 ∀ (n d : DistinctionNat) (hd : d ≠ zero),
482 (remainder n d hd).toNat < d.toNat
483 quotient_remainder_decomposition :
484 ∀ (n d : DistinctionNat) (hd : d ≠ zero),
485 quotient n d hd * d + remainder n d hd = n
486 gcd_display :
487 ∀ a b : DistinctionNat, (gcd a b).toNat = Nat.gcd a.toNat b.toNat
488 coprime_display :
489 ∀ a b : DistinctionNat, coprime a b ↔ Nat.Coprime a.toNat b.toNat
490 gcd_greatest_divisor :
491 ∀ {c a b : DistinctionNat}, divides c a → divides c b → divides c (gcd a b)
492 coprime_divisor_cancellation :
493 ∀ {a b c : DistinctionNat}, coprime b a → divides a (b * c) → divides a c
494 ratio_normalization :
495 RatioNormalizationTarget
496
497/-- The closed δ-only Euclidean orbit surface, including signed-rational
498normalization by native orbit GCD. -/
499theorem orbit_euclidean_certificate : OrbitEuclideanCertificate where
500 divmod_display := divMod_toNat
501 quotient_display := quotient_toNat
502 remainder_display := remainder_toNat
503 remainder_bound := remainder_lt_divisor
504 quotient_remainder_decomposition := quotient_mul_divisor_add_remainder_eq
505 gcd_display := gcd_toNat
506 coprime_display := coprime_iff_nat_coprime
507 gcd_greatest_divisor := by
508 intro c a b hca hcb
509 exact divides_gcd_of_divides_left_right hca hcb
510 coprime_divisor_cancellation := by
511 intro a b c hcop hdiv
512 exact coprime_divides_of_divides_mul_left hcop hdiv
513 ratio_normalization := ratio_normalization_target
514
515end DistinctionNat
516end PrimitiveRecognitionCalculus
517end Foundation
518end IndisputableMonolith
519