FP004E

prime_field_unit_trace_successor

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.

Append the genuinely computed next unit sum to an actual finite beta history.

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. ∀ b. ∀ c. ∀ n. ∀ r. ∀ s. FpUnitTrace(p,b,c,n,r) → FpAdd(p,r,1,s) → FpUnitMultiple(p,S n,s)

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

Definition DAG

FpAdd(p,a,b,c) · 1FpUnitTrace(p,b,c,n,r) · 2FpUnitMultiple(p,n,r) · 1Lt(a,b) · 2BetaAt(b,c,i,x) · 3

Actual proof prerequisites

beta_prefix_extend · checked external prerequisiteprime_field_unit_trace_recodefinite_lt_succ_eq_or_lt · checked external prerequisite
Original expanded first-order statement 
forall p b c n r s. (((((exists ff_h_pft_trace_successor_sourcestart. ff_h_pft_trace_successor_sourcestart + S (0) = S ((S (0)) * c)) /\ exists ff_q_pft_trace_successor_sourcestart. b = ff_q_pft_trace_successor_sourcestart * S ((S (0)) * c) + (0))) /\ (((((exists ff_h_pft_trace_successor_sourceterminal. ff_h_pft_trace_successor_sourceterminal + S (r) = S ((S (n)) * c)) /\ exists ff_q_pft_trace_successor_sourceterminal. b = ff_q_pft_trace_successor_sourceterminal * S ((S (n)) * c) + (r))) /\ ((forall pff_trace_index_trace_successor_sourcesteps. (exists pfa_gap_trace_successor_sourcestepsindex. pfa_gap_trace_successor_sourcestepsindex + S (pff_trace_index_trace_successor_sourcesteps) = (n)) -> exists pff_trace_before_trace_successor_sourcesteps pff_trace_after_trace_successor_sourcesteps. ((((exists ff_h_pft_trace_successor_sourcestepsbefore. ff_h_pft_trace_successor_sourcestepsbefore + S (pff_trace_before_trace_successor_sourcesteps) = S ((S (pff_trace_index_trace_successor_sourcesteps)) * c)) /\ exists ff_q_pft_trace_successor_sourcestepsbefore. b = ff_q_pft_trace_successor_sourcestepsbefore * S ((S (pff_trace_index_trace_successor_sourcesteps)) * c) + (pff_trace_before_trace_successor_sourcesteps))) /\ (((((exists ff_h_pft_trace_successor_sourcestepsafter. ff_h_pft_trace_successor_sourcestepsafter + S (pff_trace_after_trace_successor_sourcesteps) = S ((S (S (pff_trace_index_trace_successor_sourcesteps))) * c)) /\ exists ff_q_pft_trace_successor_sourcestepsafter. b = ff_q_pft_trace_successor_sourcestepsafter * S ((S (S (pff_trace_index_trace_successor_sourcesteps))) * c) + (pff_trace_after_trace_successor_sourcesteps))) /\ ((((exists pfa_gap_trace_successor_sourcestepsadditionleft. pfa_gap_trace_successor_sourcestepsadditionleft + S (pff_trace_before_trace_successor_sourcesteps) = (p)) /\ (((exists pfa_gap_trace_successor_sourcestepsadditionright. pfa_gap_trace_successor_sourcestepsadditionright + S (1) = (p)) /\ ((((exists pfa_gap_trace_successor_sourcestepsadditionresultbound. pfa_gap_trace_successor_sourcestepsadditionresultbound + S (pff_trace_after_trace_successor_sourcesteps) = (p)) /\ ((exists pfa_offset_left_trace_successor_sourcestepsadditionresultcongruence pfa_offset_right_trace_successor_sourcestepsadditionresultcongruence. ((pff_trace_before_trace_successor_sourcesteps) + (1)) + (p) * pfa_offset_left_trace_successor_sourcestepsadditionresultcongruence = (pff_trace_after_trace_successor_sourcesteps) + (p) * pfa_offset_right_trace_successor_sourcestepsadditionresultcongruence))))))))))))))))))) -> (((exists pfa_gap_trace_successor_addleft. pfa_gap_trace_successor_addleft + S (r) = (p)) /\ (((exists pfa_gap_trace_successor_addright. pfa_gap_trace_successor_addright + S (1) = (p)) /\ ((((exists pfa_gap_trace_successor_addresultbound. pfa_gap_trace_successor_addresultbound + S (s) = (p)) /\ ((exists pfa_offset_left_trace_successor_addresultcongruence pfa_offset_right_trace_successor_addresultcongruence. ((r) + (1)) + (p) * pfa_offset_left_trace_successor_addresultcongruence = (s) + (p) * pfa_offset_right_trace_successor_addresultcongruence))))))))) -> exists B C. (((((exists ff_h_pft_trace_successor_resultstart. ff_h_pft_trace_successor_resultstart + S (0) = S ((S (0)) * C)) /\ exists ff_q_pft_trace_successor_resultstart. B = ff_q_pft_trace_successor_resultstart * S ((S (0)) * C) + (0))) /\ (((((exists ff_h_pft_trace_successor_resultterminal. ff_h_pft_trace_successor_resultterminal + S (s) = S ((S (S n)) * C)) /\ exists ff_q_pft_trace_successor_resultterminal. B = ff_q_pft_trace_successor_resultterminal * S ((S (S n)) * C) + (s))) /\ ((forall pff_trace_index_trace_successor_resultsteps. (exists pfa_gap_trace_successor_resultstepsindex. pfa_gap_trace_successor_resultstepsindex + S (pff_trace_index_trace_successor_resultsteps) = (S n)) -> exists pff_trace_before_trace_successor_resultsteps pff_trace_after_trace_successor_resultsteps. ((((exists ff_h_pft_trace_successor_resultstepsbefore. ff_h_pft_trace_successor_resultstepsbefore + S (pff_trace_before_trace_successor_resultsteps) = S ((S (pff_trace_index_trace_successor_resultsteps)) * C)) /\ exists ff_q_pft_trace_successor_resultstepsbefore. B = ff_q_pft_trace_successor_resultstepsbefore * S ((S (pff_trace_index_trace_successor_resultsteps)) * C) + (pff_trace_before_trace_successor_resultsteps))) /\ (((((exists ff_h_pft_trace_successor_resultstepsafter. ff_h_pft_trace_successor_resultstepsafter + S (pff_trace_after_trace_successor_resultsteps) = S ((S (S (pff_trace_index_trace_successor_resultsteps))) * C)) /\ exists ff_q_pft_trace_successor_resultstepsafter. B = ff_q_pft_trace_successor_resultstepsafter * S ((S (S (pff_trace_index_trace_successor_resultsteps))) * C) + (pff_trace_after_trace_successor_resultsteps))) /\ ((((exists pfa_gap_trace_successor_resultstepsadditionleft. pfa_gap_trace_successor_resultstepsadditionleft + S (pff_trace_before_trace_successor_resultsteps) = (p)) /\ (((exists pfa_gap_trace_successor_resultstepsadditionright. pfa_gap_trace_successor_resultstepsadditionright + S (1) = (p)) /\ ((((exists pfa_gap_trace_successor_resultstepsadditionresultbound. pfa_gap_trace_successor_resultstepsadditionresultbound + S (pff_trace_after_trace_successor_resultsteps) = (p)) /\ ((exists pfa_offset_left_trace_successor_resultstepsadditionresultcongruence pfa_offset_right_trace_successor_resultstepsadditionresultcongruence. ((pff_trace_before_trace_successor_resultsteps) + (1)) + (p) * pfa_offset_left_trace_successor_resultstepsadditionresultcongruence = (pff_trace_after_trace_successor_resultsteps) + (p) * pfa_offset_right_trace_successor_resultstepsadditionresultcongruence)))))))))))))))))))

