FP0031

prime_field_negate_prefix_choice

Public research checkpoint, not admitted to Alpha or Stable. Alpha v30 remains 3222 checked-use theorems; Stable remains 432. The on-demand Alpha Lean service does not yet expose these checkpoint theorems; their independently checked literal bundles and unchanged sources are available below.

Public research checkpoint: original HA and independently compiled Lean verified; not Alpha-enrolled, no Alpha checked-use authority; not Stable

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

Exact expanded first-order arithmetic statement

forall p l. (forall i. (exists pfa_gap_negatechoice_domain. pfa_gap_negatechoice_domain + S (i) = (l)) -> exists v. (((exists pfa_gap_negatechoice_valueadditionleft. pfa_gap_negatechoice_valueadditionleft + S (i) = (p)) /\ (((exists pfa_gap_negatechoice_valueadditionright. pfa_gap_negatechoice_valueadditionright + S (v) = (p)) /\ ((((exists pfa_gap_negatechoice_valueadditionresultbound. pfa_gap_negatechoice_valueadditionresultbound + S (0) = (p)) /\ ((exists pfa_offset_left_negatechoice_valueadditionresultcongruence pfa_offset_right_negatechoice_valueadditionresultcongruence. ((i) + (v)) + (p) * pfa_offset_left_negatechoice_valueadditionresultcongruence = (0) + (p) * pfa_offset_right_negatechoice_valueadditionresultcongruence)))))))))) -> (exists b c. (forall pft_index_negatechoice_result. (exists pfa_gap_negatechoice_resultprefix. pfa_gap_negatechoice_resultprefix + S (pft_index_negatechoice_result) = (l)) -> exists pft_value_negatechoice_result. (((((exists ff_h_pft_negatechoice_resultpointentry. ff_h_pft_negatechoice_resultpointentry + S (pft_value_negatechoice_result) = S ((S (pft_index_negatechoice_result)) * c)) /\ exists ff_q_pft_negatechoice_resultpointentry. b = ff_q_pft_negatechoice_resultpointentry * S ((S (pft_index_negatechoice_result)) * c) + (pft_value_negatechoice_result))) /\ ((((exists pfa_gap_negatechoice_resultpointvalueadditionleft. pfa_gap_negatechoice_resultpointvalueadditionleft + S (pft_index_negatechoice_result) = (p)) /\ (((exists pfa_gap_negatechoice_resultpointvalueadditionright. pfa_gap_negatechoice_resultpointvalueadditionright + S (pft_value_negatechoice_result) = (p)) /\ ((((exists pfa_gap_negatechoice_resultpointvalueadditionresultbound. pfa_gap_negatechoice_resultpointvalueadditionresultbound + S (0) = (p)) /\ ((exists pfa_offset_left_negatechoice_resultpointvalueadditionresultcongruence pfa_offset_right_negatechoice_resultpointvalueadditionresultcongruence. ((pft_index_negatechoice_result) + (pft_value_negatechoice_result)) + (p) * pfa_offset_left_negatechoice_resultpointvalueadditionresultcongruence = (0) + (p) * pfa_offset_right_negatechoice_resultpointvalueadditionresultcongruence))))))))))))))

Constructive proof overview

Generated structural guide

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

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

Public research checkpoint: original HA and independently compiled Lean verified; not Alpha-enrolled, no Alpha checked-use authority; not Stable

Proof neighborhood

Direct dependencies

lt_not_le Alpha theorem; checked-use authorized zero_le Alpha theorem; checked-use authorized le_succ Alpha theorem; checked-use authorized zero_add Alpha theorem; checked-use authorized beta_prefix_extend Alpha theorem; checked-use authorized finite_lt_succ_eq_or_lt Alpha theorem; checked-use authorized

Direct dependents

FP0035 prime_field_negate_table_exists

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Local theorem links identify exact declared prerequisites. The literal dependency-closed bundle is checked by original HA and the independently compiled Lean verifier. Public delivery grants no Alpha checked-use authority or Stable membership.

Read the argument

Proof checkpoints

75 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. FpNegPrefix(p,b,c,l)Definitions: FpNegPrefix
  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. FpAdd(p,l,v,0)Definitions: FpAdd
  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_negatechoice_cases. pfa_gap_negatechoice_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–57

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
  4. L57
    rewrite hcases_left
21Construct an explicit witnessL58–58

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

  1. L58
    exists x2
22Separate the logical casesL59–59

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

  1. L59
    split
23Use earlier factsL60–61

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

  1. L60
    exact hext_witness_witness_left
  2. L61
    exact hv_witness
24Establish holdL62–65

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

  1. L62
    have hold : ∃ v. BetaAt(x,x1,i,v) ∧ FpAdd(p,i,v,0)Definitions: FpAddBetaAt
  2. L63
    specialize hprev_witness_witness (i)
  3. L64
    apply hprev_witness_witness
  4. L65
    exact hcases_right
25Separate the logical casesL66–67

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

  1. L66
    cases hold
  2. L67
    cases hold_witness
26Construct an explicit witnessL68–68

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

  1. L68
    exists x5
27Separate the logical casesL69–69

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

  1. L69
    split
28Use earlier factsL70–75

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

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

Library-wide reading audit

