FP004D

prime_field_unit_trace_recode

A genuine recoding preserving every one of the n+1 trace entries preserves all actual unit-addition steps.

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. ∀ b. ∀ c. ∀ B. ∀ C. ∀ n. ∀ r. FpUnitTrace(p,b,c,n,r) → (∀ x. ∀ y. Lt(x,S n) → BetaAt(b,c,x,y) → BetaAt(B,C,x,y)) → FpUnitTrace(p,B,C,n,r)

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

Definition DAG

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

Actual proof prerequisites

zero_add · checked external prerequisitele_succ · checked external prerequisitesucc_le_succ · checked external prerequisite
Original expanded first-order statement 
forall p b c B C n r. (((((exists ff_h_pft_trace_recode_sourcestart. ff_h_pft_trace_recode_sourcestart + S (0) = S ((S (0)) * c)) /\ exists ff_q_pft_trace_recode_sourcestart. b = ff_q_pft_trace_recode_sourcestart * S ((S (0)) * c) + (0))) /\ (((((exists ff_h_pft_trace_recode_sourceterminal. ff_h_pft_trace_recode_sourceterminal + S (r) = S ((S (n)) * c)) /\ exists ff_q_pft_trace_recode_sourceterminal. b = ff_q_pft_trace_recode_sourceterminal * S ((S (n)) * c) + (r))) /\ ((forall pff_trace_index_trace_recode_sourcesteps. (exists pfa_gap_trace_recode_sourcestepsindex. pfa_gap_trace_recode_sourcestepsindex + S (pff_trace_index_trace_recode_sourcesteps) = (n)) -> exists pff_trace_before_trace_recode_sourcesteps pff_trace_after_trace_recode_sourcesteps. ((((exists ff_h_pft_trace_recode_sourcestepsbefore. ff_h_pft_trace_recode_sourcestepsbefore + S (pff_trace_before_trace_recode_sourcesteps) = S ((S (pff_trace_index_trace_recode_sourcesteps)) * c)) /\ exists ff_q_pft_trace_recode_sourcestepsbefore. b = ff_q_pft_trace_recode_sourcestepsbefore * S ((S (pff_trace_index_trace_recode_sourcesteps)) * c) + (pff_trace_before_trace_recode_sourcesteps))) /\ (((((exists ff_h_pft_trace_recode_sourcestepsafter. ff_h_pft_trace_recode_sourcestepsafter + S (pff_trace_after_trace_recode_sourcesteps) = S ((S (S (pff_trace_index_trace_recode_sourcesteps))) * c)) /\ exists ff_q_pft_trace_recode_sourcestepsafter. b = ff_q_pft_trace_recode_sourcestepsafter * S ((S (S (pff_trace_index_trace_recode_sourcesteps))) * c) + (pff_trace_after_trace_recode_sourcesteps))) /\ ((((exists pfa_gap_trace_recode_sourcestepsadditionleft. pfa_gap_trace_recode_sourcestepsadditionleft + S (pff_trace_before_trace_recode_sourcesteps) = (p)) /\ (((exists pfa_gap_trace_recode_sourcestepsadditionright. pfa_gap_trace_recode_sourcestepsadditionright + S (1) = (p)) /\ ((((exists pfa_gap_trace_recode_sourcestepsadditionresultbound. pfa_gap_trace_recode_sourcestepsadditionresultbound + S (pff_trace_after_trace_recode_sourcesteps) = (p)) /\ ((exists pfa_offset_left_trace_recode_sourcestepsadditionresultcongruence pfa_offset_right_trace_recode_sourcestepsadditionresultcongruence. ((pff_trace_before_trace_recode_sourcesteps) + (1)) + (p) * pfa_offset_left_trace_recode_sourcestepsadditionresultcongruence = (pff_trace_after_trace_recode_sourcesteps) + (p) * pfa_offset_right_trace_recode_sourcestepsadditionresultcongruence))))))))))))))))))) -> (forall i v. (exists pfa_gap_trace_recode_bound. pfa_gap_trace_recode_bound + S (i) = (S n)) -> (((exists ff_h_pft_trace_recode_old. ff_h_pft_trace_recode_old + S (v) = S ((S (i)) * c)) /\ exists ff_q_pft_trace_recode_old. b = ff_q_pft_trace_recode_old * S ((S (i)) * c) + (v))) -> (((exists ff_h_pft_trace_recode_new. ff_h_pft_trace_recode_new + S (v) = S ((S (i)) * C)) /\ exists ff_q_pft_trace_recode_new. B = ff_q_pft_trace_recode_new * S ((S (i)) * C) + (v)))) -> (((((exists ff_h_pft_trace_recode_targetstart. ff_h_pft_trace_recode_targetstart + S (0) = S ((S (0)) * C)) /\ exists ff_q_pft_trace_recode_targetstart. B = ff_q_pft_trace_recode_targetstart * S ((S (0)) * C) + (0))) /\ (((((exists ff_h_pft_trace_recode_targetterminal. ff_h_pft_trace_recode_targetterminal + S (r) = S ((S (n)) * C)) /\ exists ff_q_pft_trace_recode_targetterminal. B = ff_q_pft_trace_recode_targetterminal * S ((S (n)) * C) + (r))) /\ ((forall pff_trace_index_trace_recode_targetsteps. (exists pfa_gap_trace_recode_targetstepsindex. pfa_gap_trace_recode_targetstepsindex + S (pff_trace_index_trace_recode_targetsteps) = (n)) -> exists pff_trace_before_trace_recode_targetsteps pff_trace_after_trace_recode_targetsteps. ((((exists ff_h_pft_trace_recode_targetstepsbefore. ff_h_pft_trace_recode_targetstepsbefore + S (pff_trace_before_trace_recode_targetsteps) = S ((S (pff_trace_index_trace_recode_targetsteps)) * C)) /\ exists ff_q_pft_trace_recode_targetstepsbefore. B = ff_q_pft_trace_recode_targetstepsbefore * S ((S (pff_trace_index_trace_recode_targetsteps)) * C) + (pff_trace_before_trace_recode_targetsteps))) /\ (((((exists ff_h_pft_trace_recode_targetstepsafter. ff_h_pft_trace_recode_targetstepsafter + S (pff_trace_after_trace_recode_targetsteps) = S ((S (S (pff_trace_index_trace_recode_targetsteps))) * C)) /\ exists ff_q_pft_trace_recode_targetstepsafter. B = ff_q_pft_trace_recode_targetstepsafter * S ((S (S (pff_trace_index_trace_recode_targetsteps))) * C) + (pff_trace_after_trace_recode_targetsteps))) /\ ((((exists pfa_gap_trace_recode_targetstepsadditionleft. pfa_gap_trace_recode_targetstepsadditionleft + S (pff_trace_before_trace_recode_targetsteps) = (p)) /\ (((exists pfa_gap_trace_recode_targetstepsadditionright. pfa_gap_trace_recode_targetstepsadditionright + S (1) = (p)) /\ ((((exists pfa_gap_trace_recode_targetstepsadditionresultbound. pfa_gap_trace_recode_targetstepsadditionresultbound + S (pff_trace_after_trace_recode_targetsteps) = (p)) /\ ((exists pfa_offset_left_trace_recode_targetstepsadditionresultcongruence pfa_offset_right_trace_recode_targetstepsadditionresultcongruence. ((pff_trace_before_trace_recode_targetsteps) + (1)) + (p) * pfa_offset_left_trace_recode_targetstepsadditionresultcongruence = (pff_trace_after_trace_recode_targetsteps) + (p) * pfa_offset_right_trace_recode_targetstepsadditionresultcongruence)))))))))))))))))))

