FP004F

prime_field_unit_trace_residue

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

Ordinary induction proves that an actual n-step addition-of-one history has canonical residue n; the relation does not assume this invariant.

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 n b c r. (~((p) = 1) /\ forall pfa_factor_left_trace_bridge_domain pfa_factor_right_trace_bridge_domain. (p) = pfa_factor_left_trace_bridge_domain * pfa_factor_right_trace_bridge_domain -> pfa_factor_left_trace_bridge_domain = 1 \/ pfa_factor_right_trace_bridge_domain = 1) -> (((((exists ff_h_pft_trace_bridge_sourcestart. ff_h_pft_trace_bridge_sourcestart + S (0) = S ((S (0)) * c)) /\ exists ff_q_pft_trace_bridge_sourcestart. b = ff_q_pft_trace_bridge_sourcestart * S ((S (0)) * c) + (0))) /\ (((((exists ff_h_pft_trace_bridge_sourceterminal. ff_h_pft_trace_bridge_sourceterminal + S (r) = S ((S (n)) * c)) /\ exists ff_q_pft_trace_bridge_sourceterminal. b = ff_q_pft_trace_bridge_sourceterminal * S ((S (n)) * c) + (r))) /\ ((forall pff_trace_index_trace_bridge_sourcesteps. (exists pfa_gap_trace_bridge_sourcestepsindex. pfa_gap_trace_bridge_sourcestepsindex + S (pff_trace_index_trace_bridge_sourcesteps) = (n)) -> exists pff_trace_before_trace_bridge_sourcesteps pff_trace_after_trace_bridge_sourcesteps. ((((exists ff_h_pft_trace_bridge_sourcestepsbefore. ff_h_pft_trace_bridge_sourcestepsbefore + S (pff_trace_before_trace_bridge_sourcesteps) = S ((S (pff_trace_index_trace_bridge_sourcesteps)) * c)) /\ exists ff_q_pft_trace_bridge_sourcestepsbefore. b = ff_q_pft_trace_bridge_sourcestepsbefore * S ((S (pff_trace_index_trace_bridge_sourcesteps)) * c) + (pff_trace_before_trace_bridge_sourcesteps))) /\ (((((exists ff_h_pft_trace_bridge_sourcestepsafter. ff_h_pft_trace_bridge_sourcestepsafter + S (pff_trace_after_trace_bridge_sourcesteps) = S ((S (S (pff_trace_index_trace_bridge_sourcesteps))) * c)) /\ exists ff_q_pft_trace_bridge_sourcestepsafter. b = ff_q_pft_trace_bridge_sourcestepsafter * S ((S (S (pff_trace_index_trace_bridge_sourcesteps))) * c) + (pff_trace_after_trace_bridge_sourcesteps))) /\ ((((exists pfa_gap_trace_bridge_sourcestepsadditionleft. pfa_gap_trace_bridge_sourcestepsadditionleft + S (pff_trace_before_trace_bridge_sourcesteps) = (p)) /\ (((exists pfa_gap_trace_bridge_sourcestepsadditionright. pfa_gap_trace_bridge_sourcestepsadditionright + S (1) = (p)) /\ ((((exists pfa_gap_trace_bridge_sourcestepsadditionresultbound. pfa_gap_trace_bridge_sourcestepsadditionresultbound + S (pff_trace_after_trace_bridge_sourcesteps) = (p)) /\ ((exists pfa_offset_left_trace_bridge_sourcestepsadditionresultcongruence pfa_offset_right_trace_bridge_sourcestepsadditionresultcongruence. ((pff_trace_before_trace_bridge_sourcesteps) + (1)) + (p) * pfa_offset_left_trace_bridge_sourcestepsadditionresultcongruence = (pff_trace_after_trace_bridge_sourcesteps) + (p) * pfa_offset_right_trace_bridge_sourcestepsadditionresultcongruence))))))))))))))))))) -> (((exists pfa_gap_trace_bridge_resultbound. pfa_gap_trace_bridge_resultbound + S (r) = (p)) /\ ((exists pfa_offset_left_trace_bridge_resultcongruence pfa_offset_right_trace_bridge_resultcongruence. (n) + (p) * pfa_offset_left_trace_bridge_resultcongruence = (r) + (p) * pfa_offset_right_trace_bridge_resultcongruence))))

