FP0046

prime_field_inverse_table_zero

The totalized inverse table really stores zero at zero, without claiming zero has an inverse.

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. Prime(p) → FpInvPrefix(p,B,C,p) → BetaAt(B,C,0,0)

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

Definition DAG

FpInvPrefix(p,b,c,l) · 1Lt(a,b) · 1Prime(p) · 1BetaAt(b,c,i,x) · 1

Actual proof prerequisites

prime_field_inverse_table_reflectprime_field_zero_below_prime
Original expanded first-order statement 
forall p B C. (~((p) = 1) /\ forall pfa_factor_left_inverse_zero_domain pfa_factor_right_inverse_zero_domain. (p) = pfa_factor_left_inverse_zero_domain * pfa_factor_right_inverse_zero_domain -> pfa_factor_left_inverse_zero_domain = 1 \/ pfa_factor_right_inverse_zero_domain = 1) -> (forall pft_index_inverse_zero_table. (exists pfa_gap_inverse_zero_tableprefix. pfa_gap_inverse_zero_tableprefix + S (pft_index_inverse_zero_table) = (p)) -> exists pft_value_inverse_zero_table. (((((exists ff_h_pft_inverse_zero_tablepointentry. ff_h_pft_inverse_zero_tablepointentry + S (pft_value_inverse_zero_table) = S ((S (pft_index_inverse_zero_table)) * C)) /\ exists ff_q_pft_inverse_zero_tablepointentry. B = ff_q_pft_inverse_zero_tablepointentry * S ((S (pft_index_inverse_zero_table)) * C) + (pft_value_inverse_zero_table))) /\ ((((exists pfa_gap_inverse_zero_tablepointvalueinput. pfa_gap_inverse_zero_tablepointvalueinput + S (pft_index_inverse_zero_table) = (p)) /\ (((exists pfa_gap_inverse_zero_tablepointvalueoutput. pfa_gap_inverse_zero_tablepointvalueoutput + S (pft_value_inverse_zero_table) = (p)) /\ ((((pft_index_inverse_zero_table) = 0 /\ (pft_value_inverse_zero_table) = 0) \/ (((~((pft_index_inverse_zero_table) = 0)) /\ ((((exists pfa_gap_inverse_zero_tablepointvaluenonzeromultiplicationleft. pfa_gap_inverse_zero_tablepointvaluenonzeromultiplicationleft + S (pft_index_inverse_zero_table) = (p)) /\ (((exists pfa_gap_inverse_zero_tablepointvaluenonzeromultiplicationright. pfa_gap_inverse_zero_tablepointvaluenonzeromultiplicationright + S (pft_value_inverse_zero_table) = (p)) /\ ((((exists pfa_gap_inverse_zero_tablepointvaluenonzeromultiplicationresultbound. pfa_gap_inverse_zero_tablepointvaluenonzeromultiplicationresultbound + S (1) = (p)) /\ ((exists pfa_offset_left_inverse_zero_tablepointvaluenonzeromultiplicationresultcongruence pfa_offset_right_inverse_zero_tablepointvaluenonzeromultiplicationresultcongruence. ((pft_index_inverse_zero_table) * (pft_value_inverse_zero_table)) + (p) * pfa_offset_left_inverse_zero_tablepointvaluenonzeromultiplicationresultcongruence = (1) + (p) * pfa_offset_right_inverse_zero_tablepointvaluenonzeromultiplicationresultcongruence)))))))))))))))))))))) -> (((exists ff_h_pft_inverse_zero_entry. ff_h_pft_inverse_zero_entry + S (0) = S ((S (0)) * C)) /\ exists ff_q_pft_inverse_zero_entry. B = ff_q_pft_inverse_zero_entry * S ((S (0)) * C) + (0)))

Complete tactic proof in conservative notation

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

24 script commands · 9 reading checkpoints · 1 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 inverse table reflectprime field zero below prime
01Fix variables and assumptionsL1–5

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 hp
  5. L5
    intro htable
02Use earlier factsL6–12

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

  1. L6
    specialize prime_field_inverse_table_reflect (p)
  2. L7
    specialize prime_field_inverse_table_reflect (B)
  3. L8
    specialize prime_field_inverse_table_reflect (C)
  4. L9
    specialize prime_field_inverse_table_reflect (0)
  5. L10
    specialize prime_field_inverse_table_reflect (0)
  6. L11
    apply prime_field_inverse_table_reflect
  7. L12
    exact htable
03Establish hzL13–16

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

  1. L13
  2. L14
    specialize prime_field_zero_below_prime (p)
  3. L15
    apply prime_field_zero_below_prime
  4. L16
    exact hp
04Separate the logical casesL17–17

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

  1. L17
    split
05Use earlier factsL18–18

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

  1. L18
    exact hz
06Separate the logical casesL19–19

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

  1. L19
    split
07Use earlier factsL20–20

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

  1. L20
    exact hz
08Separate the logical casesL21–22

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

  1. L21
    left
  2. L22
    split
09Calculate and transport equalitiesL23–24

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

  1. L23
    refl
  2. L24
    refl

Library-wide reading audit

Original defined command ledger · 24 lines
  1. 0001intro p
  2. 0002intro B
  3. 0003intro C
  4. 0004intro hp
  5. 0005intro htable
  6. 0006specialize prime_field_inverse_table_reflect (p)
  7. 0007specialize prime_field_inverse_table_reflect (B)
  8. 0008specialize prime_field_inverse_table_reflect (C)
  9. 0009specialize prime_field_inverse_table_reflect (0)
  10. 0010specialize prime_field_inverse_table_reflect (0)
  11. 0011apply prime_field_inverse_table_reflect
  12. 0012exact htable
  13. 0013have hz : Lt(0,p)
  14. 0014specialize prime_field_zero_below_prime (p)
  15. 0015apply prime_field_zero_below_prime
  16. 0016exact hp
  17. 0017split
  18. 0018exact hz
  19. 0019split
  20. 0020exact hz
  21. 0021left
  22. 0022split
  23. 0023refl
  24. 0024refl