MX003E

signed_support_incidence_flat_entry_coordinates

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

Uniqueness of actual quotient and strict remainder recovers the specified incidence coordinates.

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 A r s M i j z. (exists pvs_gap_flat_column_bound. pvs_gap_flat_column_bound + S (j) = (S M)) -> (exists ssr_flat_row_flat_read ssr_flat_column_flat_read. (((((S (M))*(i)+(j)))=(((S (M))*(ssr_flat_row_flat_read)+(ssr_flat_column_flat_read)))) /\ (((exists pvs_gap_flat_readremainder. pvs_gap_flat_readremainder + S (ssr_flat_column_flat_read) = (S (M))) /\ (exists ssr_entry_value_flat_readentry ssr_entry_image_flat_readentry. ((exists dst_positive_code_flat_readentrysource dst_positive_scale_flat_readentrysource dst_negative_code_flat_readentrysource dst_negative_scale_flat_readentrysource dst_positive_flat_readentrysource dst_negative_flat_readentrysource. (((A) = (((((dst_positive_code_flat_readentrysource) + (dst_positive_scale_flat_readentrysource)) * S ((dst_positive_code_flat_readentrysource) + (dst_positive_scale_flat_readentrysource)) + ((dst_positive_scale_flat_readentrysource) + (dst_positive_scale_flat_readentrysource))) + (((dst_negative_code_flat_readentrysource) + (dst_negative_scale_flat_readentrysource)) * S ((dst_negative_code_flat_readentrysource) + (dst_negative_scale_flat_readentrysource)) + ((dst_negative_scale_flat_readentrysource) + (dst_negative_scale_flat_readentrysource)))) * S ((((dst_positive_code_flat_readentrysource) + (dst_positive_scale_flat_readentrysource)) * S ((dst_positive_code_flat_readentrysource) + (dst_positive_scale_flat_readentrysource)) + ((dst_positive_scale_flat_readentrysource) + (dst_positive_scale_flat_readentrysource))) + (((dst_negative_code_flat_readentrysource) + (dst_negative_scale_flat_readentrysource)) * S ((dst_negative_code_flat_readentrysource) + (dst_negative_scale_flat_readentrysource)) + ((dst_negative_scale_flat_readentrysource) + (dst_negative_scale_flat_readentrysource)))) + ((((dst_negative_code_flat_readentrysource) + (dst_negative_scale_flat_readentrysource)) * S ((dst_negative_code_flat_readentrysource) + (dst_negative_scale_flat_readentrysource)) + ((dst_negative_scale_flat_readentrysource) + (dst_negative_scale_flat_readentrysource))) + (((dst_negative_code_flat_readentrysource) + (dst_negative_scale_flat_readentrysource)) * S ((dst_negative_code_flat_readentrysource) + (dst_negative_scale_flat_readentrysource)) + ((dst_negative_scale_flat_readentrysource) + (dst_negative_scale_flat_readentrysource)))))) /\ (((((exists ff_h_pvs_flat_readentrysourcepositive. ff_h_pvs_flat_readentrysourcepositive + S (dst_positive_flat_readentrysource) = S ((S (ssr_flat_row_flat_read)) * dst_positive_scale_flat_readentrysource)) /\ exists ff_q_pvs_flat_readentrysourcepositive. dst_positive_code_flat_readentrysource = ff_q_pvs_flat_readentrysourcepositive * S ((S (ssr_flat_row_flat_read)) * dst_positive_scale_flat_readentrysource) + (dst_positive_flat_readentrysource))) /\ (((((exists ff_h_pvs_flat_readentrysourcenegative. ff_h_pvs_flat_readentrysourcenegative + S (dst_negative_flat_readentrysource) = S ((S (ssr_flat_row_flat_read)) * dst_negative_scale_flat_readentrysource)) /\ exists ff_q_pvs_flat_readentrysourcenegative. dst_negative_code_flat_readentrysource = ff_q_pvs_flat_readentrysourcenegative * S ((S (ssr_flat_row_flat_read)) * dst_negative_scale_flat_readentrysource) + (dst_negative_flat_readentrysource))) /\ (exists ge_balance_positive_flat_readentrysourcevalue ge_balance_negative_flat_readentrysourcevalue. (((((ssr_entry_value_flat_readentry) = 2 * (ge_balance_positive_flat_readentrysourcevalue) /\ (ge_balance_negative_flat_readentrysourcevalue) = 0) \/ exists ge_signed_half_flat_readentrysourcevaluedecode. (((ssr_entry_value_flat_readentry) = 2 * ge_signed_half_flat_readentrysourcevaluedecode + 1 /\ (ge_balance_positive_flat_readentrysourcevalue) = 0) /\ (ge_balance_negative_flat_readentrysourcevalue) = S ge_signed_half_flat_readentrysourcevaluedecode))) /\ ((dst_positive_flat_readentrysource) + ge_balance_negative_flat_readentrysourcevalue = (dst_negative_flat_readentrysource) + ge_balance_positive_flat_readentrysourcevalue))))))))) /\ (((((exists ff_h_pvs_flat_readentrymap. ff_h_pvs_flat_readentrymap + S (ssr_entry_image_flat_readentry) = S ((S (ssr_flat_row_flat_read)) * s)) /\ exists ff_q_pvs_flat_readentrymap. r = ff_q_pvs_flat_readentrymap * S ((S (ssr_flat_row_flat_read)) * s) + (ssr_entry_image_flat_readentry))) /\ (((((ssr_flat_column_flat_read)=(ssr_entry_image_flat_readentry)) /\ ((z)=(ssr_entry_value_flat_readentry)))) \/ (((~((ssr_flat_column_flat_read)=(ssr_entry_image_flat_readentry))) /\ ((z)=0)))))))))))) -> (exists ssr_entry_value_flat_coordinates ssr_entry_image_flat_coordinates. ((exists dst_positive_code_flat_coordinatessource dst_positive_scale_flat_coordinatessource dst_negative_code_flat_coordinatessource dst_negative_scale_flat_coordinatessource dst_positive_flat_coordinatessource dst_negative_flat_coordinatessource. (((A) = (((((dst_positive_code_flat_coordinatessource) + (dst_positive_scale_flat_coordinatessource)) * S ((dst_positive_code_flat_coordinatessource) + (dst_positive_scale_flat_coordinatessource)) + ((dst_positive_scale_flat_coordinatessource) + (dst_positive_scale_flat_coordinatessource))) + (((dst_negative_code_flat_coordinatessource) + (dst_negative_scale_flat_coordinatessource)) * S ((dst_negative_code_flat_coordinatessource) + (dst_negative_scale_flat_coordinatessource)) + ((dst_negative_scale_flat_coordinatessource) + (dst_negative_scale_flat_coordinatessource)))) * S ((((dst_positive_code_flat_coordinatessource) + (dst_positive_scale_flat_coordinatessource)) * S ((dst_positive_code_flat_coordinatessource) + (dst_positive_scale_flat_coordinatessource)) + ((dst_positive_scale_flat_coordinatessource) + (dst_positive_scale_flat_coordinatessource))) + (((dst_negative_code_flat_coordinatessource) + (dst_negative_scale_flat_coordinatessource)) * S ((dst_negative_code_flat_coordinatessource) + (dst_negative_scale_flat_coordinatessource)) + ((dst_negative_scale_flat_coordinatessource) + (dst_negative_scale_flat_coordinatessource)))) + ((((dst_negative_code_flat_coordinatessource) + (dst_negative_scale_flat_coordinatessource)) * S ((dst_negative_code_flat_coordinatessource) + (dst_negative_scale_flat_coordinatessource)) + ((dst_negative_scale_flat_coordinatessource) + (dst_negative_scale_flat_coordinatessource))) + (((dst_negative_code_flat_coordinatessource) + (dst_negative_scale_flat_coordinatessource)) * S ((dst_negative_code_flat_coordinatessource) + (dst_negative_scale_flat_coordinatessource)) + ((dst_negative_scale_flat_coordinatessource) + (dst_negative_scale_flat_coordinatessource)))))) /\ (((((exists ff_h_pvs_flat_coordinatessourcepositive. ff_h_pvs_flat_coordinatessourcepositive + S (dst_positive_flat_coordinatessource) = S ((S (i)) * dst_positive_scale_flat_coordinatessource)) /\ exists ff_q_pvs_flat_coordinatessourcepositive. dst_positive_code_flat_coordinatessource = ff_q_pvs_flat_coordinatessourcepositive * S ((S (i)) * dst_positive_scale_flat_coordinatessource) + (dst_positive_flat_coordinatessource))) /\ (((((exists ff_h_pvs_flat_coordinatessourcenegative. ff_h_pvs_flat_coordinatessourcenegative + S (dst_negative_flat_coordinatessource) = S ((S (i)) * dst_negative_scale_flat_coordinatessource)) /\ exists ff_q_pvs_flat_coordinatessourcenegative. dst_negative_code_flat_coordinatessource = ff_q_pvs_flat_coordinatessourcenegative * S ((S (i)) * dst_negative_scale_flat_coordinatessource) + (dst_negative_flat_coordinatessource))) /\ (exists ge_balance_positive_flat_coordinatessourcevalue ge_balance_negative_flat_coordinatessourcevalue. (((((ssr_entry_value_flat_coordinates) = 2 * (ge_balance_positive_flat_coordinatessourcevalue) /\ (ge_balance_negative_flat_coordinatessourcevalue) = 0) \/ exists ge_signed_half_flat_coordinatessourcevaluedecode. (((ssr_entry_value_flat_coordinates) = 2 * ge_signed_half_flat_coordinatessourcevaluedecode + 1 /\ (ge_balance_positive_flat_coordinatessourcevalue) = 0) /\ (ge_balance_negative_flat_coordinatessourcevalue) = S ge_signed_half_flat_coordinatessourcevaluedecode))) /\ ((dst_positive_flat_coordinatessource) + ge_balance_negative_flat_coordinatessourcevalue = (dst_negative_flat_coordinatessource) + ge_balance_positive_flat_coordinatessourcevalue))))))))) /\ (((((exists ff_h_pvs_flat_coordinatesmap. ff_h_pvs_flat_coordinatesmap + S (ssr_entry_image_flat_coordinates) = S ((S (i)) * s)) /\ exists ff_q_pvs_flat_coordinatesmap. r = ff_q_pvs_flat_coordinatesmap * S ((S (i)) * s) + (ssr_entry_image_flat_coordinates))) /\ (((((j)=(ssr_entry_image_flat_coordinates)) /\ ((z)=(ssr_entry_value_flat_coordinates)))) \/ (((~((j)=(ssr_entry_image_flat_coordinates))) /\ ((z)=0))))))))