Constructive proof overview

Generated structural guide

Ordinary induction proves that an actual n-step addition-of-one history has canonical residue n; the relation does not assume this invariant.

The unchanged tactic script uses 8 declared prerequisites and contains 97 exact native proof lines.

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

Proof neighborhood

Direct dependencies

beta_at_unique Stable theorem; checked-use authorized FP0003 prime_field_residue_reflexive FP0002 prime_field_zero_below_prime zero_add Stable theorem; checked-use authorized le_succ Stable theorem; checked-use authorized FP0027 prime_field_residue_add prime_two_le Alpha theorem; checked-use authorized FP0004 prime_field_residue_input_equal

Direct dependents

FP0050 prime_field_unit_trace_result_bounded FP0052 prime_field_unit_multiple_residue FP0053 prime_field_unit_multiple_from_residue

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

97 script commands · 27 reading checkpoints · 6 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 (4)
prime field residue reflexiveprime field zero below primeprime field residue addprime field residue input equal

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–2

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

  1. L1
    intro p
  2. L2
    intro n
02Induction on nL3–8

Split the argument into the base and successor obligations. The induction hypothesis is available only in the successor branch.

  1. L3
    induction n
  2. L4
    intro b
  3. L5
    intro c
  4. L6
    intro r
  5. L7
    intro hp
  6. L8
    intro htrace
03Separate the logical casesL9–10

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

  1. L9
    cases htrace
  2. L10
    cases htrace_right
04Establish heqL11–20

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

  1. L11
    have heq : r = 0
  2. L12
    specialize beta_at_unique (b)
  3. L13
    specialize beta_at_unique (c)
  4. L14
    specialize beta_at_unique (0)
  5. L15
    specialize beta_at_unique (r)
  6. L16
    specialize beta_at_unique (0)
  7. L17
    apply beta_at_unique
  8. L18
    exact htrace_right_left
  9. L19
    exact htrace_left
  10. L20
    rewrite heq
05Calculate and transport equalitiesL21–21

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

  1. L21
    rewrite heq
06Use earlier factsL22–27

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

  1. L22
    specialize prime_field_residue_reflexive (p)
  2. L23
    specialize prime_field_residue_reflexive (0)
  3. L24
    apply prime_field_residue_reflexive
  4. L25
    specialize prime_field_zero_below_prime (p)
  5. L26
    apply prime_field_zero_below_prime
  6. L27
    exact hp
07Fix variables and assumptionsL28–32

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

  1. L28
    intro b
  2. L29
    intro c
  3. L30
    intro r
  4. L31
    intro hp
  5. L32
    intro htrace
08Separate the logical casesL33–34

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

  1. L33
    cases htrace
  2. L34
    cases htrace_right
09Establish hsL35–37

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

  1. L35
    have hs : ∃ u. ∃ v. BetaAt(b,c,n,u) ∧ (BetaAt(b,c,S n,v) ∧ FpAdd(p,u,1,v))Definitions: FpAddBetaAt
  2. L36
    specialize htrace_right_right (n)
  3. L37
    apply htrace_right_right
10Construct an explicit witnessL38–38

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

  1. L38
    exists 0
11Use earlier factsL39–39

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

  1. L39
    apply zero_add
12Separate the logical casesL40–43

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

  1. L40
    cases hs
  2. L41
    cases hs_witness
  3. L42
    cases hs_witness_witness
  4. L43
    cases hs_witness_witness_right
13Establish heqL44–52

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

  1. L44
    have heq : x1 = r
  2. L45
    specialize beta_at_unique (b)
  3. L46
    specialize beta_at_unique (c)
  4. L47
    specialize beta_at_unique (S n)
  5. L48
    specialize beta_at_unique (x1)
  6. L49
    specialize beta_at_unique (r)
  7. L50
    apply beta_at_unique
  8. L51
    exact hs_witness_witness_right_left
  9. L52
    exact htrace_right_left
14Establish hprevL53–53

Establish this local claim before using it. It is not an additional assumption.

  1. L53
    have hprev : FpUnitTrace(p,b,c,n,x)Definitions: FpUnitTrace
15Separate the logical casesL54–54

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

  1. L54
    split
16Use earlier factsL55–55

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

  1. L55
    exact htrace_left
