FP002F

prime_field_add_prefix_choice

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

Ordinary finite induction codes actual pointwise add witnesses; no choice axiom or unproved field law is introduced.

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 p l. (forall i. (exists pfa_gap_addchoice_domain. pfa_gap_addchoice_domain + S (i) = (l)) -> exists v. (exists pft_row_addchoice_value pft_column_addchoice_value. (((i) = pft_row_addchoice_value * (p) + pft_column_addchoice_value) /\ ((((exists pfa_gap_addchoice_valueoperationleft. pfa_gap_addchoice_valueoperationleft + S (pft_row_addchoice_value) = (p)) /\ (((exists pfa_gap_addchoice_valueoperationright. pfa_gap_addchoice_valueoperationright + S (pft_column_addchoice_value) = (p)) /\ ((((exists pfa_gap_addchoice_valueoperationresultbound. pfa_gap_addchoice_valueoperationresultbound + S (v) = (p)) /\ ((exists pfa_offset_left_addchoice_valueoperationresultcongruence pfa_offset_right_addchoice_valueoperationresultcongruence. ((pft_row_addchoice_value) + (pft_column_addchoice_value)) + (p) * pfa_offset_left_addchoice_valueoperationresultcongruence = (v) + (p) * pfa_offset_right_addchoice_valueoperationresultcongruence))))))))))))) -> (exists b c. (forall pft_index_addchoice_result. (exists pfa_gap_addchoice_resultprefix. pfa_gap_addchoice_resultprefix + S (pft_index_addchoice_result) = (l)) -> exists pft_value_addchoice_result. (((((exists ff_h_pft_addchoice_resultpointentry. ff_h_pft_addchoice_resultpointentry + S (pft_value_addchoice_result) = S ((S (pft_index_addchoice_result)) * c)) /\ exists ff_q_pft_addchoice_resultpointentry. b = ff_q_pft_addchoice_resultpointentry * S ((S (pft_index_addchoice_result)) * c) + (pft_value_addchoice_result))) /\ ((exists pft_row_addchoice_resultpointvalue pft_column_addchoice_resultpointvalue. (((pft_index_addchoice_result) = pft_row_addchoice_resultpointvalue * (p) + pft_column_addchoice_resultpointvalue) /\ ((((exists pfa_gap_addchoice_resultpointvalueoperationleft. pfa_gap_addchoice_resultpointvalueoperationleft + S (pft_row_addchoice_resultpointvalue) = (p)) /\ (((exists pfa_gap_addchoice_resultpointvalueoperationright. pfa_gap_addchoice_resultpointvalueoperationright + S (pft_column_addchoice_resultpointvalue) = (p)) /\ ((((exists pfa_gap_addchoice_resultpointvalueoperationresultbound. pfa_gap_addchoice_resultpointvalueoperationresultbound + S (pft_value_addchoice_result) = (p)) /\ ((exists pfa_offset_left_addchoice_resultpointvalueoperationresultcongruence pfa_offset_right_addchoice_resultpointvalueoperationresultcongruence. ((pft_row_addchoice_resultpointvalue) + (pft_column_addchoice_resultpointvalue)) + (p) * pfa_offset_left_addchoice_resultpointvalueoperationresultcongruence = (pft_value_addchoice_result) + (p) * pfa_offset_right_addchoice_resultpointvalueoperationresultcongruence)))))))))))))))))

Constructive proof overview

Generated structural guide

Ordinary finite induction codes actual pointwise add witnesses; no choice axiom or unproved field law is introduced.

The unchanged tactic script uses 6 declared prerequisites and contains 74 exact native proof lines.

Alpha v34 checked-use · first admitted v31 · 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 le_succ Stable theorem; checked-use authorized zero_add Stable theorem; checked-use authorized beta_prefix_extend Stable theorem; checked-use authorized finite_lt_succ_eq_or_lt Stable theorem; checked-use authorized

Direct dependents

FP0033 prime_field_add_table_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

74 script commands · 28 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–2

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

  1. L1
    intro p
  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 htotal
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
04Fix variables and assumptionsL7–8

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

  1. L7
    intro i
  2. L8
    intro hi
05Separate the logical casesL9–9

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

  1. L9
    exfalso
