GT000A

euclidean_gcd_zero_terminal_unique

Any relational gcd at a zero-remainder terminal state is exactly its nonzero-side dividend, including a=0.

Alpha v34 checked-use · first admitted v22 · 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.

G101 was OPEN at this family's Alpha-v22 first admission: its complete anchored trace and actual terminal gcd were proved but its logarithmic bound was not. G101 is now CLOSED in Alpha v23, including the exact first-order bound steps≤2*BitLen(b)+1.

Exact theorem in conservative defined notation

∀ g. ∀ a. IsGCD(g,a,0) → g = a

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

Definition DAG

IsGCD(g,a,b) · 1

Actual proof prerequisites

is_gcd_zero_right · checked external prerequisiteis_gcd_unique · checked external prerequisite
Original expanded first-order statement 
forall g a. ((((exists ec_gcd_left_egt_zero. a = g * ec_gcd_left_egt_zero) /\ (exists ec_gcd_right_egt_zero. 0 = g * ec_gcd_right_egt_zero)) /\ forall ec_gcd_common_egt_zero. (exists ec_gcd_common_left_egt_zero. a = ec_gcd_common_egt_zero * ec_gcd_common_left_egt_zero) -> (exists ec_gcd_common_right_egt_zero. 0 = ec_gcd_common_egt_zero * ec_gcd_common_right_egt_zero) -> exists ec_gcd_greatest_egt_zero. g = ec_gcd_common_egt_zero * ec_gcd_greatest_egt_zero)) -> g = a

Complete unchanged native tactic proof

All 11 lines are the exact independently kernel-checked original script.

Read the argument

Proof checkpoints

11 script commands · 2 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–3

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

  1. L1
    intro g
  2. L2
    intro a
  3. L3
    intro hg
02Use earlier factsL4–11

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

  1. L4
    specialize is_gcd_unique g
  2. L5
    specialize is_gcd_unique a
  3. L6
    specialize is_gcd_unique a
  4. L7
    specialize is_gcd_unique 0
  5. L8
    apply is_gcd_unique
  6. L9
    exact hg
  7. L10
    specialize is_gcd_zero_right a
  8. L11
    exact is_gcd_zero_right

Library-wide reading audit

Original defined command ledger · 11 lines
  1. 0001intro g
  2. 0002intro a
  3. 0003intro hg
  4. 0004specialize is_gcd_unique g
  5. 0005specialize is_gcd_unique a
  6. 0006specialize is_gcd_unique a
  7. 0007specialize is_gcd_unique 0
  8. 0008apply is_gcd_unique
  9. 0009exact hg
  10. 0010specialize is_gcd_zero_right a
  11. 0011exact is_gcd_zero_right