MX0014

divisor_pair_index_map_append

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

Actual bounded quotient and remainder determine the next product value; beta-prefix extension constructs new codes and preserves all earlier decoded entries.

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 V L r s. (((~((V)=0)) /\ (forall dpi_index_dpi_append_source dpi_row_dpi_append_source dpi_column_dpi_append_source. (exists pvs_gap_dpi_append_sourcewindow. pvs_gap_dpi_append_sourcewindow + S (dpi_index_dpi_append_source) = (L)) -> (exists pvs_gap_dpi_append_sourceremainder. pvs_gap_dpi_append_sourceremainder + S (dpi_column_dpi_append_source) = (V)) -> (dpi_index_dpi_append_source)=(V)*(dpi_row_dpi_append_source)+(dpi_column_dpi_append_source) -> (((exists ff_h_pvs_dpi_append_sourcevalue. ff_h_pvs_dpi_append_sourcevalue + S ((dpi_row_dpi_append_source)*(dpi_column_dpi_append_source)) = S ((S (dpi_index_dpi_append_source)) * s)) /\ exists ff_q_pvs_dpi_append_sourcevalue. r = ff_q_pvs_dpi_append_sourcevalue * S ((S (dpi_index_dpi_append_source)) * s) + ((dpi_row_dpi_append_source)*(dpi_column_dpi_append_source))))))) -> exists t u. ((((~((V)=0)) /\ (forall dpi_index_dpi_append_target dpi_row_dpi_append_target dpi_column_dpi_append_target. (exists pvs_gap_dpi_append_targetwindow. pvs_gap_dpi_append_targetwindow + S (dpi_index_dpi_append_target) = (S L)) -> (exists pvs_gap_dpi_append_targetremainder. pvs_gap_dpi_append_targetremainder + S (dpi_column_dpi_append_target) = (V)) -> (dpi_index_dpi_append_target)=(V)*(dpi_row_dpi_append_target)+(dpi_column_dpi_append_target) -> (((exists ff_h_pvs_dpi_append_targetvalue. ff_h_pvs_dpi_append_targetvalue + S ((dpi_row_dpi_append_target)*(dpi_column_dpi_append_target)) = S ((S (dpi_index_dpi_append_target)) * u)) /\ exists ff_q_pvs_dpi_append_targetvalue. t = ff_q_pvs_dpi_append_targetvalue * S ((S (dpi_index_dpi_append_target)) * u) + ((dpi_row_dpi_append_target)*(dpi_column_dpi_append_target))))))) /\ (forall pfp_i_pvs_dpi_append_old_entries pfp_a_pvs_dpi_append_old_entries. (exists pfp_gap_pvs_dpi_append_old_entriesbound. pfp_gap_pvs_dpi_append_old_entriesbound + S (pfp_i_pvs_dpi_append_old_entries) = (L)) -> (((exists ff_h_pfp_pvs_dpi_append_old_entriesold. ff_h_pfp_pvs_dpi_append_old_entriesold + S (pfp_a_pvs_dpi_append_old_entries) = S ((S (pfp_i_pvs_dpi_append_old_entries)) * s)) /\ exists ff_q_pfp_pvs_dpi_append_old_entriesold. r = ff_q_pfp_pvs_dpi_append_old_entriesold * S ((S (pfp_i_pvs_dpi_append_old_entries)) * s) + (pfp_a_pvs_dpi_append_old_entries))) -> (((exists ff_h_pfp_pvs_dpi_append_old_entriesnew. ff_h_pfp_pvs_dpi_append_old_entriesnew + S (pfp_a_pvs_dpi_append_old_entries) = S ((S (pfp_i_pvs_dpi_append_old_entries)) * u)) /\ exists ff_q_pfp_pvs_dpi_append_old_entriesnew. t = ff_q_pfp_pvs_dpi_append_old_entriesnew * S ((S (pfp_i_pvs_dpi_append_old_entries)) * u) + (pfp_a_pvs_dpi_append_old_entries)))))

Constructive proof overview

Generated structural guide

Actual bounded quotient and remainder determine the next product value; beta-prefix extension constructs new codes and preserves all earlier decoded entries.

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

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

Proof neighborhood

Direct dependencies

division_remainder_exists Stable theorem; checked-use authorized beta_prefix_extend Stable theorem; checked-use authorized finite_lt_succ_eq_or_lt Stable theorem; checked-use authorized division_remainder_unique Stable theorem; checked-use authorized

Direct dependents

MX0015 divisor_pair_index_map_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

77 script commands · 19 reading checkpoints · 5 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.

Long local formulas use this family’s existing definitions. Each new abbreviation was expanded back to the identical native formula, including its free-variable context. The original edition is preserved below.