06Use earlier factsL10–15

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

  1. L10
    specialize lt_not_le (i)
  2. L11
    specialize lt_not_le (0)
  3. L12
    apply lt_not_le
  4. L13
    exact hi
  5. L14
    specialize zero_le (i)
  6. L15
    apply zero_le
07Fix variables and assumptionsL16–16

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

  1. L16
    intro htotal
08Establish hprevL17–26

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

  1. L17
    have hprev : ∃ b. ∃ c. FpAddPrefix(p,b,c,l)Definitions: FpAddPrefix
  2. L18
    apply IH
  3. L19
    intro i
  4. L20
    intro hi
  5. L21
    specialize htotal (i)
  6. L22
    apply htotal
  7. L23
    specialize le_succ (S i)
  8. L24
    specialize le_succ (l)
  9. L25
    apply le_succ
  10. L26
    exact hi
09Separate the logical casesL27–28

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

  1. L27
    cases hprev
  2. L28
    cases hprev_witness
10Establish hvL29–31

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

  1. L29
    have hv : ∃ v. FpAddGridValue(p,l,v)Definitions: FpAddGridValue
  2. L30
    specialize htotal (l)
  3. L31
    apply htotal
11Construct an explicit witnessL32–32

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

  1. L32
    exists 0
12Use earlier factsL33–33

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

  1. L33
    apply zero_add
13Separate the logical casesL34–34

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

  1. L34
    cases hv
14Establish hextL35–40

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

  1. L35
    have hext : ∃ b. ∃ c. BetaAt(b,c,l,x2) ∧ (∀ y. ∀ z. Lt(y,l) → BetaAt(x,x1,y,z) → BetaAt(b,c,y,z))Definitions: LtBetaAt
  2. L36
    specialize beta_prefix_extend (l)
  3. L37
    specialize beta_prefix_extend (x)
  4. L38
    specialize beta_prefix_extend (x1)
  5. L39
    specialize beta_prefix_extend (x2)
  6. L40
    apply beta_prefix_extend
15Separate the logical casesL41–43

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

  1. L41
    cases hext
  2. L42
    cases hext_witness
  3. L43
    cases hext_witness_witness
16Construct an explicit witnessL44–45

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

  1. L44
    exists x3
  2. L45
    exists x4
17Fix variables and assumptionsL46–47

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

  1. L46
    intro i
  2. L47
    intro hi
18Establish hcasesL48–52

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. L48
    have hcases : i = l \/ (exists pfa_gap_addchoice_cases. pfa_gap_addchoice_cases + S (i) = (l))
  2. L49
    specialize finite_lt_succ_eq_or_lt (l)
  3. L50
    specialize finite_lt_succ_eq_or_lt (i)
  4. L51
    apply finite_lt_succ_eq_or_lt
  5. L52
    exact hi
19Separate the logical casesL53–53

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

  1. L53
    cases hcases
20Calculate and transport equalitiesL54–56

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

  1. L54
    rewrite hcases_left
  2. L55
    rewrite hcases_left
  3. L56
    rewrite hcases_left
21Construct an explicit witnessL57–57

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

  1. L57
    exists x2
22Separate the logical casesL58–58

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

  1. L58
    split
23Use earlier factsL59–60

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

  1. L59
    exact hext_witness_witness_left
  2. L60
    exact hv_witness
24Establish holdL61–64

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

  1. L61
    have hold : ∃ v. BetaAt(x,x1,i,v) ∧ FpAddGridValue(p,i,v)Definitions: FpAddGridValueBetaAt
  2. L62
    specialize hprev_witness_witness (i)
  3. L63
    apply hprev_witness_witness
  4. L64
    exact hcases_right
25Separate the logical casesL65–66

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

  1. L65
    cases hold
  2. L66
    cases hold_witness
26Construct an explicit witnessL67–67

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

  1. L67
    exists x5
27Separate the logical casesL68–68

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

  1. L68
    split
28Use earlier factsL69–74

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

  1. L69
    specialize hext_witness_witness_right (i)
  2. L70
    specialize hext_witness_witness_right (x5)
  3. L71
    apply hext_witness_witness_right
  4. L72
    exact hcases_right
  5. L73
    exact hold_witness_left
  6. L74
    exact hold_witness_right

Library-wide reading audit

