FP0056

prime_field_characteristic_exact

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.

The first positive number of additions of the actual identity one that returns zero is exactly p, including p=2.

Public research checkpoint: original HA and independently compiled Lean verified; not Alpha-enrolled, no Alpha checked-use authority; not Stable

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. Prime(p) → FpCharacteristic(p)

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

Definition DAG

FpCharacteristic(p) · 1Prime(p) · 1

Actual proof prerequisites

prime_field_unit_multiple_from_residueprime_field_residue_modulus_zeroprime_field_unit_multiple_residueprime_field_positive_below_modulus_not_zero
Original expanded first-order statement 
forall p. (~((p) = 1) /\ forall pfa_factor_left_characteristic_domain pfa_factor_right_characteristic_domain. (p) = pfa_factor_left_characteristic_domain * pfa_factor_right_characteristic_domain -> pfa_factor_left_characteristic_domain = 1 \/ pfa_factor_right_characteristic_domain = 1) -> (((exists pff_history_code_characteristic_exactmodulus pff_history_scale_characteristic_exactmodulus. (((((exists ff_h_pft_characteristic_exactmodulushistorystart. ff_h_pft_characteristic_exactmodulushistorystart + S (0) = S ((S (0)) * pff_history_scale_characteristic_exactmodulus)) /\ exists ff_q_pft_characteristic_exactmodulushistorystart. pff_history_code_characteristic_exactmodulus = ff_q_pft_characteristic_exactmodulushistorystart * S ((S (0)) * pff_history_scale_characteristic_exactmodulus) + (0))) /\ (((((exists ff_h_pft_characteristic_exactmodulushistoryterminal. ff_h_pft_characteristic_exactmodulushistoryterminal + S (0) = S ((S (p)) * pff_history_scale_characteristic_exactmodulus)) /\ exists ff_q_pft_characteristic_exactmodulushistoryterminal. pff_history_code_characteristic_exactmodulus = ff_q_pft_characteristic_exactmodulushistoryterminal * S ((S (p)) * pff_history_scale_characteristic_exactmodulus) + (0))) /\ ((forall pff_trace_index_characteristic_exactmodulushistorysteps. (exists pfa_gap_characteristic_exactmodulushistorystepsindex. pfa_gap_characteristic_exactmodulushistorystepsindex + S (pff_trace_index_characteristic_exactmodulushistorysteps) = (p)) -> exists pff_trace_before_characteristic_exactmodulushistorysteps pff_trace_after_characteristic_exactmodulushistorysteps. ((((exists ff_h_pft_characteristic_exactmodulushistorystepsbefore. ff_h_pft_characteristic_exactmodulushistorystepsbefore + S (pff_trace_before_characteristic_exactmodulushistorysteps) = S ((S (pff_trace_index_characteristic_exactmodulushistorysteps)) * pff_history_scale_characteristic_exactmodulus)) /\ exists ff_q_pft_characteristic_exactmodulushistorystepsbefore. pff_history_code_characteristic_exactmodulus = ff_q_pft_characteristic_exactmodulushistorystepsbefore * S ((S (pff_trace_index_characteristic_exactmodulushistorysteps)) * pff_history_scale_characteristic_exactmodulus) + (pff_trace_before_characteristic_exactmodulushistorysteps))) /\ (((((exists ff_h_pft_characteristic_exactmodulushistorystepsafter. ff_h_pft_characteristic_exactmodulushistorystepsafter + S (pff_trace_after_characteristic_exactmodulushistorysteps) = S ((S (S (pff_trace_index_characteristic_exactmodulushistorysteps))) * pff_history_scale_characteristic_exactmodulus)) /\ exists ff_q_pft_characteristic_exactmodulushistorystepsafter. pff_history_code_characteristic_exactmodulus = ff_q_pft_characteristic_exactmodulushistorystepsafter * S ((S (S (pff_trace_index_characteristic_exactmodulushistorysteps))) * pff_history_scale_characteristic_exactmodulus) + (pff_trace_after_characteristic_exactmodulushistorysteps))) /\ ((((exists pfa_gap_characteristic_exactmodulushistorystepsadditionleft. pfa_gap_characteristic_exactmodulushistorystepsadditionleft + S (pff_trace_before_characteristic_exactmodulushistorysteps) = (p)) /\ (((exists pfa_gap_characteristic_exactmodulushistorystepsadditionright. pfa_gap_characteristic_exactmodulushistorystepsadditionright + S (1) = (p)) /\ ((((exists pfa_gap_characteristic_exactmodulushistorystepsadditionresultbound. pfa_gap_characteristic_exactmodulushistorystepsadditionresultbound + S (pff_trace_after_characteristic_exactmodulushistorysteps) = (p)) /\ ((exists pfa_offset_left_characteristic_exactmodulushistorystepsadditionresultcongruence pfa_offset_right_characteristic_exactmodulushistorystepsadditionresultcongruence. ((pff_trace_before_characteristic_exactmodulushistorysteps) + (1)) + (p) * pfa_offset_left_characteristic_exactmodulushistorystepsadditionresultcongruence = (pff_trace_after_characteristic_exactmodulushistorysteps) + (p) * pfa_offset_right_characteristic_exactmodulushistorystepsadditionresultcongruence)))))))))))))))))))) /\ ((forall pff_smaller_positive_characteristic_exact. (exists pfa_gap_characteristic_exactstrict. pfa_gap_characteristic_exactstrict + S (pff_smaller_positive_characteristic_exact) = (p)) -> ~(pff_smaller_positive_characteristic_exact = 0) -> ~(exists pff_history_code_characteristic_exactsmaller pff_history_scale_characteristic_exactsmaller. (((((exists ff_h_pft_characteristic_exactsmallerhistorystart. ff_h_pft_characteristic_exactsmallerhistorystart + S (0) = S ((S (0)) * pff_history_scale_characteristic_exactsmaller)) /\ exists ff_q_pft_characteristic_exactsmallerhistorystart. pff_history_code_characteristic_exactsmaller = ff_q_pft_characteristic_exactsmallerhistorystart * S ((S (0)) * pff_history_scale_characteristic_exactsmaller) + (0))) /\ (((((exists ff_h_pft_characteristic_exactsmallerhistoryterminal. ff_h_pft_characteristic_exactsmallerhistoryterminal + S (0) = S ((S (pff_smaller_positive_characteristic_exact)) * pff_history_scale_characteristic_exactsmaller)) /\ exists ff_q_pft_characteristic_exactsmallerhistoryterminal. pff_history_code_characteristic_exactsmaller = ff_q_pft_characteristic_exactsmallerhistoryterminal * S ((S (pff_smaller_positive_characteristic_exact)) * pff_history_scale_characteristic_exactsmaller) + (0))) /\ ((forall pff_trace_index_characteristic_exactsmallerhistorysteps. (exists pfa_gap_characteristic_exactsmallerhistorystepsindex. pfa_gap_characteristic_exactsmallerhistorystepsindex + S (pff_trace_index_characteristic_exactsmallerhistorysteps) = (pff_smaller_positive_characteristic_exact)) -> exists pff_trace_before_characteristic_exactsmallerhistorysteps pff_trace_after_characteristic_exactsmallerhistorysteps. ((((exists ff_h_pft_characteristic_exactsmallerhistorystepsbefore. ff_h_pft_characteristic_exactsmallerhistorystepsbefore + S (pff_trace_before_characteristic_exactsmallerhistorysteps) = S ((S (pff_trace_index_characteristic_exactsmallerhistorysteps)) * pff_history_scale_characteristic_exactsmaller)) /\ exists ff_q_pft_characteristic_exactsmallerhistorystepsbefore. pff_history_code_characteristic_exactsmaller = ff_q_pft_characteristic_exactsmallerhistorystepsbefore * S ((S (pff_trace_index_characteristic_exactsmallerhistorysteps)) * pff_history_scale_characteristic_exactsmaller) + (pff_trace_before_characteristic_exactsmallerhistorysteps))) /\ (((((exists ff_h_pft_characteristic_exactsmallerhistorystepsafter. ff_h_pft_characteristic_exactsmallerhistorystepsafter + S (pff_trace_after_characteristic_exactsmallerhistorysteps) = S ((S (S (pff_trace_index_characteristic_exactsmallerhistorysteps))) * pff_history_scale_characteristic_exactsmaller)) /\ exists ff_q_pft_characteristic_exactsmallerhistorystepsafter. pff_history_code_characteristic_exactsmaller = ff_q_pft_characteristic_exactsmallerhistorystepsafter * S ((S (S (pff_trace_index_characteristic_exactsmallerhistorysteps))) * pff_history_scale_characteristic_exactsmaller) + (pff_trace_after_characteristic_exactsmallerhistorysteps))) /\ ((((exists pfa_gap_characteristic_exactsmallerhistorystepsadditionleft. pfa_gap_characteristic_exactsmallerhistorystepsadditionleft + S (pff_trace_before_characteristic_exactsmallerhistorysteps) = (p)) /\ (((exists pfa_gap_characteristic_exactsmallerhistorystepsadditionright. pfa_gap_characteristic_exactsmallerhistorystepsadditionright + S (1) = (p)) /\ ((((exists pfa_gap_characteristic_exactsmallerhistorystepsadditionresultbound. pfa_gap_characteristic_exactsmallerhistorystepsadditionresultbound + S (pff_trace_after_characteristic_exactsmallerhistorysteps) = (p)) /\ ((exists pfa_offset_left_characteristic_exactsmallerhistorystepsadditionresultcongruence pfa_offset_right_characteristic_exactsmallerhistorystepsadditionresultcongruence. ((pff_trace_before_characteristic_exactsmallerhistorysteps) + (1)) + (p) * pfa_offset_left_characteristic_exactsmallerhistorystepsadditionresultcongruence = (pff_trace_after_characteristic_exactsmallerhistorysteps) + (p) * pfa_offset_right_characteristic_exactsmallerhistorystepsadditionresultcongruence))))))))))))))))))))))))

