FP004D

prime_field_unit_trace_recode

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

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

Exact expanded first-order arithmetic 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)))))))))))))))))))

Constructive proof overview

Generated structural guide

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

The unchanged tactic script uses 3 declared prerequisites and contains 56 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

zero_add Alpha theorem; checked-use authorized le_succ Alpha theorem; checked-use authorized succ_le_succ Alpha theorem; checked-use authorized

Direct dependents

FP004E prime_field_unit_trace_successor

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

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.

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–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: FpAddBetaAt
  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 exact 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 : exists u v. (((((exists ff_h_pft_trace_recode_before. ff_h_pft_trace_recode_before + S (u) = S ((S (i)) * c)) /\ exists ff_q_pft_trace_recode_before. b = ff_q_pft_trace_recode_before * S ((S (i)) * c) + (u))) /\ (((((exists ff_h_pft_trace_recode_after. ff_h_pft_trace_recode_after + S (v) = S ((S (S i)) * c)) /\ exists ff_q_pft_trace_recode_after. b = ff_q_pft_trace_recode_after * S ((S (S i)) * c) + (v))) /\ ((((exists pfa_gap_trace_recode_addleft. pfa_gap_trace_recode_addleft + S (u) = (p)) /\ (((exists pfa_gap_trace_recode_addright. pfa_gap_trace_recode_addright + S (1) = (p)) /\ ((((exists pfa_gap_trace_recode_addresultbound. pfa_gap_trace_recode_addresultbound + S (v) = (p)) /\ ((exists pfa_offset_left_trace_recode_addresultcongruence pfa_offset_right_trace_recode_addresultcongruence. ((u) + (1)) + (p) * pfa_offset_left_trace_recode_addresultcongruence = (v) + (p) * pfa_offset_right_trace_recode_addresultcongruence))))))))))))))
  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