FP0055

prime_field_unit_multiple_exists_unique

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

Repeated addition is a total functional computation on every natural length, with an actual beta execution 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 n. (~((p) = 1) /\ forall pfa_factor_left_multiple_total_domain pfa_factor_right_multiple_total_domain. (p) = pfa_factor_left_multiple_total_domain * pfa_factor_right_multiple_total_domain -> pfa_factor_left_multiple_total_domain = 1 \/ pfa_factor_right_multiple_total_domain = 1) -> exists r. (exists pff_history_code_multiple_total_chosen pff_history_scale_multiple_total_chosen. (((((exists ff_h_pft_multiple_total_chosenhistorystart. ff_h_pft_multiple_total_chosenhistorystart + S (0) = S ((S (0)) * pff_history_scale_multiple_total_chosen)) /\ exists ff_q_pft_multiple_total_chosenhistorystart. pff_history_code_multiple_total_chosen = ff_q_pft_multiple_total_chosenhistorystart * S ((S (0)) * pff_history_scale_multiple_total_chosen) + (0))) /\ (((((exists ff_h_pft_multiple_total_chosenhistoryterminal. ff_h_pft_multiple_total_chosenhistoryterminal + S (r) = S ((S (n)) * pff_history_scale_multiple_total_chosen)) /\ exists ff_q_pft_multiple_total_chosenhistoryterminal. pff_history_code_multiple_total_chosen = ff_q_pft_multiple_total_chosenhistoryterminal * S ((S (n)) * pff_history_scale_multiple_total_chosen) + (r))) /\ ((forall pff_trace_index_multiple_total_chosenhistorysteps. (exists pfa_gap_multiple_total_chosenhistorystepsindex. pfa_gap_multiple_total_chosenhistorystepsindex + S (pff_trace_index_multiple_total_chosenhistorysteps) = (n)) -> exists pff_trace_before_multiple_total_chosenhistorysteps pff_trace_after_multiple_total_chosenhistorysteps. ((((exists ff_h_pft_multiple_total_chosenhistorystepsbefore. ff_h_pft_multiple_total_chosenhistorystepsbefore + S (pff_trace_before_multiple_total_chosenhistorysteps) = S ((S (pff_trace_index_multiple_total_chosenhistorysteps)) * pff_history_scale_multiple_total_chosen)) /\ exists ff_q_pft_multiple_total_chosenhistorystepsbefore. pff_history_code_multiple_total_chosen = ff_q_pft_multiple_total_chosenhistorystepsbefore * S ((S (pff_trace_index_multiple_total_chosenhistorysteps)) * pff_history_scale_multiple_total_chosen) + (pff_trace_before_multiple_total_chosenhistorysteps))) /\ (((((exists ff_h_pft_multiple_total_chosenhistorystepsafter. ff_h_pft_multiple_total_chosenhistorystepsafter + S (pff_trace_after_multiple_total_chosenhistorysteps) = S ((S (S (pff_trace_index_multiple_total_chosenhistorysteps))) * pff_history_scale_multiple_total_chosen)) /\ exists ff_q_pft_multiple_total_chosenhistorystepsafter. pff_history_code_multiple_total_chosen = ff_q_pft_multiple_total_chosenhistorystepsafter * S ((S (S (pff_trace_index_multiple_total_chosenhistorysteps))) * pff_history_scale_multiple_total_chosen) + (pff_trace_after_multiple_total_chosenhistorysteps))) /\ ((((exists pfa_gap_multiple_total_chosenhistorystepsadditionleft. pfa_gap_multiple_total_chosenhistorystepsadditionleft + S (pff_trace_before_multiple_total_chosenhistorysteps) = (p)) /\ (((exists pfa_gap_multiple_total_chosenhistorystepsadditionright. pfa_gap_multiple_total_chosenhistorystepsadditionright + S (1) = (p)) /\ ((((exists pfa_gap_multiple_total_chosenhistorystepsadditionresultbound. pfa_gap_multiple_total_chosenhistorystepsadditionresultbound + S (pff_trace_after_multiple_total_chosenhistorysteps) = (p)) /\ ((exists pfa_offset_left_multiple_total_chosenhistorystepsadditionresultcongruence pfa_offset_right_multiple_total_chosenhistorystepsadditionresultcongruence. ((pff_trace_before_multiple_total_chosenhistorysteps) + (1)) + (p) * pfa_offset_left_multiple_total_chosenhistorystepsadditionresultcongruence = (pff_trace_after_multiple_total_chosenhistorysteps) + (p) * pfa_offset_right_multiple_total_chosenhistorystepsadditionresultcongruence)))))))))))))))))))) /\ forall s. (exists pff_history_code_multiple_total_other pff_history_scale_multiple_total_other. (((((exists ff_h_pft_multiple_total_otherhistorystart. ff_h_pft_multiple_total_otherhistorystart + S (0) = S ((S (0)) * pff_history_scale_multiple_total_other)) /\ exists ff_q_pft_multiple_total_otherhistorystart. pff_history_code_multiple_total_other = ff_q_pft_multiple_total_otherhistorystart * S ((S (0)) * pff_history_scale_multiple_total_other) + (0))) /\ (((((exists ff_h_pft_multiple_total_otherhistoryterminal. ff_h_pft_multiple_total_otherhistoryterminal + S (s) = S ((S (n)) * pff_history_scale_multiple_total_other)) /\ exists ff_q_pft_multiple_total_otherhistoryterminal. pff_history_code_multiple_total_other = ff_q_pft_multiple_total_otherhistoryterminal * S ((S (n)) * pff_history_scale_multiple_total_other) + (s))) /\ ((forall pff_trace_index_multiple_total_otherhistorysteps. (exists pfa_gap_multiple_total_otherhistorystepsindex. pfa_gap_multiple_total_otherhistorystepsindex + S (pff_trace_index_multiple_total_otherhistorysteps) = (n)) -> exists pff_trace_before_multiple_total_otherhistorysteps pff_trace_after_multiple_total_otherhistorysteps. ((((exists ff_h_pft_multiple_total_otherhistorystepsbefore. ff_h_pft_multiple_total_otherhistorystepsbefore + S (pff_trace_before_multiple_total_otherhistorysteps) = S ((S (pff_trace_index_multiple_total_otherhistorysteps)) * pff_history_scale_multiple_total_other)) /\ exists ff_q_pft_multiple_total_otherhistorystepsbefore. pff_history_code_multiple_total_other = ff_q_pft_multiple_total_otherhistorystepsbefore * S ((S (pff_trace_index_multiple_total_otherhistorysteps)) * pff_history_scale_multiple_total_other) + (pff_trace_before_multiple_total_otherhistorysteps))) /\ (((((exists ff_h_pft_multiple_total_otherhistorystepsafter. ff_h_pft_multiple_total_otherhistorystepsafter + S (pff_trace_after_multiple_total_otherhistorysteps) = S ((S (S (pff_trace_index_multiple_total_otherhistorysteps))) * pff_history_scale_multiple_total_other)) /\ exists ff_q_pft_multiple_total_otherhistorystepsafter. pff_history_code_multiple_total_other = ff_q_pft_multiple_total_otherhistorystepsafter * S ((S (S (pff_trace_index_multiple_total_otherhistorysteps))) * pff_history_scale_multiple_total_other) + (pff_trace_after_multiple_total_otherhistorysteps))) /\ ((((exists pfa_gap_multiple_total_otherhistorystepsadditionleft. pfa_gap_multiple_total_otherhistorystepsadditionleft + S (pff_trace_before_multiple_total_otherhistorysteps) = (p)) /\ (((exists pfa_gap_multiple_total_otherhistorystepsadditionright. pfa_gap_multiple_total_otherhistorystepsadditionright + S (1) = (p)) /\ ((((exists pfa_gap_multiple_total_otherhistorystepsadditionresultbound. pfa_gap_multiple_total_otherhistorystepsadditionresultbound + S (pff_trace_after_multiple_total_otherhistorysteps) = (p)) /\ ((exists pfa_offset_left_multiple_total_otherhistorystepsadditionresultcongruence pfa_offset_right_multiple_total_otherhistorystepsadditionresultcongruence. ((pff_trace_before_multiple_total_otherhistorysteps) + (1)) + (p) * pfa_offset_left_multiple_total_otherhistorystepsadditionresultcongruence = (pff_trace_after_multiple_total_otherhistorysteps) + (p) * pfa_offset_right_multiple_total_otherhistorystepsadditionresultcongruence)))))))))))))))))))) -> s = r