Original exact command ledger · 74 lines
  1. 0001intro p
  2. 0002intro l
  3. 0003induction l
  4. 0004intro htotal
  5. 0005exists 0
  6. 0006exists 0
  7. 0007intro i
  8. 0008intro hi
  9. 0009exfalso
  10. 0010specialize lt_not_le (i)
  11. 0011specialize lt_not_le (0)
  12. 0012apply lt_not_le
  13. 0013exact hi
  14. 0014specialize zero_le (i)
  15. 0015apply zero_le
  16. 0016intro htotal
  17. 0017have hprev : exists b c. (forall pft_index_addchoice_previous. (exists pfa_gap_addchoice_previousprefix. pfa_gap_addchoice_previousprefix + S (pft_index_addchoice_previous) = (l)) -> exists pft_value_addchoice_previous. (((((exists ff_h_pft_addchoice_previouspointentry. ff_h_pft_addchoice_previouspointentry + S (pft_value_addchoice_previous) = S ((S (pft_index_addchoice_previous)) * c)) /\ exists ff_q_pft_addchoice_previouspointentry. b = ff_q_pft_addchoice_previouspointentry * S ((S (pft_index_addchoice_previous)) * c) + (pft_value_addchoice_previous))) /\ ((exists pft_row_addchoice_previouspointvalue pft_column_addchoice_previouspointvalue. (((pft_index_addchoice_previous) = pft_row_addchoice_previouspointvalue * (p) + pft_column_addchoice_previouspointvalue) /\ ((((exists pfa_gap_addchoice_previouspointvalueoperationleft. pfa_gap_addchoice_previouspointvalueoperationleft + S (pft_row_addchoice_previouspointvalue) = (p)) /\ (((exists pfa_gap_addchoice_previouspointvalueoperationright. pfa_gap_addchoice_previouspointvalueoperationright + S (pft_column_addchoice_previouspointvalue) = (p)) /\ ((((exists pfa_gap_addchoice_previouspointvalueoperationresultbound. pfa_gap_addchoice_previouspointvalueoperationresultbound + S (pft_value_addchoice_previous) = (p)) /\ ((exists pfa_offset_left_addchoice_previouspointvalueoperationresultcongruence pfa_offset_right_addchoice_previouspointvalueoperationresultcongruence. ((pft_row_addchoice_previouspointvalue) + (pft_column_addchoice_previouspointvalue)) + (p) * pfa_offset_left_addchoice_previouspointvalueoperationresultcongruence = (pft_value_addchoice_previous) + (p) * pfa_offset_right_addchoice_previouspointvalueoperationresultcongruence))))))))))))))))
  18. 0018apply IH
  19. 0019intro i
  20. 0020intro hi
  21. 0021specialize htotal (i)
  22. 0022apply htotal
  23. 0023specialize le_succ (S i)
  24. 0024specialize le_succ (l)
  25. 0025apply le_succ
  26. 0026exact hi
  27. 0027cases hprev
  28. 0028cases hprev_witness
  29. 0029have hv : exists v. (exists pft_row_addchoice_last_value pft_column_addchoice_last_value. (((l) = pft_row_addchoice_last_value * (p) + pft_column_addchoice_last_value) /\ ((((exists pfa_gap_addchoice_last_valueoperationleft. pfa_gap_addchoice_last_valueoperationleft + S (pft_row_addchoice_last_value) = (p)) /\ (((exists pfa_gap_addchoice_last_valueoperationright. pfa_gap_addchoice_last_valueoperationright + S (pft_column_addchoice_last_value) = (p)) /\ ((((exists pfa_gap_addchoice_last_valueoperationresultbound. pfa_gap_addchoice_last_valueoperationresultbound + S (v) = (p)) /\ ((exists pfa_offset_left_addchoice_last_valueoperationresultcongruence pfa_offset_right_addchoice_last_valueoperationresultcongruence. ((pft_row_addchoice_last_value) + (pft_column_addchoice_last_value)) + (p) * pfa_offset_left_addchoice_last_valueoperationresultcongruence = (v) + (p) * pfa_offset_right_addchoice_last_valueoperationresultcongruence))))))))))))
  30. 0030specialize htotal (l)
  31. 0031apply htotal
  32. 0032exists 0
  33. 0033apply zero_add
  34. 0034cases hv
  35. 0035have hext : exists b c. (((exists ff_h_pft_addchoice_last_entry. ff_h_pft_addchoice_last_entry + S (x2) = S ((S (l)) * c)) /\ exists ff_q_pft_addchoice_last_entry. b = ff_q_pft_addchoice_last_entry * S ((S (l)) * c) + (x2))) /\ (forall i v. (exists pfa_gap_addchoice_preserve_bound. pfa_gap_addchoice_preserve_bound + S (i) = (l)) -> (((exists ff_h_pft_addchoice_old. ff_h_pft_addchoice_old + S (v) = S ((S (i)) * x1)) /\ exists ff_q_pft_addchoice_old. x = ff_q_pft_addchoice_old * S ((S (i)) * x1) + (v))) -> (((exists ff_h_pft_addchoice_new. ff_h_pft_addchoice_new + S (v) = S ((S (i)) * c)) /\ exists ff_q_pft_addchoice_new. b = ff_q_pft_addchoice_new * S ((S (i)) * c) + (v))))
  36. 0036specialize beta_prefix_extend (l)
  37. 0037specialize beta_prefix_extend (x)
  38. 0038specialize beta_prefix_extend (x1)
  39. 0039specialize beta_prefix_extend (x2)
  40. 0040apply beta_prefix_extend
  41. 0041cases hext
  42. 0042cases hext_witness
  43. 0043cases hext_witness_witness
  44. 0044exists x3
  45. 0045exists x4
  46. 0046intro i
  47. 0047intro hi
  48. 0048have hcases : i = l \/ (exists pfa_gap_addchoice_cases. pfa_gap_addchoice_cases + S (i) = (l))
  49. 0049specialize finite_lt_succ_eq_or_lt (l)
  50. 0050specialize finite_lt_succ_eq_or_lt (i)
  51. 0051apply finite_lt_succ_eq_or_lt
  52. 0052exact hi
  53. 0053cases hcases
  54. 0054rewrite hcases_left
  55. 0055rewrite hcases_left
  56. 0056rewrite hcases_left
  57. 0057exists x2
  58. 0058split
  59. 0059exact hext_witness_witness_left
  60. 0060exact hv_witness
  61. 0061have hold : exists v. (((((exists ff_h_pft_addchoice_old_entryentry. ff_h_pft_addchoice_old_entryentry + S (v) = S ((S (i)) * x1)) /\ exists ff_q_pft_addchoice_old_entryentry. x = ff_q_pft_addchoice_old_entryentry * S ((S (i)) * x1) + (v))) /\ ((exists pft_row_addchoice_old_entryvalue pft_column_addchoice_old_entryvalue. (((i) = pft_row_addchoice_old_entryvalue * (p) + pft_column_addchoice_old_entryvalue) /\ ((((exists pfa_gap_addchoice_old_entryvalueoperationleft. pfa_gap_addchoice_old_entryvalueoperationleft + S (pft_row_addchoice_old_entryvalue) = (p)) /\ (((exists pfa_gap_addchoice_old_entryvalueoperationright. pfa_gap_addchoice_old_entryvalueoperationright + S (pft_column_addchoice_old_entryvalue) = (p)) /\ ((((exists pfa_gap_addchoice_old_entryvalueoperationresultbound. pfa_gap_addchoice_old_entryvalueoperationresultbound + S (v) = (p)) /\ ((exists pfa_offset_left_addchoice_old_entryvalueoperationresultcongruence pfa_offset_right_addchoice_old_entryvalueoperationresultcongruence. ((pft_row_addchoice_old_entryvalue) + (pft_column_addchoice_old_entryvalue)) + (p) * pfa_offset_left_addchoice_old_entryvalueoperationresultcongruence = (v) + (p) * pfa_offset_right_addchoice_old_entryvalueoperationresultcongruence)))))))))))))))
  62. 0062specialize hprev_witness_witness (i)
  63. 0063apply hprev_witness_witness
  64. 0064exact hcases_right
  65. 0065cases hold
  66. 0066cases hold_witness
  67. 0067exists x5
  68. 0068split
  69. 0069specialize hext_witness_witness_right (i)
  70. 0070specialize hext_witness_witness_right (x5)
  71. 0071apply hext_witness_witness_right
  72. 0072exact hcases_right
  73. 0073exact hold_witness_left
  74. 0074exact hold_witness_right