17Separate the logical casesL56–56

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

  1. L56
    split
18Use earlier factsL57–57

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

  1. L57
    exact hs_witness_witness_left
19Fix variables and assumptionsL58–59

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

  1. L58
    intro i
  2. L59
    intro hi
20Use earlier factsL60–65

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

  1. L60
    specialize htrace_right_right (i)
  2. L61
    apply htrace_right_right
  3. L62
    specialize le_succ (S i)
  4. L63
    specialize le_succ (n)
  5. L64
    apply le_succ
  6. L65
    exact hi
21Establish hresL66–72

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

  1. L66
    have hres : ((exists pfa_gap_trace_bridge_old_residuebound. pfa_gap_trace_bridge_old_residuebound + S (x) = (p)) /\ ((exists pfa_offset_left_trace_bridge_old_residuecongruence pfa_offset_right_trace_bridge_old_residuecongruence. (n) + (p) * pfa_offset_left_trace_bridge_old_residuecongruence = (x) + (p) * pfa_offset_right_trace_bridge_old_residuecongruence)))
  2. L67
    specialize IH (b)
  3. L68
    specialize IH (c)
  4. L69
    specialize IH (x)
  5. L70
    apply IH
  6. L71
    exact hp
  7. L72
    exact hprev
22Establish hsumL73–82

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

  1. L73
    have hsum : ((exists pfa_gap_trace_bridge_sum_residuebound. pfa_gap_trace_bridge_sum_residuebound + S (x1) = (p)) /\ ((exists pfa_offset_left_trace_bridge_sum_residuecongruence pfa_offset_right_trace_bridge_sum_residuecongruence. (n+1) + (p) * pfa_offset_left_trace_bridge_sum_residuecongruence = (x1) + (p) * pfa_offset_right_trace_bridge_sum_residuecongruence)))
  2. L74
    specialize prime_field_residue_add (p)
  3. L75
    specialize prime_field_residue_add (n)
  4. L76
    specialize prime_field_residue_add (1)
  5. L77
    specialize prime_field_residue_add (x)
  6. L78
    specialize prime_field_residue_add (1)
  7. L79
    specialize prime_field_residue_add (x1)
  8. L80
    apply prime_field_residue_add
  9. L81
    exact hres
  10. L82
    specialize prime_field_residue_reflexive (p)
23Use earlier factsL83–88

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

  1. L83
    specialize prime_field_residue_reflexive (1)
  2. L84
    apply prime_field_residue_reflexive
  3. L85
    specialize prime_two_le (p)
  4. L86
    apply prime_two_le
  5. L87
    exact hp
  6. L88
    exact hs_witness_witness_right_right
24Calculate and transport equalitiesL89–90

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

  1. L89
    rewrite heq at hsum
  2. L90
    rewrite heq at hsum
25Use earlier factsL91–95

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

  1. L91
    specialize prime_field_residue_input_equal (p)
  2. L92
    specialize prime_field_residue_input_equal (S n)
  3. L93
    specialize prime_field_residue_input_equal (n+1)
  4. L94
    specialize prime_field_residue_input_equal (r)
  5. L95
    apply prime_field_residue_input_equal
26Calculate and transport equalitiesL96–96

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

  1. L96
    simp
27Use earlier factsL97–97

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

  1. L97
    exact hsum

Library-wide reading audit