Constructive proof overview

Generated structural guide

Uniqueness of actual quotient and strict remainder recovers the specified incidence coordinates.

The unchanged tactic script uses 1 declared prerequisite and contains 35 exact native proof lines.

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

Proof neighborhood

Direct dependencies

division_remainder_unique Stable theorem; checked-use authorized

Direct dependents

MX0042 signed_support_incidence_from_flat_prefix

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

35 script commands · 8 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.

01Fix variables and assumptionsL1–9

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

  1. L1
    intro A
  2. L2
    intro r
  3. L3
    intro s
  4. L4
    intro M
  5. L5
    intro i
  6. L6
    intro j
  7. L7
    intro z
  8. L8
    intro hj
  9. L9
    intro hv
02Separate the logical casesL10–13

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

  1. L10
    cases hv
  2. L11
    cases hv_witness
  3. L12
    cases hv_witness_witness
  4. L13
    cases hv_witness_witness_right
03Establish heL14–23

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

  1. L14
    have he : x=i /\ x1=j
  2. L15
    specialize division_remainder_unique (S M)
  3. L16
    specialize division_remainder_unique (((S (M))*(i)+(j)))
  4. L17
    specialize division_remainder_unique (x)
  5. L18
    specialize division_remainder_unique (x1)
  6. L19
    specialize division_remainder_unique (i)
  7. L20
    specialize division_remainder_unique (j)
  8. L21
    apply division_remainder_unique
  9. L22
    exact hv_witness_witness_left
  10. L23
    exact hv_witness_witness_right_left