Complete tactic proof in conservative notation

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

58 script commands · 20 reading checkpoints · 3 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.

Named ingredients (1)
prime field unit trace recode
01Fix variables and assumptionsL1–8

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

  1. L1
    intro p
  2. L2
    intro b
  3. L3
    intro c
  4. L4
    intro n
  5. L5
    intro r
  6. L6
    intro s
  7. L7
    intro htrace
  8. L8
    intro hadd
02Establish heL9–14

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

  1. L9
    have he : ∃ B. ∃ C. BetaAt(B,C,S n,s) ∧ (∀ x. ∀ y. Lt(x,S n) → BetaAt(b,c,x,y) → BetaAt(B,C,x,y))Definitions: BetaAt(B,C,S n,s)Lt(x,S n)BetaAt(b,c,x,y)BetaAt(B,C,x,y)Original native command in the exact edition
  2. L10
    specialize beta_prefix_extend (S n)
  3. L11
    specialize beta_prefix_extend (b)
  4. L12
    specialize beta_prefix_extend (c)
  5. L13
    specialize beta_prefix_extend (s)
  6. L14
    apply beta_prefix_extend
03Separate the logical casesL15–17

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

  1. L15
    cases he
  2. L16
    cases he_witness
  3. L17
    cases he_witness_witness
04Establish htL18–27

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply prime field unit trace recode.

  1. L18
    have ht : FpUnitTrace(p,x,x1,n,r)Definitions: FpUnitTrace(p,x,x1,n,r)Original native command in the exact edition
  2. L19
    specialize prime_field_unit_trace_recode (p)
  3. L20
    specialize prime_field_unit_trace_recode (b)
  4. L21
    specialize prime_field_unit_trace_recode (c)
  5. L22
    specialize prime_field_unit_trace_recode (x)
  6. L23
    specialize prime_field_unit_trace_recode (x1)
  7. L24
    specialize prime_field_unit_trace_recode (n)
  8. L25
    specialize prime_field_unit_trace_recode (r)
  9. L26
    apply prime_field_unit_trace_recode
  10. L27
    exact htrace
