MX0015

divisor_pair_index_map_exists

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

Finite HA induction constructs a native-beta pair-product map for every positive width and finite window, including the empty window.

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. ~(V=0) -> exists r s. (((~((V)=0)) /\ (forall dpi_index_dpi_exists_result dpi_row_dpi_exists_result dpi_column_dpi_exists_result. (exists pvs_gap_dpi_exists_resultwindow. pvs_gap_dpi_exists_resultwindow + S (dpi_index_dpi_exists_result) = (L)) -> (exists pvs_gap_dpi_exists_resultremainder. pvs_gap_dpi_exists_resultremainder + S (dpi_column_dpi_exists_result) = (V)) -> (dpi_index_dpi_exists_result)=(V)*(dpi_row_dpi_exists_result)+(dpi_column_dpi_exists_result) -> (((exists ff_h_pvs_dpi_exists_resultvalue. ff_h_pvs_dpi_exists_resultvalue + S ((dpi_row_dpi_exists_result)*(dpi_column_dpi_exists_result)) = S ((S (dpi_index_dpi_exists_result)) * s)) /\ exists ff_q_pvs_dpi_exists_resultvalue. r = ff_q_pvs_dpi_exists_resultvalue * S ((S (dpi_index_dpi_exists_result)) * s) + ((dpi_row_dpi_exists_result)*(dpi_column_dpi_exists_result)))))))

Constructive proof overview

Generated structural guide

Finite HA induction constructs a native-beta pair-product map for every positive width and finite window, including the empty window.

The unchanged tactic script uses 2 declared prerequisites and contains 37 exact native proof lines.

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

Proof neighborhood

Direct dependencies

factor_permutation_below_zero_impossible Alpha theorem; checked-use authorized MX0014 divisor_pair_index_map_append

Direct dependents

MX0056 dirichlet_coprime_product_data_construct

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

37 script commands · 15 reading checkpoints · 2 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)
divisor pair index map append

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–2

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

  1. L1
    intro V
  2. L2
    intro L
02Induction on LL3–4

Split the argument into the base and successor obligations. The induction hypothesis is available only in the successor branch.

  1. L3
    induction L
  2. L4
    intro hV
03Construct an explicit witnessL5–6

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

  1. L5
    exists 0
  2. L6
    exists 0
04Separate the logical casesL7–7

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

  1. L7
    split
05Use earlier factsL8–8

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

  1. L8
    exact hV
06Fix variables and assumptionsL9–14

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

  1. L9
    intro i
  2. L10
    intro d
  3. L11
    intro e
  4. L12
    intro hi
  5. L13
    intro he
  6. L14
    intro heq
07Separate the logical casesL15–15

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

  1. L15
    exfalso
08Use earlier factsL16–18

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

  1. L16
    specialize factor_permutation_below_zero_impossible (i)
  2. L17
    apply factor_permutation_below_zero_impossible
  3. L18
    exact hi
09Fix variables and assumptionsL19–19

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

  1. L19
    intro hV
10Establish hpL20–22

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

  1. L20
    have hp : ∃ r. ∃ s. DivisorPairIndexMap(V,L,r,s)Definitions: DivisorPairIndexMap
  2. L21
    apply IH
  3. L22
    exact hV
11Separate the logical casesL23–24

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

  1. L23
    cases hp
  2. L24
    cases hp_witness
12Establish heL25–31

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply divisor pair index map append.

  1. L25
    have he : ∃ t. ∃ u. DivisorPairIndexMap(V,S L,t,u) ∧ (∀ y. ∀ z. Lt(y,L) → BetaAt(x,x1,y,z) → BetaAt(t,u,y,z))Definitions: DivisorPairIndexMapLtBetaAt
  2. L26
    specialize divisor_pair_index_map_append (V)
  3. L27
    specialize divisor_pair_index_map_append (L)
  4. L28
    specialize divisor_pair_index_map_append (x)
  5. L29
    specialize divisor_pair_index_map_append (x1)
  6. L30
    apply divisor_pair_index_map_append
  7. L31
    exact hp_witness_witness
13Separate the logical casesL32–34

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

  1. L32
    cases he
  2. L33
    cases he_witness
  3. L34
    cases he_witness_witness
14Construct an explicit witnessL35–36

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

  1. L35
    exists x2
  2. L36
    exists x3
15Use earlier factsL37–37

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

  1. L37
    exact he_witness_witness_left

Library-wide reading audit