Original exact command ledger · 97 lines
  1. 0001intro p
  2. 0002intro n
  3. 0003induction n
  4. 0004intro b
  5. 0005intro c
  6. 0006intro r
  7. 0007intro hp
  8. 0008intro htrace
  9. 0009cases htrace
  10. 0010cases htrace_right
  11. 0011have heq : r = 0
  12. 0012specialize beta_at_unique (b)
  13. 0013specialize beta_at_unique (c)
  14. 0014specialize beta_at_unique (0)
  15. 0015specialize beta_at_unique (r)
  16. 0016specialize beta_at_unique (0)
  17. 0017apply beta_at_unique
  18. 0018exact htrace_right_left
  19. 0019exact htrace_left
  20. 0020rewrite heq
  21. 0021rewrite heq
  22. 0022specialize prime_field_residue_reflexive (p)
  23. 0023specialize prime_field_residue_reflexive (0)
  24. 0024apply prime_field_residue_reflexive
  25. 0025specialize prime_field_zero_below_prime (p)
  26. 0026apply prime_field_zero_below_prime
  27. 0027exact hp
  28. 0028intro b
  29. 0029intro c
  30. 0030intro r
  31. 0031intro hp
  32. 0032intro htrace
  33. 0033cases htrace
  34. 0034cases htrace_right
  35. 0035have hs : exists u v. (((((exists ff_h_pft_trace_bridge_last_before. ff_h_pft_trace_bridge_last_before + S (u) = S ((S (n)) * c)) /\ exists ff_q_pft_trace_bridge_last_before. b = ff_q_pft_trace_bridge_last_before * S ((S (n)) * c) + (u))) /\ (((((exists ff_h_pft_trace_bridge_last_after. ff_h_pft_trace_bridge_last_after + S (v) = S ((S (S n)) * c)) /\ exists ff_q_pft_trace_bridge_last_after. b = ff_q_pft_trace_bridge_last_after * S ((S (S n)) * c) + (v))) /\ ((((exists pfa_gap_trace_bridge_last_addleft. pfa_gap_trace_bridge_last_addleft + S (u) = (p)) /\ (((exists pfa_gap_trace_bridge_last_addright. pfa_gap_trace_bridge_last_addright + S (1) = (p)) /\ ((((exists pfa_gap_trace_bridge_last_addresultbound. pfa_gap_trace_bridge_last_addresultbound + S (v) = (p)) /\ ((exists pfa_offset_left_trace_bridge_last_addresultcongruence pfa_offset_right_trace_bridge_last_addresultcongruence. ((u) + (1)) + (p) * pfa_offset_left_trace_bridge_last_addresultcongruence = (v) + (p) * pfa_offset_right_trace_bridge_last_addresultcongruence))))))))))))))
  36. 0036specialize htrace_right_right (n)
  37. 0037apply htrace_right_right
  38. 0038exists 0
  39. 0039apply zero_add
  40. 0040cases hs
  41. 0041cases hs_witness
  42. 0042cases hs_witness_witness
  43. 0043cases hs_witness_witness_right
  44. 0044have heq : x1 = r
  45. 0045specialize beta_at_unique (b)
  46. 0046specialize beta_at_unique (c)
  47. 0047specialize beta_at_unique (S n)
  48. 0048specialize beta_at_unique (x1)
  49. 0049specialize beta_at_unique (r)
  50. 0050apply beta_at_unique
  51. 0051exact hs_witness_witness_right_left
  52. 0052exact htrace_right_left
  53. 0053have hprev : ((((exists ff_h_pft_trace_bridge_previousstart. ff_h_pft_trace_bridge_previousstart + S (0) = S ((S (0)) * c)) /\ exists ff_q_pft_trace_bridge_previousstart. b = ff_q_pft_trace_bridge_previousstart * S ((S (0)) * c) + (0))) /\ (((((exists ff_h_pft_trace_bridge_previousterminal. ff_h_pft_trace_bridge_previousterminal + S (x) = S ((S (n)) * c)) /\ exists ff_q_pft_trace_bridge_previousterminal. b = ff_q_pft_trace_bridge_previousterminal * S ((S (n)) * c) + (x))) /\ ((forall pff_trace_index_trace_bridge_previoussteps. (exists pfa_gap_trace_bridge_previousstepsindex. pfa_gap_trace_bridge_previousstepsindex + S (pff_trace_index_trace_bridge_previoussteps) = (n)) -> exists pff_trace_before_trace_bridge_previoussteps pff_trace_after_trace_bridge_previoussteps. ((((exists ff_h_pft_trace_bridge_previousstepsbefore. ff_h_pft_trace_bridge_previousstepsbefore + S (pff_trace_before_trace_bridge_previoussteps) = S ((S (pff_trace_index_trace_bridge_previoussteps)) * c)) /\ exists ff_q_pft_trace_bridge_previousstepsbefore. b = ff_q_pft_trace_bridge_previousstepsbefore * S ((S (pff_trace_index_trace_bridge_previoussteps)) * c) + (pff_trace_before_trace_bridge_previoussteps))) /\ (((((exists ff_h_pft_trace_bridge_previousstepsafter. ff_h_pft_trace_bridge_previousstepsafter + S (pff_trace_after_trace_bridge_previoussteps) = S ((S (S (pff_trace_index_trace_bridge_previoussteps))) * c)) /\ exists ff_q_pft_trace_bridge_previousstepsafter. b = ff_q_pft_trace_bridge_previousstepsafter * S ((S (S (pff_trace_index_trace_bridge_previoussteps))) * c) + (pff_trace_after_trace_bridge_previoussteps))) /\ ((((exists pfa_gap_trace_bridge_previousstepsadditionleft. pfa_gap_trace_bridge_previousstepsadditionleft + S (pff_trace_before_trace_bridge_previoussteps) = (p)) /\ (((exists pfa_gap_trace_bridge_previousstepsadditionright. pfa_gap_trace_bridge_previousstepsadditionright + S (1) = (p)) /\ ((((exists pfa_gap_trace_bridge_previousstepsadditionresultbound. pfa_gap_trace_bridge_previousstepsadditionresultbound + S (pff_trace_after_trace_bridge_previoussteps) = (p)) /\ ((exists pfa_offset_left_trace_bridge_previousstepsadditionresultcongruence pfa_offset_right_trace_bridge_previousstepsadditionresultcongruence. ((pff_trace_before_trace_bridge_previoussteps) + (1)) + (p) * pfa_offset_left_trace_bridge_previousstepsadditionresultcongruence = (pff_trace_after_trace_bridge_previoussteps) + (p) * pfa_offset_right_trace_bridge_previousstepsadditionresultcongruence))))))))))))))))))
  54. 0054split
  55. 0055exact htrace_left
  56. 0056split
  57. 0057exact hs_witness_witness_left
  58. 0058intro i
  59. 0059intro hi
  60. 0060specialize htrace_right_right (i)
  61. 0061apply htrace_right_right
  62. 0062specialize le_succ (S i)
  63. 0063specialize le_succ (n)
  64. 0064apply le_succ
  65. 0065exact hi
  66. 0066have hres : ((exists pfa_gap_trace_bridge_old_residuebound. pfa_gap_trace_bridge_old_residuebound + S (x) = (p)) /\ ((exists pfa_offset_left_trace_bridge_old_residuecongruence pfa_offset_right_trace_bridge_old_residuecongruence. (n) + (p) * pfa_offset_left_trace_bridge_old_residuecongruence = (x) + (p) * pfa_offset_right_trace_bridge_old_residuecongruence)))
  67. 0067specialize IH (b)
  68. 0068specialize IH (c)
  69. 0069specialize IH (x)
  70. 0070apply IH
  71. 0071exact hp
  72. 0072exact hprev
  73. 0073have hsum : ((exists pfa_gap_trace_bridge_sum_residuebound. pfa_gap_trace_bridge_sum_residuebound + S (x1) = (p)) /\ ((exists pfa_offset_left_trace_bridge_sum_residuecongruence pfa_offset_right_trace_bridge_sum_residuecongruence. (n+1) + (p) * pfa_offset_left_trace_bridge_sum_residuecongruence = (x1) + (p) * pfa_offset_right_trace_bridge_sum_residuecongruence)))
  74. 0074specialize prime_field_residue_add (p)
  75. 0075specialize prime_field_residue_add (n)
  76. 0076specialize prime_field_residue_add (1)
  77. 0077specialize prime_field_residue_add (x)
  78. 0078specialize prime_field_residue_add (1)
  79. 0079specialize prime_field_residue_add (x1)
  80. 0080apply prime_field_residue_add
  81. 0081exact hres
  82. 0082specialize prime_field_residue_reflexive (p)
  83. 0083specialize prime_field_residue_reflexive (1)
  84. 0084apply prime_field_residue_reflexive
  85. 0085specialize prime_two_le (p)
  86. 0086apply prime_two_le
  87. 0087exact hp
  88. 0088exact hs_witness_witness_right_right
  89. 0089rewrite heq at hsum
  90. 0090rewrite heq at hsum
  91. 0091specialize prime_field_residue_input_equal (p)
  92. 0092specialize prime_field_residue_input_equal (S n)
  93. 0093specialize prime_field_residue_input_equal (n+1)
  94. 0094specialize prime_field_residue_input_equal (r)
  95. 0095apply prime_field_residue_input_equal
  96. 0096simp
  97. 0097exact hsum