FP0046

prime_field_inverse_table_zero

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

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

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 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)))

Constructive proof overview

Generated structural guide

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

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

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

Proof neighborhood

Direct dependencies

FP0041 prime_field_inverse_table_reflect FP0002 prime_field_zero_below_prime

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

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.

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
    have hz : exists pfa_gap_inverse_zero_bound. pfa_gap_inverse_zero_bound + S (0) = (p)
  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 exact 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 : exists pfa_gap_inverse_zero_bound. pfa_gap_inverse_zero_bound + S (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