FP004B

prime_field_enumeration_is_bijection

The actual p-entry enumeration is bounded, injective and onto every canonical field representative.

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. ∀ b. ∀ c. IdentityMatrixSelector(b,c,p) → FpCardinality(p,b,c)

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

Definition DAG

IdentityMatrixSelector(b,c,l) · 1FpCardinality(p,b,c) · 1

Actual proof prerequisites

prime_field_enumeration_value
Original expanded first-order statement 
forall p b c. (forall pff_enumeration_index_bijection_source. (exists pfa_gap_bijection_sourcebound. pfa_gap_bijection_sourcebound + S (pff_enumeration_index_bijection_source) = (p)) -> (((exists ff_h_pft_bijection_sourceentry. ff_h_pft_bijection_sourceentry + S (pff_enumeration_index_bijection_source) = S ((S (pff_enumeration_index_bijection_source)) * c)) /\ exists ff_q_pft_bijection_sourceentry. b = ff_q_pft_bijection_sourceentry * S ((S (pff_enumeration_index_bijection_source)) * c) + (pff_enumeration_index_bijection_source)))) -> (((forall pff_enumeration_index_bijection_resultenumeration. (exists pfa_gap_bijection_resultenumerationbound. pfa_gap_bijection_resultenumerationbound + S (pff_enumeration_index_bijection_resultenumeration) = (p)) -> (((exists ff_h_pft_bijection_resultenumerationentry. ff_h_pft_bijection_resultenumerationentry + S (pff_enumeration_index_bijection_resultenumeration) = S ((S (pff_enumeration_index_bijection_resultenumeration)) * c)) /\ exists ff_q_pft_bijection_resultenumerationentry. b = ff_q_pft_bijection_resultenumerationentry * S ((S (pff_enumeration_index_bijection_resultenumeration)) * c) + (pff_enumeration_index_bijection_resultenumeration)))) /\ (((forall pff_cardinality_i_bijection_result pff_cardinality_a_bijection_result. (exists pfa_gap_bijection_resultbounded_index. pfa_gap_bijection_resultbounded_index + S (pff_cardinality_i_bijection_result) = (p)) -> (((exists ff_h_pft_bijection_resultbounded_entry. ff_h_pft_bijection_resultbounded_entry + S (pff_cardinality_a_bijection_result) = S ((S (pff_cardinality_i_bijection_result)) * c)) /\ exists ff_q_pft_bijection_resultbounded_entry. b = ff_q_pft_bijection_resultbounded_entry * S ((S (pff_cardinality_i_bijection_result)) * c) + (pff_cardinality_a_bijection_result))) -> (exists pfa_gap_bijection_resultbounded_value. pfa_gap_bijection_resultbounded_value + S (pff_cardinality_a_bijection_result) = (p))) /\ (((forall pff_cardinality_i_bijection_result pff_cardinality_j_bijection_result pff_cardinality_a_bijection_result. (exists pfa_gap_bijection_resultinjective_i. pfa_gap_bijection_resultinjective_i + S (pff_cardinality_i_bijection_result) = (p)) -> (exists pfa_gap_bijection_resultinjective_j. pfa_gap_bijection_resultinjective_j + S (pff_cardinality_j_bijection_result) = (p)) -> (((exists ff_h_pft_bijection_resultinjective_first. ff_h_pft_bijection_resultinjective_first + S (pff_cardinality_a_bijection_result) = S ((S (pff_cardinality_i_bijection_result)) * c)) /\ exists ff_q_pft_bijection_resultinjective_first. b = ff_q_pft_bijection_resultinjective_first * S ((S (pff_cardinality_i_bijection_result)) * c) + (pff_cardinality_a_bijection_result))) -> (((exists ff_h_pft_bijection_resultinjective_second. ff_h_pft_bijection_resultinjective_second + S (pff_cardinality_a_bijection_result) = S ((S (pff_cardinality_j_bijection_result)) * c)) /\ exists ff_q_pft_bijection_resultinjective_second. b = ff_q_pft_bijection_resultinjective_second * S ((S (pff_cardinality_j_bijection_result)) * c) + (pff_cardinality_a_bijection_result))) -> pff_cardinality_i_bijection_result = pff_cardinality_j_bijection_result) /\ ((forall pff_cardinality_a_bijection_result. (exists pfa_gap_bijection_resultsurjective_value. pfa_gap_bijection_resultsurjective_value + S (pff_cardinality_a_bijection_result) = (p)) -> exists pff_cardinality_i_bijection_result. (exists pfa_gap_bijection_resultsurjective_index. pfa_gap_bijection_resultsurjective_index + S (pff_cardinality_i_bijection_result) = (p)) /\ (((exists ff_h_pft_bijection_resultsurjective_entry. ff_h_pft_bijection_resultsurjective_entry + S (pff_cardinality_a_bijection_result) = S ((S (pff_cardinality_i_bijection_result)) * c)) /\ exists ff_q_pft_bijection_resultsurjective_entry. b = ff_q_pft_bijection_resultsurjective_entry * S ((S (pff_cardinality_i_bijection_result)) * c) + (pff_cardinality_a_bijection_result)))))))))))

Complete tactic proof in conservative notation

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

63 script commands · 18 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.

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 (1)
prime field enumeration value
01Fix variables and assumptionsL1–4

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 henum
02Separate the logical casesL5–5

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

  1. L5
    split