Complete tactic proof in conservative notation

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

26 script commands · 6 reading checkpoints · 0 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 (4)
prime field unit multiple from residueprime field residue modulus zeroprime field positive below modulus not zeroprime field unit multiple residue
01Fix variables and assumptionsL1–2

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

  1. L1
    intro p
  2. L2
    intro hp
02Separate the logical casesL3–3

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

  1. L3
    split
03Use earlier factsL4–11

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

  1. L4
    specialize prime_field_unit_multiple_from_residue (p)
  2. L5
    specialize prime_field_unit_multiple_from_residue (p)
  3. L6
    specialize prime_field_unit_multiple_from_residue (0)
  4. L7
    apply prime_field_unit_multiple_from_residue
  5. L8
    exact hp
  6. L9
    specialize prime_field_residue_modulus_zero (p)
  7. L10
    apply prime_field_residue_modulus_zero
  8. L11
    exact hp
04Fix variables and assumptionsL12–15

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

  1. L12
    intro n
  2. L13
    intro hn
  3. L14
    intro hpositive
  4. L15
    intro hm
05Use earlier factsL16–25

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

  1. L16
    specialize prime_field_positive_below_modulus_not_zero (p)
  2. L17
    specialize prime_field_positive_below_modulus_not_zero (n)
  3. L18
    apply prime_field_positive_below_modulus_not_zero
  4. L19
    exact hn
  5. L20
    exact hpositive
  6. L21
    specialize prime_field_unit_multiple_residue (p)
  7. L22
    specialize prime_field_unit_multiple_residue (n)
  8. L23
    specialize prime_field_unit_multiple_residue (0)
  9. L24
    apply prime_field_unit_multiple_residue
  10. L25
    exact hp