04Calculate and transport equalitiesL24–24

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L24
    refl
05Use earlier factsL25–25

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

  1. L25
    exact hj
06Separate the logical casesL26–26

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

  1. L26
    cases he
07Calculate and transport equalitiesL27–34

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L27
    rewrite he_left at hv_witness_witness_right_right
  2. L28
    rewrite he_left at hv_witness_witness_right_right
  3. L29
    rewrite he_left at hv_witness_witness_right_right
  4. L30
    rewrite he_left at hv_witness_witness_right_right
  5. L31
    rewrite he_left at hv_witness_witness_right_right
  6. L32
    rewrite he_left at hv_witness_witness_right_right
  7. L33
    rewrite he_right at hv_witness_witness_right_right
  8. L34
    rewrite he_right at hv_witness_witness_right_right
08Use earlier factsL35–35

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

  1. L35
    exact hv_witness_witness_right_right

Library-wide reading audit

Original exact command ledger · 35 lines
  1. 0001intro A
  2. 0002intro r
  3. 0003intro s
  4. 0004intro M
  5. 0005intro i
  6. 0006intro j
  7. 0007intro z
  8. 0008intro hj
  9. 0009intro hv
  10. 0010cases hv
  11. 0011cases hv_witness
  12. 0012cases hv_witness_witness
  13. 0013cases hv_witness_witness_right
  14. 0014have he : x=i /\ x1=j
  15. 0015specialize division_remainder_unique (S M)
  16. 0016specialize division_remainder_unique (((S (M))*(i)+(j)))
  17. 0017specialize division_remainder_unique (x)
  18. 0018specialize division_remainder_unique (x1)
  19. 0019specialize division_remainder_unique (i)
  20. 0020specialize division_remainder_unique (j)
  21. 0021apply division_remainder_unique
  22. 0022exact hv_witness_witness_left
  23. 0023exact hv_witness_witness_right_left
  24. 0024refl
  25. 0025exact hj
  26. 0026cases he
  27. 0027rewrite he_left at hv_witness_witness_right_right
  28. 0028rewrite he_left at hv_witness_witness_right_right
  29. 0029rewrite he_left at hv_witness_witness_right_right
  30. 0030rewrite he_left at hv_witness_witness_right_right
  31. 0031rewrite he_left at hv_witness_witness_right_right
  32. 0032rewrite he_left at hv_witness_witness_right_right
  33. 0033rewrite he_right at hv_witness_witness_right_right
  34. 0034rewrite he_right at hv_witness_witness_right_right
  35. 0035exact hv_witness_witness_right_right