FP0030

prime_field_multiply_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.

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

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

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. FpMulGridValue(p,x,y)) → ∃ x. ∃ y. FpMulPrefix(p,x,y,l)

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

Definition DAG

FpMulGridValue(p,i,v) · 3FpMulPrefix(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_multiplychoice_domain. pfa_gap_multiplychoice_domain + S (i) = (l)) -> exists v. (exists pft_row_multiplychoice_value pft_column_multiplychoice_value. (((i) = pft_row_multiplychoice_value * (p) + pft_column_multiplychoice_value) /\ ((((exists pfa_gap_multiplychoice_valueoperationleft. pfa_gap_multiplychoice_valueoperationleft + S (pft_row_multiplychoice_value) = (p)) /\ (((exists pfa_gap_multiplychoice_valueoperationright. pfa_gap_multiplychoice_valueoperationright + S (pft_column_multiplychoice_value) = (p)) /\ ((((exists pfa_gap_multiplychoice_valueoperationresultbound. pfa_gap_multiplychoice_valueoperationresultbound + S (v) = (p)) /\ ((exists pfa_offset_left_multiplychoice_valueoperationresultcongruence pfa_offset_right_multiplychoice_valueoperationresultcongruence. ((pft_row_multiplychoice_value) * (pft_column_multiplychoice_value)) + (p) * pfa_offset_left_multiplychoice_valueoperationresultcongruence = (v) + (p) * pfa_offset_right_multiplychoice_valueoperationresultcongruence))))))))))))) -> (exists b c. (forall pft_index_multiplychoice_result. (exists pfa_gap_multiplychoice_resultprefix. pfa_gap_multiplychoice_resultprefix + S (pft_index_multiplychoice_result) = (l)) -> exists pft_value_multiplychoice_result. (((((exists ff_h_pft_multiplychoice_resultpointentry. ff_h_pft_multiplychoice_resultpointentry + S (pft_value_multiplychoice_result) = S ((S (pft_index_multiplychoice_result)) * c)) /\ exists ff_q_pft_multiplychoice_resultpointentry. b = ff_q_pft_multiplychoice_resultpointentry * S ((S (pft_index_multiplychoice_result)) * c) + (pft_value_multiplychoice_result))) /\ ((exists pft_row_multiplychoice_resultpointvalue pft_column_multiplychoice_resultpointvalue. (((pft_index_multiplychoice_result) = pft_row_multiplychoice_resultpointvalue * (p) + pft_column_multiplychoice_resultpointvalue) /\ ((((exists pfa_gap_multiplychoice_resultpointvalueoperationleft. pfa_gap_multiplychoice_resultpointvalueoperationleft + S (pft_row_multiplychoice_resultpointvalue) = (p)) /\ (((exists pfa_gap_multiplychoice_resultpointvalueoperationright. pfa_gap_multiplychoice_resultpointvalueoperationright + S (pft_column_multiplychoice_resultpointvalue) = (p)) /\ ((((exists pfa_gap_multiplychoice_resultpointvalueoperationresultbound. pfa_gap_multiplychoice_resultpointvalueoperationresultbound + S (pft_value_multiplychoice_result) = (p)) /\ ((exists pfa_offset_left_multiplychoice_resultpointvalueoperationresultcongruence pfa_offset_right_multiplychoice_resultpointvalueoperationresultcongruence. ((pft_row_multiplychoice_resultpointvalue) * (pft_column_multiplychoice_resultpointvalue)) + (p) * pfa_offset_left_multiplychoice_resultpointvalueoperationresultcongruence = (pft_value_multiplychoice_result) + (p) * pfa_offset_right_multiplychoice_resultpointvalueoperationresultcongruence)))))))))))))))))

Complete tactic proof in conservative notation

All 74 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

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.

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. FpMulPrefix(p,b,c,l)Definitions: FpMulPrefix(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. FpMulGridValue(p,l,v)Definitions: FpMulGridValue(p,l,v)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–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) ∧ FpMulGridValue(p,i,v)Definitions: BetaAt(x,x1,i,v)FpMulGridValue(p,i,v)Original native command in the exact edition
  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 defined 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 : ∃ b. ∃ c. FpMulPrefix(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. FpMulGridValue(p,l,v)
  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. 0057exists x2
  58. 0058split
  59. 0059exact hext_witness_witness_left
  60. 0060exact hv_witness
  61. 0061have hold : ∃ v. BetaAt(x,x1,i,v) ∧ FpMulGridValue(p,i,v)
  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