FP004E

prime_field_unit_trace_successor

Alpha v34 independently verified · alpha_closed; checked-use authorized; not Stable

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

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

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

Constructive proof overview

Generated structural guide

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

The unchanged tactic script uses 3 declared prerequisites and contains 58 exact native proof lines.

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

Proof neighborhood

Direct dependencies

beta_prefix_extend Stable theorem; checked-use authorized FP004D prime_field_unit_trace_recode finite_lt_succ_eq_or_lt Stable theorem; checked-use authorized

Direct dependents

FP0051 prime_field_unit_trace_exists

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Local theorem links identify exact declared prerequisites. This exact body belongs to a complete independently kernel-checked constructive proof bundle and has Alpha checked-use authority; it does not imply Stable membership.

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.

Named ingredients (1)
prime field unit trace recode

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–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: LtBetaAt
  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
  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 \/ (exists pfa_gap_trace_append_cases. pfa_gap_trace_append_cases + S (i) = (n))
  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 exact 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 : exists B C. (((exists ff_h_pft_trace_append_last. ff_h_pft_trace_append_last + S (s) = S ((S (S n)) * C)) /\ exists ff_q_pft_trace_append_last. B = ff_q_pft_trace_append_last * S ((S (S n)) * C) + (s))) /\ (forall i v. (exists pfa_gap_trace_append_bound. pfa_gap_trace_append_bound + S (i) = (S n)) -> (((exists ff_h_pft_trace_append_old. ff_h_pft_trace_append_old + S (v) = S ((S (i)) * c)) /\ exists ff_q_pft_trace_append_old. b = ff_q_pft_trace_append_old * S ((S (i)) * c) + (v))) -> (((exists ff_h_pft_trace_append_new. ff_h_pft_trace_append_new + S (v) = S ((S (i)) * C)) /\ exists ff_q_pft_trace_append_new. B = ff_q_pft_trace_append_new * S ((S (i)) * C) + (v))))
  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 : ((((exists ff_h_pft_trace_append_recodedstart. ff_h_pft_trace_append_recodedstart + S (0) = S ((S (0)) * x1)) /\ exists ff_q_pft_trace_append_recodedstart. x = ff_q_pft_trace_append_recodedstart * S ((S (0)) * x1) + (0))) /\ (((((exists ff_h_pft_trace_append_recodedterminal. ff_h_pft_trace_append_recodedterminal + S (r) = S ((S (n)) * x1)) /\ exists ff_q_pft_trace_append_recodedterminal. x = ff_q_pft_trace_append_recodedterminal * S ((S (n)) * x1) + (r))) /\ ((forall pff_trace_index_trace_append_recodedsteps. (exists pfa_gap_trace_append_recodedstepsindex. pfa_gap_trace_append_recodedstepsindex + S (pff_trace_index_trace_append_recodedsteps) = (n)) -> exists pff_trace_before_trace_append_recodedsteps pff_trace_after_trace_append_recodedsteps. ((((exists ff_h_pft_trace_append_recodedstepsbefore. ff_h_pft_trace_append_recodedstepsbefore + S (pff_trace_before_trace_append_recodedsteps) = S ((S (pff_trace_index_trace_append_recodedsteps)) * x1)) /\ exists ff_q_pft_trace_append_recodedstepsbefore. x = ff_q_pft_trace_append_recodedstepsbefore * S ((S (pff_trace_index_trace_append_recodedsteps)) * x1) + (pff_trace_before_trace_append_recodedsteps))) /\ (((((exists ff_h_pft_trace_append_recodedstepsafter. ff_h_pft_trace_append_recodedstepsafter + S (pff_trace_after_trace_append_recodedsteps) = S ((S (S (pff_trace_index_trace_append_recodedsteps))) * x1)) /\ exists ff_q_pft_trace_append_recodedstepsafter. x = ff_q_pft_trace_append_recodedstepsafter * S ((S (S (pff_trace_index_trace_append_recodedsteps))) * x1) + (pff_trace_after_trace_append_recodedsteps))) /\ ((((exists pfa_gap_trace_append_recodedstepsadditionleft. pfa_gap_trace_append_recodedstepsadditionleft + S (pff_trace_before_trace_append_recodedsteps) = (p)) /\ (((exists pfa_gap_trace_append_recodedstepsadditionright. pfa_gap_trace_append_recodedstepsadditionright + S (1) = (p)) /\ ((((exists pfa_gap_trace_append_recodedstepsadditionresultbound. pfa_gap_trace_append_recodedstepsadditionresultbound + S (pff_trace_after_trace_append_recodedsteps) = (p)) /\ ((exists pfa_offset_left_trace_append_recodedstepsadditionresultcongruence pfa_offset_right_trace_append_recodedstepsadditionresultcongruence. ((pff_trace_before_trace_append_recodedsteps) + (1)) + (p) * pfa_offset_left_trace_append_recodedstepsadditionresultcongruence = (pff_trace_after_trace_append_recodedsteps) + (p) * pfa_offset_right_trace_append_recodedstepsadditionresultcongruence))))))))))))))))))
  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 \/ (exists pfa_gap_trace_append_cases. pfa_gap_trace_append_cases + S (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