03Use earlier factsL6–6

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

  1. L6
    exact henum
04Separate the logical casesL7–7

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

  1. L7
    split
05Fix variables and assumptionsL8–11

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

  1. L8
    intro i
  2. L9
    intro a
  3. L10
    intro hi
  4. L11
    intro hat
06Establish heqL12–21

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

  1. L12
    have heq : a = i
  2. L13
    specialize prime_field_enumeration_value (p)
  3. L14
    specialize prime_field_enumeration_value (b)
  4. L15
    specialize prime_field_enumeration_value (c)
  5. L16
    specialize prime_field_enumeration_value (i)
  6. L17
    specialize prime_field_enumeration_value (a)
  7. L18
    apply prime_field_enumeration_value
  8. L19
    exact henum
  9. L20
    exact hi
  10. L21
    exact hat
07Calculate and transport equalitiesL22–22

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

  1. L22
    rewrite heq
08Use earlier factsL23–23

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

  1. L23
    exact hi
09Separate the logical casesL24–24

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

  1. L24
    split
10Fix variables and assumptionsL25–31

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

  1. L25
    intro i
  2. L26
    intro j
  3. L27
    intro a
  4. L28
    intro hi
  5. L29
    intro hj
  6. L30
    intro hfirst
  7. L31
    intro hsecond
11Establish hleftL32–41

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

  1. L32
    have hleft : a = i
  2. L33
    specialize prime_field_enumeration_value (p)
  3. L34
    specialize prime_field_enumeration_value (b)
  4. L35
    specialize prime_field_enumeration_value (c)
  5. L36
    specialize prime_field_enumeration_value (i)
  6. L37
    specialize prime_field_enumeration_value (a)
  7. L38
    apply prime_field_enumeration_value
  8. L39
    exact henum
  9. L40
    exact hi
  10. L41
    exact hfirst
12Establish hrightL42–51

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

  1. L42
    have hright : a = j
  2. L43
    specialize prime_field_enumeration_value (p)
  3. L44
    specialize prime_field_enumeration_value (b)
  4. L45
    specialize prime_field_enumeration_value (c)
  5. L46
    specialize prime_field_enumeration_value (j)
  6. L47
    specialize prime_field_enumeration_value (a)
  7. L48
    apply prime_field_enumeration_value
  8. L49
    exact henum
  9. L50
    exact hj
  10. L51
    exact hsecond
13Calculate and transport equalitiesL52–53

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

  1. L52
    trans a
  2. L53
    symm
14Use earlier factsL54–55

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

  1. L54
    exact hleft
  2. L55
    exact hright
15Fix variables and assumptionsL56–57

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

  1. L56
    intro a
  2. L57
    intro ha
16Construct an explicit witnessL58–58

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

  1. L58
    exists a
17Separate the logical casesL59–59

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

  1. L59
    split
18Use earlier factsL60–63

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

  1. L60
    exact ha
  2. L61
    specialize henum (a)
  3. L62
    apply henum
  4. L63
    exact ha

Library-wide reading audit

Original defined command ledger · 63 lines
  1. 0001intro p
  2. 0002intro b
  3. 0003intro c
  4. 0004intro henum
  5. 0005split
  6. 0006exact henum
  7. 0007split
  8. 0008intro i
  9. 0009intro a
  10. 0010intro hi
  11. 0011intro hat
  12. 0012have heq : a = i
  13. 0013specialize prime_field_enumeration_value (p)
  14. 0014specialize prime_field_enumeration_value (b)
  15. 0015specialize prime_field_enumeration_value (c)
  16. 0016specialize prime_field_enumeration_value (i)
  17. 0017specialize prime_field_enumeration_value (a)
  18. 0018apply prime_field_enumeration_value
  19. 0019exact henum
  20. 0020exact hi
  21. 0021exact hat
  22. 0022rewrite heq
  23. 0023exact hi
  24. 0024split
  25. 0025intro i
  26. 0026intro j
  27. 0027intro a
  28. 0028intro hi
  29. 0029intro hj
  30. 0030intro hfirst
  31. 0031intro hsecond
  32. 0032have hleft : a = i
  33. 0033specialize prime_field_enumeration_value (p)
  34. 0034specialize prime_field_enumeration_value (b)
  35. 0035specialize prime_field_enumeration_value (c)
  36. 0036specialize prime_field_enumeration_value (i)
  37. 0037specialize prime_field_enumeration_value (a)
  38. 0038apply prime_field_enumeration_value
  39. 0039exact henum
  40. 0040exact hi
  41. 0041exact hfirst
  42. 0042have hright : a = j
  43. 0043specialize prime_field_enumeration_value (p)
  44. 0044specialize prime_field_enumeration_value (b)
  45. 0045specialize prime_field_enumeration_value (c)
  46. 0046specialize prime_field_enumeration_value (j)
  47. 0047specialize prime_field_enumeration_value (a)
  48. 0048apply prime_field_enumeration_value
  49. 0049exact henum
  50. 0050exact hj
  51. 0051exact hsecond
  52. 0052trans a
  53. 0053symm
  54. 0054exact hleft
  55. 0055exact hright
  56. 0056intro a
  57. 0057intro ha
  58. 0058exists a
  59. 0059split
  60. 0060exact ha
  61. 0061specialize henum (a)
  62. 0062apply henum
  63. 0063exact ha