MX002E

signed_cartesian_coordinates_exists

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

Every actual index in a finite rectangular window has constructed bounded row and column coordinates, with no positive-width assumption supplied.

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

forall m n k. (exists pvs_gap_coordinate_source. pvs_gap_coordinate_source + S (k) = (m*n)) -> (exists scp_coordinate_row_coordinate_result scp_coordinate_column_coordinate_result. (((k)=((n)*(scp_coordinate_row_coordinate_result)+(scp_coordinate_column_coordinate_result))) /\ (((exists pvs_gap_coordinate_resultrow. pvs_gap_coordinate_resultrow + S (scp_coordinate_row_coordinate_result) = (m)) /\ (exists pvs_gap_coordinate_resultcolumn. pvs_gap_coordinate_resultcolumn + S (scp_coordinate_column_coordinate_result) = (n))))))

Constructive proof overview

Generated structural guide

Every actual index in a finite rectangular window has constructed bounded row and column coordinates, with no positive-width assumption supplied.

The unchanged tactic script uses 4 declared prerequisites and contains 38 exact native proof lines.

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

Proof neighborhood

Direct dependencies

lt_not_le Stable theorem; checked-use authorized zero_le Stable theorem; checked-use authorized division_remainder_exists Stable theorem; checked-use authorized MX002D signed_cartesian_quotient_row_bound

Direct dependents

MX002F signed_cartesian_product_flat_lookup MX0030 signed_cartesian_product_extensional_unique

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

38 script commands · 10 reading checkpoints · 3 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 (1)
signed cartesian quotient row bound
01Fix variables and assumptionsL1–4

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

  1. L1
    intro m
  2. L2
    intro n
  3. L3
    intro k
  4. L4
    intro hk
02Establish hnL5–6

Establish this local claim before using it. It is not an additional assumption.

  1. L5
    have hn : ~(n=0)
  2. L6
    intro hnzero
03Establish hlengthL7–16

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply lt not le.

  1. L7
    have hlength : m*n=0
  2. L8
    rewrite hnzero
  3. L9
    simp
  4. L10
    rewrite hlength at hk
  5. L11
    specialize lt_not_le (k)
  6. L12
    specialize lt_not_le (0)
  7. L13
    apply lt_not_le
  8. L14
    exact hk
  9. L15
    specialize zero_le (k)
  10. L16
    apply zero_le
04Establish hdL17–21

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

  1. L17
    have hd : exists i j. ((k=n*i+j) /\ (exists pvs_gap_coordinate_division. pvs_gap_coordinate_division + S (j) = (n)))
  2. L18
    specialize division_remainder_exists (n)
  3. L19
    specialize division_remainder_exists (k)
  4. L20
    apply division_remainder_exists
  5. L21
    exact hn
05Separate the logical casesL22–24

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

  1. L22
    cases hd
  2. L23
    cases hd_witness
  3. L24
    cases hd_witness_witness
06Construct an explicit witnessL25–26

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

  1. L25
    exists x
  2. L26
    exists x1
07Separate the logical casesL27–27

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

  1. L27
    split
08Use earlier factsL28–28

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

  1. L28
    exact hd_witness_witness_left
09Separate the logical casesL29–29

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

  1. L29
    split
10Use earlier factsL30–38

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

  1. L30
    specialize signed_cartesian_quotient_row_bound (m)
  2. L31
    specialize signed_cartesian_quotient_row_bound (n)
  3. L32
    specialize signed_cartesian_quotient_row_bound (k)
  4. L33
    specialize signed_cartesian_quotient_row_bound (x)
  5. L34
    specialize signed_cartesian_quotient_row_bound (x1)
  6. L35
    apply signed_cartesian_quotient_row_bound
  7. L36
    exact hd_witness_witness_left
  8. L37
    exact hk
  9. L38
    exact hd_witness_witness_right

Library-wide reading audit

Original exact command ledger · 38 lines
  1. 0001intro m
  2. 0002intro n
  3. 0003intro k
  4. 0004intro hk
  5. 0005have hn : ~(n=0)
  6. 0006intro hnzero
  7. 0007have hlength : m*n=0
  8. 0008rewrite hnzero
  9. 0009simp
  10. 0010rewrite hlength at hk
  11. 0011specialize lt_not_le (k)
  12. 0012specialize lt_not_le (0)
  13. 0013apply lt_not_le
  14. 0014exact hk
  15. 0015specialize zero_le (k)
  16. 0016apply zero_le
  17. 0017have hd : exists i j. ((k=n*i+j) /\ (exists pvs_gap_coordinate_division. pvs_gap_coordinate_division + S (j) = (n)))
  18. 0018specialize division_remainder_exists (n)
  19. 0019specialize division_remainder_exists (k)
  20. 0020apply division_remainder_exists
  21. 0021exact hn
  22. 0022cases hd
  23. 0023cases hd_witness
  24. 0024cases hd_witness_witness
  25. 0025exists x
  26. 0026exists x1
  27. 0027split
  28. 0028exact hd_witness_witness_left
  29. 0029split
  30. 0030specialize signed_cartesian_quotient_row_bound (m)
  31. 0031specialize signed_cartesian_quotient_row_bound (n)
  32. 0032specialize signed_cartesian_quotient_row_bound (k)
  33. 0033specialize signed_cartesian_quotient_row_bound (x)
  34. 0034specialize signed_cartesian_quotient_row_bound (x1)
  35. 0035apply signed_cartesian_quotient_row_bound
  36. 0036exact hd_witness_witness_left
  37. 0037exact hk
  38. 0038exact hd_witness_witness_right