Complete tactic proof in conservative notation

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

56 script commands · 18 reading checkpoints · 1 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–9

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 B
  5. L5
    intro C
  6. L6
    intro n
  7. L7
    intro r
  8. L8
    intro htrace
  9. L9
    intro hpreserve
02Separate the logical casesL10–12

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

  1. L10
    cases htrace
  2. L11
    cases htrace_right
  3. L12
    split
03Use earlier factsL13–15

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

  1. L13
    specialize hpreserve (0)
  2. L14
    specialize hpreserve (0)
  3. L15
    apply hpreserve
04Construct an explicit witnessL16–16

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

  1. L16
    exists n
05Calculate and transport equalitiesL17–17

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

  1. L17
    simp
06Use earlier factsL18–18

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

  1. L18
    exact htrace_left
07Separate the logical casesL19–19

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

  1. L19
    split
08Use earlier factsL20–22

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

  1. L20
    specialize hpreserve (n)
  2. L21
    specialize hpreserve (r)
  3. L22
    apply hpreserve
09Construct an explicit witnessL23–23

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

  1. L23
    exists 0
10Use earlier factsL24–25

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

  1. L24
    apply zero_add
  2. L25
    exact htrace_right_left
11Fix variables and assumptionsL26–27

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

  1. L26
    intro i
  2. L27
    intro hi
