AF0002

foundation_signed_bezout_canonical_gcd

Alpha v34 independently verified · alpha_closed; checked-use authorized; not Stable

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.

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.

Exact expanded first-order arithmetic 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))

Constructive proof overview

Generated structural guide

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.

The unchanged tactic script uses 2 declared prerequisites and contains 24 exact native proof lines.

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

Proof neighborhood

Direct dependencies

gcd_signed_bezout_exists Alpha theorem; checked-use authorized is_gcd_unique Stable theorem; checked-use authorized

Direct dependents

none

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Local theorem links identify exact declared prerequisites. This exact body belongs to a complete independently kernel-checked constructive proof bundle and has Alpha checked-use authority; it does not imply Stable membership.

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.

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 exact 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