06Use earlier factsL26–26

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

  1. L26
    exact hm

Library-wide reading audit

Original defined command ledger · 26 lines
  1. 0001intro p
  2. 0002intro hp
  3. 0003split
  4. 0004specialize prime_field_unit_multiple_from_residue (p)
  5. 0005specialize prime_field_unit_multiple_from_residue (p)
  6. 0006specialize prime_field_unit_multiple_from_residue (0)
  7. 0007apply prime_field_unit_multiple_from_residue
  8. 0008exact hp
  9. 0009specialize prime_field_residue_modulus_zero (p)
  10. 0010apply prime_field_residue_modulus_zero
  11. 0011exact hp
  12. 0012intro n
  13. 0013intro hn
  14. 0014intro hpositive
  15. 0015intro hm
  16. 0016specialize prime_field_positive_below_modulus_not_zero (p)
  17. 0017specialize prime_field_positive_below_modulus_not_zero (n)
  18. 0018apply prime_field_positive_below_modulus_not_zero
  19. 0019exact hn
  20. 0020exact hpositive
  21. 0021specialize prime_field_unit_multiple_residue (p)
  22. 0022specialize prime_field_unit_multiple_residue (n)
  23. 0023specialize prime_field_unit_multiple_residue (0)
  24. 0024apply prime_field_unit_multiple_residue
  25. 0025exact hp
  26. 0026exact hm