GI0004

signed_integer_canonical_floor_exists

The constructed floor quotient has an actual canonical historic signed-integer code, with its normalized decoder witnesses.

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 natural-code carrier consists of genuine pairs of the existing signed integers; no new primitive arithmetic is trusted. The theorem constructs quotient, remainder, and actual norm witnesses. Gaussian gcd, unique factorization, and prime classification are separate targets.

Exact theorem in conservative defined notation

∀ xp. ∀ xn. ∀ m. ¬m = 0 → ∃ x. ∃ y. ∃ z. ∃ n. SignedDecode(x,y,z) ∧ SignedFloor(xp,xn,m,y,z,n)

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

Definition DAG

SignedDecode(z,p,n) · 1SignedFloor(p,n,m,q,t,r) · 2

Actual proof prerequisites

signed_integer_floor_existssigned_balance_total · checked external prerequisitesigned_integer_floor_quotient_transport
Original expanded first-order statement 
forall xp xn m. ~(m = 0) -> exists code qp qn r. ((code = 2 * qp /\ qn = 0) \/ exists sd_half_sif_canonical. ((code = 2 * sd_half_sif_canonical + 1 /\ qp = 0) /\ qn = S sd_half_sif_canonical)) /\ (((xp) + (m) * (qn) = ((xn) + (m) * (qp)) + (r) /\ exists sif_gap_canonical. sif_gap_canonical + S (r) = (m)))

Complete tactic proof in conservative notation

All 36 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

36 script commands · 9 reading checkpoints · 1 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.

Named ingredients (2)
signed integer floor existssigned integer floor quotient transport
01Fix variables and assumptionsL1–4

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

  1. L1
    intro xp
  2. L2
    intro xn
  3. L3
    intro m
  4. L4
    intro hm
02Establish hfloorL5–10

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply signed integer floor exists.

  1. L5
    have hfloor : ∃ qp. ∃ qn. ∃ r. SignedFloor(xp,xn,m,qp,qn,r)Definitions: SignedFloor(xp,xn,m,qp,qn,r)Original native command in the exact edition
  2. L6
    specialize signed_integer_floor_exists xp
  3. L7
    specialize signed_integer_floor_exists xn
  4. L8
    specialize signed_integer_floor_exists m
  5. L9
    apply signed_integer_floor_exists
  6. L10
    exact hm
03Separate the logical casesL11–13

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

  1. L11
    cases hfloor
  2. L12
    cases hfloor_witness
  3. L13
    cases hfloor_witness_witness
04Use earlier factsL14–15

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

  1. L14
    specialize signed_balance_total x
  2. L15
    specialize signed_balance_total x1
05Separate the logical casesL16–19

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

  1. L16
    cases signed_balance_total
  2. L17
    cases signed_balance_total_witness
  3. L18
    cases signed_balance_total_witness_witness
  4. L19
    cases signed_balance_total_witness_witness_witness
06Construct an explicit witnessL20–23

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

  1. L20
    exists x3
  2. L21
    exists x4
  3. L22
    exists x5
  4. L23
    exists x2
07Separate the logical casesL24–24

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

  1. L24
    split
08Use earlier factsL25–34

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

  1. L25
    exact signed_balance_total_witness_witness_witness_left
  2. L26
    specialize signed_integer_floor_quotient_transport xp
  3. L27
    specialize signed_integer_floor_quotient_transport xn
  4. L28
    specialize signed_integer_floor_quotient_transport m
  5. L29
    specialize signed_integer_floor_quotient_transport x
  6. L30
    specialize signed_integer_floor_quotient_transport x1
  7. L31
    specialize signed_integer_floor_quotient_transport x4
  8. L32
    specialize signed_integer_floor_quotient_transport x5
  9. L33
    specialize signed_integer_floor_quotient_transport x2
  10. L34
    apply signed_integer_floor_quotient_transport
09Use earlier factsL35–36

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

  1. L35
    exact signed_balance_total_witness_witness_witness_right
  2. L36
    exact hfloor_witness_witness_witness

Library-wide reading audit

Original defined command ledger · 36 lines
  1. 0001intro xp
  2. 0002intro xn
  3. 0003intro m
  4. 0004intro hm
  5. 0005have hfloor : ∃ qp. ∃ qn. ∃ r. SignedFloor(xp,xn,m,qp,qn,r)
  6. 0006specialize signed_integer_floor_exists xp
  7. 0007specialize signed_integer_floor_exists xn
  8. 0008specialize signed_integer_floor_exists m
  9. 0009apply signed_integer_floor_exists
  10. 0010exact hm
  11. 0011cases hfloor
  12. 0012cases hfloor_witness
  13. 0013cases hfloor_witness_witness
  14. 0014specialize signed_balance_total x
  15. 0015specialize signed_balance_total x1
  16. 0016cases signed_balance_total
  17. 0017cases signed_balance_total_witness
  18. 0018cases signed_balance_total_witness_witness
  19. 0019cases signed_balance_total_witness_witness_witness
  20. 0020exists x3
  21. 0021exists x4
  22. 0022exists x5
  23. 0023exists x2
  24. 0024split
  25. 0025exact signed_balance_total_witness_witness_witness_left
  26. 0026specialize signed_integer_floor_quotient_transport xp
  27. 0027specialize signed_integer_floor_quotient_transport xn
  28. 0028specialize signed_integer_floor_quotient_transport m
  29. 0029specialize signed_integer_floor_quotient_transport x
  30. 0030specialize signed_integer_floor_quotient_transport x1
  31. 0031specialize signed_integer_floor_quotient_transport x4
  32. 0032specialize signed_integer_floor_quotient_transport x5
  33. 0033specialize signed_integer_floor_quotient_transport x2
  34. 0034apply signed_integer_floor_quotient_transport
  35. 0035exact signed_balance_total_witness_witness_witness_right
  36. 0036exact hfloor_witness_witness_witness