Constructive proof overview

Generated structural guide

Repeated addition is a total functional computation on every natural length, with an actual beta execution history.

The unchanged tactic script uses 2 declared prerequisites and contains 28 exact native proof lines.

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

Proof neighborhood

Direct dependencies

FP0051 prime_field_unit_trace_exists FP0054 prime_field_unit_multiple_functional

Direct dependents

none

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

28 script commands · 11 reading checkpoints · 2 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 (2)
prime field unit trace existsprime field unit multiple functional

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

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

  1. L1
    intro p
  2. L2
    intro n
  3. L3
    intro hp
02Establish htL4–8

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

  1. L4
    have ht : ∃ b. ∃ c. ∃ r. FpUnitTrace(p,b,c,n,r)Definitions: FpUnitTrace
  2. L5
    specialize prime_field_unit_trace_exists (p)
  3. L6
    specialize prime_field_unit_trace_exists (n)
  4. L7
    apply prime_field_unit_trace_exists
  5. L8
    exact hp
03Separate the logical casesL9–11

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

  1. L9
    cases ht
  2. L10
    cases ht_witness
  3. L11
    cases ht_witness_witness
04Establish hmL12–12

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

  1. L12
    have hm : FpUnitMultiple(p,n,x2)Definitions: FpUnitMultiple