05Use earlier factsL28–28

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

  1. L28
    exact he_witness_witness_right
06Separate the logical casesL29–30

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

  1. L29
    cases ht
  2. L30
    cases ht_right
07Construct an explicit witnessL31–32

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

  1. L31
    exists x
  2. L32
    exists x1
08Separate the logical casesL33–33

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

  1. L33
    split
09Use earlier factsL34–34

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

  1. L34
    exact ht_left
10Separate the logical casesL35–35

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

  1. L35
    split
11Use earlier factsL36–36

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

  1. L36
    exact he_witness_witness_left
12Fix variables and assumptionsL37–38

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

  1. L37
    intro i
  2. L38
    intro hi
13Establish hcasesL39–43

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. L39
    have hcases : i = n ∨ Lt(i,n)Definitions: Lt(i,n)Original native command in the exact edition
  2. L40
    specialize finite_lt_succ_eq_or_lt (n)
  3. L41
    specialize finite_lt_succ_eq_or_lt (i)
  4. L42
    apply finite_lt_succ_eq_or_lt
  5. L43
    exact hi
14Separate the logical casesL44–44

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

  1. L44
    cases hcases
15Calculate and transport equalitiesL45–48

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

  1. L45
    rewrite hcases_left
  2. L46
    rewrite hcases_left
  3. L47
    rewrite hcases_left
  4. L48
    rewrite hcases_left
16Construct an explicit witnessL49–50

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

  1. L49
    exists r
  2. L50
    exists s
17Separate the logical casesL51–51

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

  1. L51
    split
18Use earlier factsL52–52

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

  1. L52
    exact ht_right_left
19Separate the logical casesL53–53

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

  1. L53
    split
20Use earlier factsL54–58

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

  1. L54
    exact he_witness_witness_left
  2. L55
    exact hadd
  3. L56
    specialize ht_right_right (i)
  4. L57
    apply ht_right_right
  5. L58
    exact hcases_right

Library-wide reading audit

Original defined command ledger · 58 lines
  1. 0001intro p
  2. 0002intro b
  3. 0003intro c
  4. 0004intro n
  5. 0005intro r
  6. 0006intro s
  7. 0007intro htrace
  8. 0008intro hadd
  9. 0009have he : ∃ B. ∃ C. BetaAt(B,C,S n,s) ∧ (∀ x. ∀ y. Lt(x,S n) → BetaAt(b,c,x,y) → BetaAt(B,C,x,y))
  10. 0010specialize beta_prefix_extend (S n)
  11. 0011specialize beta_prefix_extend (b)
  12. 0012specialize beta_prefix_extend (c)
  13. 0013specialize beta_prefix_extend (s)
  14. 0014apply beta_prefix_extend
  15. 0015cases he
  16. 0016cases he_witness
  17. 0017cases he_witness_witness
  18. 0018have ht : FpUnitTrace(p,x,x1,n,r)
  19. 0019specialize prime_field_unit_trace_recode (p)
  20. 0020specialize prime_field_unit_trace_recode (b)
  21. 0021specialize prime_field_unit_trace_recode (c)
  22. 0022specialize prime_field_unit_trace_recode (x)
  23. 0023specialize prime_field_unit_trace_recode (x1)
  24. 0024specialize prime_field_unit_trace_recode (n)
  25. 0025specialize prime_field_unit_trace_recode (r)
  26. 0026apply prime_field_unit_trace_recode
  27. 0027exact htrace
  28. 0028exact he_witness_witness_right
  29. 0029cases ht
  30. 0030cases ht_right
  31. 0031exists x
  32. 0032exists x1
  33. 0033split
  34. 0034exact ht_left
  35. 0035split
  36. 0036exact he_witness_witness_left
  37. 0037intro i
  38. 0038intro hi
  39. 0039have hcases : i = n ∨ Lt(i,n)
  40. 0040specialize finite_lt_succ_eq_or_lt (n)
  41. 0041specialize finite_lt_succ_eq_or_lt (i)
  42. 0042apply finite_lt_succ_eq_or_lt
  43. 0043exact hi
  44. 0044cases hcases
  45. 0045rewrite hcases_left
  46. 0046rewrite hcases_left
  47. 0047rewrite hcases_left
  48. 0048rewrite hcases_left
  49. 0049exists r
  50. 0050exists s
  51. 0051split
  52. 0052exact ht_right_left
  53. 0053split
  54. 0054exact he_witness_witness_left
  55. 0055exact hadd
  56. 0056specialize ht_right_right (i)
  57. 0057apply ht_right_right
  58. 0058exact hcases_right