GI0004

signed_integer_canonical_floor_exists

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

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

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

Constructive proof overview

Generated structural guide

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

The unchanged tactic script uses 3 declared prerequisites and contains 36 exact native proof lines.

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

Proof neighborhood

Direct dependencies

GI0002 signed_integer_floor_exists signed_balance_total Alpha theorem; checked-use authorized GI0003 signed_integer_floor_quotient_transport

Direct dependents

GI0005 signed_code_floor_exists

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

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.

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 : exists qp qn r. ((xp) + (m) * (qn) = ((xn) + (m) * (qp)) + (r) /\ exists sif_gap_first. sif_gap_first + S (r) = (m))
  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 exact command ledger · 36 lines
  1. 0001intro xp
  2. 0002intro xn
  3. 0003intro m
  4. 0004intro hm
  5. 0005have hfloor : exists qp qn r. ((xp) + (m) * (qn) = ((xn) + (m) * (qp)) + (r) /\ exists sif_gap_first. sif_gap_first + S (r) = (m))
  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