Original exact command ledger · 75 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_negatechoice_previous. (exists pfa_gap_negatechoice_previousprefix. pfa_gap_negatechoice_previousprefix + S (pft_index_negatechoice_previous) = (l)) -> exists pft_value_negatechoice_previous. (((((exists ff_h_pft_negatechoice_previouspointentry. ff_h_pft_negatechoice_previouspointentry + S (pft_value_negatechoice_previous) = S ((S (pft_index_negatechoice_previous)) * c)) /\ exists ff_q_pft_negatechoice_previouspointentry. b = ff_q_pft_negatechoice_previouspointentry * S ((S (pft_index_negatechoice_previous)) * c) + (pft_value_negatechoice_previous))) /\ ((((exists pfa_gap_negatechoice_previouspointvalueadditionleft. pfa_gap_negatechoice_previouspointvalueadditionleft + S (pft_index_negatechoice_previous) = (p)) /\ (((exists pfa_gap_negatechoice_previouspointvalueadditionright. pfa_gap_negatechoice_previouspointvalueadditionright + S (pft_value_negatechoice_previous) = (p)) /\ ((((exists pfa_gap_negatechoice_previouspointvalueadditionresultbound. pfa_gap_negatechoice_previouspointvalueadditionresultbound + S (0) = (p)) /\ ((exists pfa_offset_left_negatechoice_previouspointvalueadditionresultcongruence pfa_offset_right_negatechoice_previouspointvalueadditionresultcongruence. ((pft_index_negatechoice_previous) + (pft_value_negatechoice_previous)) + (p) * pfa_offset_left_negatechoice_previouspointvalueadditionresultcongruence = (0) + (p) * pfa_offset_right_negatechoice_previouspointvalueadditionresultcongruence)))))))))))))
  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 pfa_gap_negatechoice_last_valueadditionleft. pfa_gap_negatechoice_last_valueadditionleft + S (l) = (p)) /\ (((exists pfa_gap_negatechoice_last_valueadditionright. pfa_gap_negatechoice_last_valueadditionright + S (v) = (p)) /\ ((((exists pfa_gap_negatechoice_last_valueadditionresultbound. pfa_gap_negatechoice_last_valueadditionresultbound + S (0) = (p)) /\ ((exists pfa_offset_left_negatechoice_last_valueadditionresultcongruence pfa_offset_right_negatechoice_last_valueadditionresultcongruence. ((l) + (v)) + (p) * pfa_offset_left_negatechoice_last_valueadditionresultcongruence = (0) + (p) * pfa_offset_right_negatechoice_last_valueadditionresultcongruence)))))))))
  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_negatechoice_last_entry. ff_h_pft_negatechoice_last_entry + S (x2) = S ((S (l)) * c)) /\ exists ff_q_pft_negatechoice_last_entry. b = ff_q_pft_negatechoice_last_entry * S ((S (l)) * c) + (x2))) /\ (forall i v. (exists pfa_gap_negatechoice_preserve_bound. pfa_gap_negatechoice_preserve_bound + S (i) = (l)) -> (((exists ff_h_pft_negatechoice_old. ff_h_pft_negatechoice_old + S (v) = S ((S (i)) * x1)) /\ exists ff_q_pft_negatechoice_old. x = ff_q_pft_negatechoice_old * S ((S (i)) * x1) + (v))) -> (((exists ff_h_pft_negatechoice_new. ff_h_pft_negatechoice_new + S (v) = S ((S (i)) * c)) /\ exists ff_q_pft_negatechoice_new. b = ff_q_pft_negatechoice_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_negatechoice_cases. pfa_gap_negatechoice_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. 0057rewrite hcases_left
  58. 0058exists x2
  59. 0059split
  60. 0060exact hext_witness_witness_left
  61. 0061exact hv_witness
  62. 0062have hold : exists v. (((((exists ff_h_pft_negatechoice_old_entryentry. ff_h_pft_negatechoice_old_entryentry + S (v) = S ((S (i)) * x1)) /\ exists ff_q_pft_negatechoice_old_entryentry. x = ff_q_pft_negatechoice_old_entryentry * S ((S (i)) * x1) + (v))) /\ ((((exists pfa_gap_negatechoice_old_entryvalueadditionleft. pfa_gap_negatechoice_old_entryvalueadditionleft + S (i) = (p)) /\ (((exists pfa_gap_negatechoice_old_entryvalueadditionright. pfa_gap_negatechoice_old_entryvalueadditionright + S (v) = (p)) /\ ((((exists pfa_gap_negatechoice_old_entryvalueadditionresultbound. pfa_gap_negatechoice_old_entryvalueadditionresultbound + S (0) = (p)) /\ ((exists pfa_offset_left_negatechoice_old_entryvalueadditionresultcongruence pfa_offset_right_negatechoice_old_entryvalueadditionresultcongruence. ((i) + (v)) + (p) * pfa_offset_left_negatechoice_old_entryvalueadditionresultcongruence = (0) + (p) * pfa_offset_right_negatechoice_old_entryvalueadditionresultcongruence))))))))))))
  63. 0063specialize hprev_witness_witness (i)
  64. 0064apply hprev_witness_witness
  65. 0065exact hcases_right
  66. 0066cases hold
  67. 0067cases hold_witness
  68. 0068exists x5
  69. 0069split
  70. 0070specialize hext_witness_witness_right (i)
  71. 0071specialize hext_witness_witness_right (x5)
  72. 0072apply hext_witness_witness_right
  73. 0073exact hcases_right
  74. 0074exact hold_witness_left
  75. 0075exact hold_witness_right