AF0002

foundation_signed_bezout_canonical_gcd

G002: every pair, including (0,0), has a canonical gcd value and actual signed-natural Bezout coefficient codes. Only the gcd is asserted unique, not its coefficients.

Alpha v34 checked-use · first admitted v28 · independently kernel and Lean verified; not Stable

Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved. Exact original first-admission records.

The original division, gcd, cancellation, and factor-existence foundations are exposed through checked wrappers. Unordered uniqueness adds an actual bounded, injective, surjective index map matching repeated prime occurrences. The empty factor list represents one, not zero.

Exact theorem in conservative defined notation

∀ a. ∀ b. ∃ g. ∃ u. ∃ v. IsGCD(g,a,b) ∧ (SignedBezout(g,a,b,u,v) ∧ (∀ x. IsGCD(x,a,b) → x = g))

Every linked abbreviation expands hygienically to the identical original native formula.

Definition DAG

SignedBezout(g,a,b,u,v) · 1IsGCD(g,a,b) · 2

Actual proof prerequisites

gcd_signed_bezout_exists · checked external prerequisiteis_gcd_unique · checked external prerequisite
Original expanded first-order statement 
forall a b. exists g u v. (((((exists hag_left_factor_fsat_gcd. a = g * hag_left_factor_fsat_gcd) /\ (exists hag_right_factor_fsat_gcd. b = g * hag_right_factor_fsat_gcd)) /\ forall hag_divisor_fsat_gcd. (exists hag_common_left_fsat_gcd. a = hag_divisor_fsat_gcd * hag_common_left_fsat_gcd) -> (exists hag_common_right_fsat_gcd. b = hag_divisor_fsat_gcd * hag_common_right_fsat_gcd) -> exists hag_greatest_factor_fsat_gcd. g = hag_divisor_fsat_gcd * hag_greatest_factor_fsat_gcd)) /\ ((exists sbz_xp_fsat_bezout sbz_xn_fsat_bezout sbz_yp_fsat_bezout sbz_yn_fsat_bezout. (((u = 2 * sbz_xp_fsat_bezout /\ sbz_xn_fsat_bezout = 0) \/ exists sd_half_fsat_bezout_x. ((u = 2 * sd_half_fsat_bezout_x + 1 /\ sbz_xp_fsat_bezout = 0) /\ sbz_xn_fsat_bezout = S sd_half_fsat_bezout_x)) /\ (((v = 2 * sbz_yp_fsat_bezout /\ sbz_yn_fsat_bezout = 0) \/ exists sd_half_fsat_bezout_y. ((v = 2 * sd_half_fsat_bezout_y + 1 /\ sbz_yp_fsat_bezout = 0) /\ sbz_yn_fsat_bezout = S sd_half_fsat_bezout_y)) /\ a * sbz_xp_fsat_bezout + b * sbz_yp_fsat_bezout = g + (a * sbz_xn_fsat_bezout + b * sbz_yn_fsat_bezout)))) /\ forall h. ((((exists hag_left_factor_fsat_comparison. a = h * hag_left_factor_fsat_comparison) /\ (exists hag_right_factor_fsat_comparison. b = h * hag_right_factor_fsat_comparison)) /\ forall hag_divisor_fsat_comparison. (exists hag_common_left_fsat_comparison. a = hag_divisor_fsat_comparison * hag_common_left_fsat_comparison) -> (exists hag_common_right_fsat_comparison. b = hag_divisor_fsat_comparison * hag_common_right_fsat_comparison) -> exists hag_greatest_factor_fsat_comparison. h = hag_divisor_fsat_comparison * hag_greatest_factor_fsat_comparison)) -> h = g))

Complete tactic proof in conservative notation

All 24 original proof lines are preserved. Only local proposition formulas are abbreviated; every abbreviation has an exact binder-safe expansion check. The linked exact edition contains the unchanged replay script.

Read the argument

Proof checkpoints

24 script commands · 10 reading checkpoints · 0 local claims

This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.

Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.

01Fix variables and assumptionsL1–2

Work with arbitrary variables or the premises of the current implication.

  1. L1
    intro a
  2. L2
    intro b
02Use earlier factsL3–4

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L3
    specialize gcd_signed_bezout_exists a
  2. L4
    specialize gcd_signed_bezout_exists b
03Separate the logical casesL5–8

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L5
    cases gcd_signed_bezout_exists
  2. L6
    cases gcd_signed_bezout_exists_witness
  3. L7
    cases gcd_signed_bezout_exists_witness_witness
  4. L8
    cases gcd_signed_bezout_exists_witness_witness_witness
04Construct an explicit witnessL9–11

Supply the displayed value, then prove that it has the required property.

  1. L9
    exists x
  2. L10
    exists x1
  3. L11
    exists x2
05Separate the logical casesL12–12

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L12
    split
06Use earlier factsL13–13

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L13
    exact gcd_signed_bezout_exists_witness_witness_witness_left
07Separate the logical casesL14–14

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L14
    split
08Use earlier factsL15–15

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L15
    exact gcd_signed_bezout_exists_witness_witness_witness_right
09Fix variables and assumptionsL16–17

Work with arbitrary variables or the premises of the current implication.

  1. L16
    intro h
  2. L17
    intro hh
10Use earlier factsL18–24

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L18
    specialize is_gcd_unique (h)
  2. L19
    specialize is_gcd_unique (x)
  3. L20
    specialize is_gcd_unique (a)
  4. L21
    specialize is_gcd_unique (b)
  5. L22
    apply is_gcd_unique
  6. L23
    exact hh
  7. L24
    exact gcd_signed_bezout_exists_witness_witness_witness_left

Library-wide reading audit

Original defined command ledger · 24 lines
  1. 0001intro a
  2. 0002intro b
  3. 0003specialize gcd_signed_bezout_exists a
  4. 0004specialize gcd_signed_bezout_exists b
  5. 0005cases gcd_signed_bezout_exists
  6. 0006cases gcd_signed_bezout_exists_witness
  7. 0007cases gcd_signed_bezout_exists_witness_witness
  8. 0008cases gcd_signed_bezout_exists_witness_witness_witness
  9. 0009exists x
  10. 0010exists x1
  11. 0011exists x2
  12. 0012split
  13. 0013exact gcd_signed_bezout_exists_witness_witness_witness_left
  14. 0014split
  15. 0015exact gcd_signed_bezout_exists_witness_witness_witness_right
  16. 0016intro h
  17. 0017intro hh
  18. 0018specialize is_gcd_unique (h)
  19. 0019specialize is_gcd_unique (x)
  20. 0020specialize is_gcd_unique (a)
  21. 0021specialize is_gcd_unique (b)
  22. 0022apply is_gcd_unique
  23. 0023exact hh
  24. 0024exact gcd_signed_bezout_exists_witness_witness_witness_left