Original exact command ledger · 37 lines
  1. 0001intro V
  2. 0002intro L
  3. 0003induction L
  4. 0004intro hV
  5. 0005exists 0
  6. 0006exists 0
  7. 0007split
  8. 0008exact hV
  9. 0009intro i
  10. 0010intro d
  11. 0011intro e
  12. 0012intro hi
  13. 0013intro he
  14. 0014intro heq
  15. 0015exfalso
  16. 0016specialize factor_permutation_below_zero_impossible (i)
  17. 0017apply factor_permutation_below_zero_impossible
  18. 0018exact hi
  19. 0019intro hV
  20. 0020have hp : exists r s. (((~((V)=0)) /\ (forall dpi_index_dpi_previous dpi_row_dpi_previous dpi_column_dpi_previous. (exists pvs_gap_dpi_previouswindow. pvs_gap_dpi_previouswindow + S (dpi_index_dpi_previous) = (L)) -> (exists pvs_gap_dpi_previousremainder. pvs_gap_dpi_previousremainder + S (dpi_column_dpi_previous) = (V)) -> (dpi_index_dpi_previous)=(V)*(dpi_row_dpi_previous)+(dpi_column_dpi_previous) -> (((exists ff_h_pvs_dpi_previousvalue. ff_h_pvs_dpi_previousvalue + S ((dpi_row_dpi_previous)*(dpi_column_dpi_previous)) = S ((S (dpi_index_dpi_previous)) * s)) /\ exists ff_q_pvs_dpi_previousvalue. r = ff_q_pvs_dpi_previousvalue * S ((S (dpi_index_dpi_previous)) * s) + ((dpi_row_dpi_previous)*(dpi_column_dpi_previous)))))))
  21. 0021apply IH
  22. 0022exact hV
  23. 0023cases hp
  24. 0024cases hp_witness
  25. 0025have he : exists t u. (((((~((V)=0)) /\ (forall dpi_index_dpi_next dpi_row_dpi_next dpi_column_dpi_next. (exists pvs_gap_dpi_nextwindow. pvs_gap_dpi_nextwindow + S (dpi_index_dpi_next) = (S L)) -> (exists pvs_gap_dpi_nextremainder. pvs_gap_dpi_nextremainder + S (dpi_column_dpi_next) = (V)) -> (dpi_index_dpi_next)=(V)*(dpi_row_dpi_next)+(dpi_column_dpi_next) -> (((exists ff_h_pvs_dpi_nextvalue. ff_h_pvs_dpi_nextvalue + S ((dpi_row_dpi_next)*(dpi_column_dpi_next)) = S ((S (dpi_index_dpi_next)) * u)) /\ exists ff_q_pvs_dpi_nextvalue. t = ff_q_pvs_dpi_nextvalue * S ((S (dpi_index_dpi_next)) * u) + ((dpi_row_dpi_next)*(dpi_column_dpi_next))))))) /\ (forall pfp_i_pvs_dpi_next_preserve pfp_a_pvs_dpi_next_preserve. (exists pfp_gap_pvs_dpi_next_preservebound. pfp_gap_pvs_dpi_next_preservebound + S (pfp_i_pvs_dpi_next_preserve) = (L)) -> (((exists ff_h_pfp_pvs_dpi_next_preserveold. ff_h_pfp_pvs_dpi_next_preserveold + S (pfp_a_pvs_dpi_next_preserve) = S ((S (pfp_i_pvs_dpi_next_preserve)) * x1)) /\ exists ff_q_pfp_pvs_dpi_next_preserveold. x = ff_q_pfp_pvs_dpi_next_preserveold * S ((S (pfp_i_pvs_dpi_next_preserve)) * x1) + (pfp_a_pvs_dpi_next_preserve))) -> (((exists ff_h_pfp_pvs_dpi_next_preservenew. ff_h_pfp_pvs_dpi_next_preservenew + S (pfp_a_pvs_dpi_next_preserve) = S ((S (pfp_i_pvs_dpi_next_preserve)) * u)) /\ exists ff_q_pfp_pvs_dpi_next_preservenew. t = ff_q_pfp_pvs_dpi_next_preservenew * S ((S (pfp_i_pvs_dpi_next_preserve)) * u) + (pfp_a_pvs_dpi_next_preserve))))))
  26. 0026specialize divisor_pair_index_map_append (V)
  27. 0027specialize divisor_pair_index_map_append (L)
  28. 0028specialize divisor_pair_index_map_append (x)
  29. 0029specialize divisor_pair_index_map_append (x1)
  30. 0030apply divisor_pair_index_map_append
  31. 0031exact hp_witness_witness
  32. 0032cases he
  33. 0033cases he_witness
  34. 0034cases he_witness_witness
  35. 0035exists x2
  36. 0036exists x3
  37. 0037exact he_witness_witness_left