12Establish hsL28–31

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

  1. L28
    have hs : ∃ u. ∃ v. BetaAt(b,c,i,u) ∧ (BetaAt(b,c,S i,v) ∧ FpAdd(p,u,1,v))Definitions: BetaAt(b,c,i,u)BetaAt(b,c,S i,v)FpAdd(p,u,1,v)Original native command in the exact edition
  2. L29
    specialize htrace_right_right (i)
  3. L30
    apply htrace_right_right
  4. L31
    exact hi
13Separate the logical casesL32–35

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

  1. L32
    cases hs
  2. L33
    cases hs_witness
  3. L34
    cases hs_witness_witness
  4. L35
    cases hs_witness_witness_right
14Construct an explicit witnessL36–37

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

  1. L36
    exists x
  2. L37
    exists x1
15Separate the logical casesL38–38

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

  1. L38
    split
16Use earlier factsL39–46

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

  1. L39
    specialize hpreserve (i)
  2. L40
    specialize hpreserve (x)
  3. L41
    apply hpreserve
  4. L42
    specialize le_succ (S i)
  5. L43
    specialize le_succ (n)
  6. L44
    apply le_succ
  7. L45
    exact hi
  8. L46
    exact hs_witness_witness_left
17Separate the logical casesL47–47

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

  1. L47
    split
18Use earlier factsL48–56

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

  1. L48
    specialize hpreserve (S i)
  2. L49
    specialize hpreserve (x1)
  3. L50
    apply hpreserve
  4. L51
    specialize succ_le_succ (S i)
  5. L52
    specialize succ_le_succ (n)
  6. L53
    apply succ_le_succ
  7. L54
    exact hi
  8. L55
    exact hs_witness_witness_right_left
  9. L56
    exact hs_witness_witness_right_right

Library-wide reading audit

Original defined command ledger · 56 lines
  1. 0001intro p
  2. 0002intro b
  3. 0003intro c
  4. 0004intro B
  5. 0005intro C
  6. 0006intro n
  7. 0007intro r
  8. 0008intro htrace
  9. 0009intro hpreserve
  10. 0010cases htrace
  11. 0011cases htrace_right
  12. 0012split
  13. 0013specialize hpreserve (0)
  14. 0014specialize hpreserve (0)
  15. 0015apply hpreserve
  16. 0016exists n
  17. 0017simp
  18. 0018exact htrace_left
  19. 0019split
  20. 0020specialize hpreserve (n)
  21. 0021specialize hpreserve (r)
  22. 0022apply hpreserve
  23. 0023exists 0
  24. 0024apply zero_add
  25. 0025exact htrace_right_left
  26. 0026intro i
  27. 0027intro hi
  28. 0028have hs : ∃ u. ∃ v. BetaAt(b,c,i,u) ∧ (BetaAt(b,c,S i,v) ∧ FpAdd(p,u,1,v))
  29. 0029specialize htrace_right_right (i)
  30. 0030apply htrace_right_right
  31. 0031exact hi
  32. 0032cases hs
  33. 0033cases hs_witness
  34. 0034cases hs_witness_witness
  35. 0035cases hs_witness_witness_right
  36. 0036exists x
  37. 0037exists x1
  38. 0038split
  39. 0039specialize hpreserve (i)
  40. 0040specialize hpreserve (x)
  41. 0041apply hpreserve
  42. 0042specialize le_succ (S i)
  43. 0043specialize le_succ (n)
  44. 0044apply le_succ
  45. 0045exact hi
  46. 0046exact hs_witness_witness_left
  47. 0047split
  48. 0048specialize hpreserve (S i)
  49. 0049specialize hpreserve (x1)
  50. 0050apply hpreserve
  51. 0051specialize succ_le_succ (S i)
  52. 0052specialize succ_le_succ (n)
  53. 0053apply succ_le_succ
  54. 0054exact hi
  55. 0055exact hs_witness_witness_right_left
  56. 0056exact hs_witness_witness_right_right