05Construct an explicit witnessL13–14

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

  1. L13
    exists x
  2. L14
    exists x1
06Use earlier factsL15–15

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

  1. L15
    exact ht_witness_witness_witness
07Construct an explicit witnessL16–16

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

  1. L16
    exists x2
08Separate the logical casesL17–17

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

  1. L17
    split
09Use earlier factsL18–18

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

  1. L18
    exact hm
10Fix variables and assumptionsL19–20

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

  1. L19
    intro s
  2. L20
    intro hs
11Use earlier factsL21–28

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

  1. L21
    specialize prime_field_unit_multiple_functional (p)
  2. L22
    specialize prime_field_unit_multiple_functional (n)
  3. L23
    specialize prime_field_unit_multiple_functional (s)
  4. L24
    specialize prime_field_unit_multiple_functional (x2)
  5. L25
    apply prime_field_unit_multiple_functional
  6. L26
    exact hp
  7. L27
    exact hs
  8. L28
    exact hm

Library-wide reading audit

Original exact command ledger · 28 lines
  1. 0001intro p
  2. 0002intro n
  3. 0003intro hp
  4. 0004have ht : exists b c r. (((((exists ff_h_pft_multiple_total_tracestart. ff_h_pft_multiple_total_tracestart + S (0) = S ((S (0)) * c)) /\ exists ff_q_pft_multiple_total_tracestart. b = ff_q_pft_multiple_total_tracestart * S ((S (0)) * c) + (0))) /\ (((((exists ff_h_pft_multiple_total_traceterminal. ff_h_pft_multiple_total_traceterminal + S (r) = S ((S (n)) * c)) /\ exists ff_q_pft_multiple_total_traceterminal. b = ff_q_pft_multiple_total_traceterminal * S ((S (n)) * c) + (r))) /\ ((forall pff_trace_index_multiple_total_tracesteps. (exists pfa_gap_multiple_total_tracestepsindex. pfa_gap_multiple_total_tracestepsindex + S (pff_trace_index_multiple_total_tracesteps) = (n)) -> exists pff_trace_before_multiple_total_tracesteps pff_trace_after_multiple_total_tracesteps. ((((exists ff_h_pft_multiple_total_tracestepsbefore. ff_h_pft_multiple_total_tracestepsbefore + S (pff_trace_before_multiple_total_tracesteps) = S ((S (pff_trace_index_multiple_total_tracesteps)) * c)) /\ exists ff_q_pft_multiple_total_tracestepsbefore. b = ff_q_pft_multiple_total_tracestepsbefore * S ((S (pff_trace_index_multiple_total_tracesteps)) * c) + (pff_trace_before_multiple_total_tracesteps))) /\ (((((exists ff_h_pft_multiple_total_tracestepsafter. ff_h_pft_multiple_total_tracestepsafter + S (pff_trace_after_multiple_total_tracesteps) = S ((S (S (pff_trace_index_multiple_total_tracesteps))) * c)) /\ exists ff_q_pft_multiple_total_tracestepsafter. b = ff_q_pft_multiple_total_tracestepsafter * S ((S (S (pff_trace_index_multiple_total_tracesteps))) * c) + (pff_trace_after_multiple_total_tracesteps))) /\ ((((exists pfa_gap_multiple_total_tracestepsadditionleft. pfa_gap_multiple_total_tracestepsadditionleft + S (pff_trace_before_multiple_total_tracesteps) = (p)) /\ (((exists pfa_gap_multiple_total_tracestepsadditionright. pfa_gap_multiple_total_tracestepsadditionright + S (1) = (p)) /\ ((((exists pfa_gap_multiple_total_tracestepsadditionresultbound. pfa_gap_multiple_total_tracestepsadditionresultbound + S (pff_trace_after_multiple_total_tracesteps) = (p)) /\ ((exists pfa_offset_left_multiple_total_tracestepsadditionresultcongruence pfa_offset_right_multiple_total_tracestepsadditionresultcongruence. ((pff_trace_before_multiple_total_tracesteps) + (1)) + (p) * pfa_offset_left_multiple_total_tracestepsadditionresultcongruence = (pff_trace_after_multiple_total_tracesteps) + (p) * pfa_offset_right_multiple_total_tracestepsadditionresultcongruence)))))))))))))))))))
  5. 0005specialize prime_field_unit_trace_exists (p)
  6. 0006specialize prime_field_unit_trace_exists (n)
  7. 0007apply prime_field_unit_trace_exists
  8. 0008exact hp
  9. 0009cases ht
  10. 0010cases ht_witness
  11. 0011cases ht_witness_witness
  12. 0012have hm : exists pff_history_code_multiple_total_result pff_history_scale_multiple_total_result. (((((exists ff_h_pft_multiple_total_resulthistorystart. ff_h_pft_multiple_total_resulthistorystart + S (0) = S ((S (0)) * pff_history_scale_multiple_total_result)) /\ exists ff_q_pft_multiple_total_resulthistorystart. pff_history_code_multiple_total_result = ff_q_pft_multiple_total_resulthistorystart * S ((S (0)) * pff_history_scale_multiple_total_result) + (0))) /\ (((((exists ff_h_pft_multiple_total_resulthistoryterminal. ff_h_pft_multiple_total_resulthistoryterminal + S (x2) = S ((S (n)) * pff_history_scale_multiple_total_result)) /\ exists ff_q_pft_multiple_total_resulthistoryterminal. pff_history_code_multiple_total_result = ff_q_pft_multiple_total_resulthistoryterminal * S ((S (n)) * pff_history_scale_multiple_total_result) + (x2))) /\ ((forall pff_trace_index_multiple_total_resulthistorysteps. (exists pfa_gap_multiple_total_resulthistorystepsindex. pfa_gap_multiple_total_resulthistorystepsindex + S (pff_trace_index_multiple_total_resulthistorysteps) = (n)) -> exists pff_trace_before_multiple_total_resulthistorysteps pff_trace_after_multiple_total_resulthistorysteps. ((((exists ff_h_pft_multiple_total_resulthistorystepsbefore. ff_h_pft_multiple_total_resulthistorystepsbefore + S (pff_trace_before_multiple_total_resulthistorysteps) = S ((S (pff_trace_index_multiple_total_resulthistorysteps)) * pff_history_scale_multiple_total_result)) /\ exists ff_q_pft_multiple_total_resulthistorystepsbefore. pff_history_code_multiple_total_result = ff_q_pft_multiple_total_resulthistorystepsbefore * S ((S (pff_trace_index_multiple_total_resulthistorysteps)) * pff_history_scale_multiple_total_result) + (pff_trace_before_multiple_total_resulthistorysteps))) /\ (((((exists ff_h_pft_multiple_total_resulthistorystepsafter. ff_h_pft_multiple_total_resulthistorystepsafter + S (pff_trace_after_multiple_total_resulthistorysteps) = S ((S (S (pff_trace_index_multiple_total_resulthistorysteps))) * pff_history_scale_multiple_total_result)) /\ exists ff_q_pft_multiple_total_resulthistorystepsafter. pff_history_code_multiple_total_result = ff_q_pft_multiple_total_resulthistorystepsafter * S ((S (S (pff_trace_index_multiple_total_resulthistorysteps))) * pff_history_scale_multiple_total_result) + (pff_trace_after_multiple_total_resulthistorysteps))) /\ ((((exists pfa_gap_multiple_total_resulthistorystepsadditionleft. pfa_gap_multiple_total_resulthistorystepsadditionleft + S (pff_trace_before_multiple_total_resulthistorysteps) = (p)) /\ (((exists pfa_gap_multiple_total_resulthistorystepsadditionright. pfa_gap_multiple_total_resulthistorystepsadditionright + S (1) = (p)) /\ ((((exists pfa_gap_multiple_total_resulthistorystepsadditionresultbound. pfa_gap_multiple_total_resulthistorystepsadditionresultbound + S (pff_trace_after_multiple_total_resulthistorysteps) = (p)) /\ ((exists pfa_offset_left_multiple_total_resulthistorystepsadditionresultcongruence pfa_offset_right_multiple_total_resulthistorystepsadditionresultcongruence. ((pff_trace_before_multiple_total_resulthistorysteps) + (1)) + (p) * pfa_offset_left_multiple_total_resulthistorystepsadditionresultcongruence = (pff_trace_after_multiple_total_resulthistorysteps) + (p) * pfa_offset_right_multiple_total_resulthistorystepsadditionresultcongruence)))))))))))))))))))
  13. 0013exists x
  14. 0014exists x1
  15. 0015exact ht_witness_witness_witness
  16. 0016exists x2
  17. 0017split
  18. 0018exact hm
  19. 0019intro s
  20. 0020intro hs
  21. 0021specialize prime_field_unit_multiple_functional (p)
  22. 0022specialize prime_field_unit_multiple_functional (n)
  23. 0023specialize prime_field_unit_multiple_functional (s)
  24. 0024specialize prime_field_unit_multiple_functional (x2)
  25. 0025apply prime_field_unit_multiple_functional
  26. 0026exact hp
  27. 0027exact hs
  28. 0028exact hm