01Fix variables and assumptionsL1–5

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

  1. L1
    intro V
  2. L2
    intro L
  3. L3
    intro r
  4. L4
    intro s
  5. L5
    intro hm
02Separate the logical casesL6–6

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

  1. L6
    cases hm
03Establish hcoordsL7–11

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

  1. L7
    have hcoords : exists d e. (((L=V*d+e) /\ (exists pvs_gap_dpi_append_remainder. pvs_gap_dpi_append_remainder + S (e) = (V))))
  2. L8
    specialize division_remainder_exists (V)
  3. L9
    specialize division_remainder_exists (L)
  4. L10
    apply division_remainder_exists
  5. L11
    exact hm_left
04Separate the logical casesL12–14

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

  1. L12
    cases hcoords
  2. L13
    cases hcoords_witness
  3. L14
    cases hcoords_witness_witness
05Establish hextL15–20

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta prefix extend.

  1. L15
    have hext : ∃ t. ∃ u. BetaAt(t,u,L,x · x1) ∧ (∀ y. ∀ z. Lt(y,L) → BetaAt(r,s,y,z) → BetaAt(t,u,y,z))Definitions: LtBetaAt
  2. L16
    specialize beta_prefix_extend (L)
  3. L17
    specialize beta_prefix_extend (r)
  4. L18
    specialize beta_prefix_extend (s)
  5. L19
    specialize beta_prefix_extend (x*x1)
  6. L20
    apply beta_prefix_extend
06Separate the logical casesL21–23

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

  1. L21
    cases hext
  2. L22
    cases hext_witness
  3. L23
    cases hext_witness_witness
07Construct an explicit witnessL24–25

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

  1. L24
    exists x2
  2. L25
    exists x3
08Separate the logical casesL26–27

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

  1. L26
    split
  2. L27
    split
09Use earlier factsL28–28

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

  1. L28
    exact hm_left
10Fix variables and assumptionsL29–34

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

  1. L29
    intro i
  2. L30
    intro d
  3. L31
    intro e
  4. L32
    intro hi
  5. L33
    intro he
  6. L34
    intro heq
11Establish hcaseL35–39

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

  1. L35
    have hcase : i=L \/ (exists pvs_gap_dpi_append_cases. pvs_gap_dpi_append_cases + S (i) = (L))
  2. L36
    specialize finite_lt_succ_eq_or_lt (L)
  3. L37
    specialize finite_lt_succ_eq_or_lt (i)
  4. L38
    apply finite_lt_succ_eq_or_lt
  5. L39
    exact hi
12Separate the logical casesL40–40

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

  1. L40
    cases hcase
13Establish hnewL41–45

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

  1. L41
    have hnew : L=V*d+e
  2. L42
    trans i
  3. L43
    symm
  4. L44
    exact hcase_left
  5. L45
    exact heq
14Establish hsameL46–55

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

  1. L46
    have hsame : d=x /\ e=x1
  2. L47
    specialize division_remainder_unique (V)
  3. L48
    specialize division_remainder_unique (L)
  4. L49
    specialize division_remainder_unique (d)
  5. L50
    specialize division_remainder_unique (e)
  6. L51
    specialize division_remainder_unique (x)
  7. L52
    specialize division_remainder_unique (x1)
  8. L53
    apply division_remainder_unique
  9. L54
    exact hnew
  10. L55
    exact he
15Use earlier factsL56–57

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

  1. L56
    exact hcoords_witness_witness_left
  2. L57
    exact hcoords_witness_witness_right
16Separate the logical casesL58–58

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

  1. L58
    cases hsame
17Calculate and transport equalitiesL59–64

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

  1. L59
    rewrite hcase_left
  2. L60
    rewrite hcase_left
  3. L61
    rewrite hsame_left
  4. L62
    rewrite hsame_left
  5. L63
    rewrite hsame_right
  6. L64
    rewrite hsame_right
18Use earlier factsL65–74

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

  1. L65
    exact hext_witness_witness_left
  2. L66
    specialize hext_witness_witness_right (i)
  3. L67
    specialize hext_witness_witness_right (d*e)
  4. L68
    apply hext_witness_witness_right
  5. L69
    exact hcase_right
  6. L70
    specialize hm_right (i)
  7. L71
    specialize hm_right (d)
  8. L72
    specialize hm_right (e)
  9. L73
    apply hm_right
  10. L74
    exact hcase_right
19Use earlier factsL75–77

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

  1. L75
    exact he
  2. L76
    exact heq
  3. L77
    exact hext_witness_witness_right

Library-wide reading audit

