FP0031

prime_field_negate_prefix_choice

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

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

Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved.

This checkpoint constructs prime-order fields (k=1), with genuine finite arithmetic tables, cardinality, and characteristic. Inversion is proved only for nonzero elements; the table's zero entry is a zero-to-zero convention. G091 for every prime power p^k, with an irreducible polynomial of degree k, remains open. No extension-field construction or G091 closure is claimed.

Exact theorem in conservative defined notation

∀ p. ∀ l. (∀ x. Lt(x,l) → ∃ y. FpAdd(p,x,y,0)) → ∃ x. ∃ y. FpNegPrefix(p,x,y,l)

Every linked abbreviation expands hygienically to the identical original native formula.

Definition DAG

FpAdd(p,a,b,c) · 3FpNegPrefix(p,b,c,l) · 2Lt(a,b) · 3BetaAt(b,c,i,x) · 4

Actual proof prerequisites

lt_not_le · checked external prerequisitezero_le · checked external prerequisitele_succ · checked external prerequisitezero_add · checked external prerequisitebeta_prefix_extend · checked external prerequisitefinite_lt_succ_eq_or_lt · checked external prerequisite
Original expanded first-order 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))))))))))))))

Complete tactic proof in conservative notation

All 75 original proof lines are preserved. Only local proposition formulas are abbreviated; every abbreviation has an exact binder-safe expansion check. The linked exact edition contains the unchanged replay script.

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.

Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.

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(p,b,c,l)Original native command in the exact edition
  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(p,l,v,0)Original native command in the exact edition
  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: BetaAt(b,c,l,x2)Lt(y,l)BetaAt(x,x1,y,z)BetaAt(b,c,y,z)Original native command in the exact edition
  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 ∨ Lt(i,l)Definitions: Lt(i,l)Original native command in the exact edition
  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: BetaAt(x,x1,i,v)FpAdd(p,i,v,0)Original native command in the exact edition
  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 defined 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 : ∃ b. ∃ c. FpNegPrefix(p,b,c,l)
  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 : ∃ v. FpAdd(p,l,v,0)
  30. 0030specialize htotal (l)
  31. 0031apply htotal
  32. 0032exists 0
  33. 0033apply zero_add
  34. 0034cases hv
  35. 0035have hext : ∃ b. ∃ c. BetaAt(b,c,l,x2) ∧ (∀ y. ∀ z. Lt(y,l) → BetaAt(x,x1,y,z) → BetaAt(b,c,y,z))
  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 ∨ Lt(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 : ∃ v. BetaAt(x,x1,i,v) ∧ FpAdd(p,i,v,0)
  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