FP0055

prime_field_unit_multiple_exists_unique

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

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. ∀ n. Prime(p) → ∃ x. FpUnitMultiple(p,n,x) ∧ (∀ y. FpUnitMultiple(p,n,y) → y = x)

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

Definition DAG

FpUnitTrace(p,b,c,n,r) · 1FpUnitMultiple(p,n,r) · 3Prime(p) · 1

Actual proof prerequisites

prime_field_unit_trace_existsprime_field_unit_multiple_functional
Original expanded first-order 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

Complete tactic proof in conservative notation

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

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.

Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.

Named ingredients (2)
prime field unit trace existsprime field unit multiple functional
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(p,b,c,n,r)Original native command in the exact edition
  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(p,n,x2)Original native command in the exact edition
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 defined command ledger · 28 lines
  1. 0001intro p
  2. 0002intro n
  3. 0003intro hp
  4. 0004have ht : ∃ b. ∃ c. ∃ r. FpUnitTrace(p,b,c,n,r)
  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 : FpUnitMultiple(p,n,x2)
  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