Original exact command ledger · 77 lines
  1. 0001intro V
  2. 0002intro L
  3. 0003intro r
  4. 0004intro s
  5. 0005intro hm
  6. 0006cases hm
  7. 0007have hcoords : exists d e. (((L=V*d+e) /\ (exists pvs_gap_dpi_append_remainder. pvs_gap_dpi_append_remainder + S (e) = (V))))
  8. 0008specialize division_remainder_exists (V)
  9. 0009specialize division_remainder_exists (L)
  10. 0010apply division_remainder_exists
  11. 0011exact hm_left
  12. 0012cases hcoords
  13. 0013cases hcoords_witness
  14. 0014cases hcoords_witness_witness
  15. 0015have hext : exists t u. (((((exists ff_h_pvs_dpi_append_last. ff_h_pvs_dpi_append_last + S (x*x1) = S ((S (L)) * u)) /\ exists ff_q_pvs_dpi_append_last. t = ff_q_pvs_dpi_append_last * S ((S (L)) * u) + (x*x1))) /\ (forall pfp_i_pvs_dpi_append_preserve pfp_a_pvs_dpi_append_preserve. (exists pfp_gap_pvs_dpi_append_preservebound. pfp_gap_pvs_dpi_append_preservebound + S (pfp_i_pvs_dpi_append_preserve) = (L)) -> (((exists ff_h_pfp_pvs_dpi_append_preserveold. ff_h_pfp_pvs_dpi_append_preserveold + S (pfp_a_pvs_dpi_append_preserve) = S ((S (pfp_i_pvs_dpi_append_preserve)) * s)) /\ exists ff_q_pfp_pvs_dpi_append_preserveold. r = ff_q_pfp_pvs_dpi_append_preserveold * S ((S (pfp_i_pvs_dpi_append_preserve)) * s) + (pfp_a_pvs_dpi_append_preserve))) -> (((exists ff_h_pfp_pvs_dpi_append_preservenew. ff_h_pfp_pvs_dpi_append_preservenew + S (pfp_a_pvs_dpi_append_preserve) = S ((S (pfp_i_pvs_dpi_append_preserve)) * u)) /\ exists ff_q_pfp_pvs_dpi_append_preservenew. t = ff_q_pfp_pvs_dpi_append_preservenew * S ((S (pfp_i_pvs_dpi_append_preserve)) * u) + (pfp_a_pvs_dpi_append_preserve))))))
  16. 0016specialize beta_prefix_extend (L)
  17. 0017specialize beta_prefix_extend (r)
  18. 0018specialize beta_prefix_extend (s)
  19. 0019specialize beta_prefix_extend (x*x1)
  20. 0020apply beta_prefix_extend
  21. 0021cases hext
  22. 0022cases hext_witness
  23. 0023cases hext_witness_witness
  24. 0024exists x2
  25. 0025exists x3
  26. 0026split
  27. 0027split
  28. 0028exact hm_left
  29. 0029intro i
  30. 0030intro d
  31. 0031intro e
  32. 0032intro hi
  33. 0033intro he
  34. 0034intro heq
  35. 0035have hcase : i=L \/ (exists pvs_gap_dpi_append_cases. pvs_gap_dpi_append_cases + S (i) = (L))
  36. 0036specialize finite_lt_succ_eq_or_lt (L)
  37. 0037specialize finite_lt_succ_eq_or_lt (i)
  38. 0038apply finite_lt_succ_eq_or_lt
  39. 0039exact hi
  40. 0040cases hcase
  41. 0041have hnew : L=V*d+e
  42. 0042trans i
  43. 0043symm
  44. 0044exact hcase_left
  45. 0045exact heq
  46. 0046have hsame : d=x /\ e=x1
  47. 0047specialize division_remainder_unique (V)
  48. 0048specialize division_remainder_unique (L)
  49. 0049specialize division_remainder_unique (d)
  50. 0050specialize division_remainder_unique (e)
  51. 0051specialize division_remainder_unique (x)
  52. 0052specialize division_remainder_unique (x1)
  53. 0053apply division_remainder_unique
  54. 0054exact hnew
  55. 0055exact he
  56. 0056exact hcoords_witness_witness_left
  57. 0057exact hcoords_witness_witness_right
  58. 0058cases hsame
  59. 0059rewrite hcase_left
  60. 0060rewrite hcase_left
  61. 0061rewrite hsame_left
  62. 0062rewrite hsame_left
  63. 0063rewrite hsame_right
  64. 0064rewrite hsame_right
  65. 0065exact hext_witness_witness_left
  66. 0066specialize hext_witness_witness_right (i)
  67. 0067specialize hext_witness_witness_right (d*e)
  68. 0068apply hext_witness_witness_right
  69. 0069exact hcase_right
  70. 0070specialize hm_right (i)
  71. 0071specialize hm_right (d)
  72. 0072specialize hm_right (e)
  73. 0073apply hm_right
  74. 0074exact hcase_right
  75. 0075exact he
  76. 0076exact heq
  77. 0077exact hext_witness_witness_right