FP002E

prime_field_zero_extended_inverse_functional

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

The explicit zero convention and genuine nonzero inverses together define a functional total table operation.

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 a b c. (((exists pfa_gap_zero_inverse_firstinput. pfa_gap_zero_inverse_firstinput + S (a) = (p)) /\ (((exists pfa_gap_zero_inverse_firstoutput. pfa_gap_zero_inverse_firstoutput + S (b) = (p)) /\ ((((a) = 0 /\ (b) = 0) \/ (((~((a) = 0)) /\ ((((exists pfa_gap_zero_inverse_firstnonzeromultiplicationleft. pfa_gap_zero_inverse_firstnonzeromultiplicationleft + S (a) = (p)) /\ (((exists pfa_gap_zero_inverse_firstnonzeromultiplicationright. pfa_gap_zero_inverse_firstnonzeromultiplicationright + S (b) = (p)) /\ ((((exists pfa_gap_zero_inverse_firstnonzeromultiplicationresultbound. pfa_gap_zero_inverse_firstnonzeromultiplicationresultbound + S (1) = (p)) /\ ((exists pfa_offset_left_zero_inverse_firstnonzeromultiplicationresultcongruence pfa_offset_right_zero_inverse_firstnonzeromultiplicationresultcongruence. ((a) * (b)) + (p) * pfa_offset_left_zero_inverse_firstnonzeromultiplicationresultcongruence = (1) + (p) * pfa_offset_right_zero_inverse_firstnonzeromultiplicationresultcongruence)))))))))))))))))) -> (((exists pfa_gap_zero_inverse_secondinput. pfa_gap_zero_inverse_secondinput + S (a) = (p)) /\ (((exists pfa_gap_zero_inverse_secondoutput. pfa_gap_zero_inverse_secondoutput + S (c) = (p)) /\ ((((a) = 0 /\ (c) = 0) \/ (((~((a) = 0)) /\ ((((exists pfa_gap_zero_inverse_secondnonzeromultiplicationleft. pfa_gap_zero_inverse_secondnonzeromultiplicationleft + S (a) = (p)) /\ (((exists pfa_gap_zero_inverse_secondnonzeromultiplicationright. pfa_gap_zero_inverse_secondnonzeromultiplicationright + S (c) = (p)) /\ ((((exists pfa_gap_zero_inverse_secondnonzeromultiplicationresultbound. pfa_gap_zero_inverse_secondnonzeromultiplicationresultbound + S (1) = (p)) /\ ((exists pfa_offset_left_zero_inverse_secondnonzeromultiplicationresultcongruence pfa_offset_right_zero_inverse_secondnonzeromultiplicationresultcongruence. ((a) * (c)) + (p) * pfa_offset_left_zero_inverse_secondnonzeromultiplicationresultcongruence = (1) + (p) * pfa_offset_right_zero_inverse_secondnonzeromultiplicationresultcongruence)))))))))))))))))) -> b = c

Constructive proof overview

Generated structural guide

The explicit zero convention and genuine nonzero inverses together define a functional total table operation.

The unchanged tactic script uses 1 declared prerequisite and contains 35 exact native proof lines.

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

Proof neighborhood

Direct dependencies

FP001F prime_field_inverse_functional

Direct dependents

FP0041 prime_field_inverse_table_reflect

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

35 script commands · 10 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.

Named ingredients (1)
prime field inverse functional
01Fix variables and assumptionsL1–6

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

  1. L1
    intro p
  2. L2
    intro a
  3. L3
    intro b
  4. L4
    intro c
  5. L5
    intro hb
  6. L6
    intro hc
02Separate the logical casesL7–14

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

  1. L7
    cases hb
  2. L8
    cases hb_right
  3. L9
    cases hc
  4. L10
    cases hc_right
  5. L11
    cases hb_right_right
  6. L12
    cases hb_right_right_left
  7. L13
    cases hc_right_right
  8. L14
    cases hc_right_right_left
03Calculate and transport equalitiesL15–15

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

  1. L15
    trans 0
04Use earlier factsL16–16

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

  1. L16
    exact hb_right_right_left_right
05Calculate and transport equalitiesL17–17

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

  1. L17
    symm
06Use earlier factsL18–18

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

  1. L18
    exact hc_right_right_left_right
07Separate the logical casesL19–20

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

  1. L19
    exfalso
  2. L20
    cases hc_right_right_right
08Use earlier factsL21–22

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

  1. L21
    apply hc_right_right_right_left
  2. L22
    exact hb_right_right_left_left
09Separate the logical casesL23–26

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

  1. L23
    cases hc_right_right
  2. L24
    cases hc_right_right_left
  3. L25
    exfalso
  4. L26
    cases hb_right_right_right
10Use earlier factsL27–35

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

  1. L27
    apply hb_right_right_right_left
  2. L28
    exact hc_right_right_left_left
  3. L29
    specialize prime_field_inverse_functional (p)
  4. L30
    specialize prime_field_inverse_functional (a)
  5. L31
    specialize prime_field_inverse_functional (b)
  6. L32
    specialize prime_field_inverse_functional (c)
  7. L33
    apply prime_field_inverse_functional
  8. L34
    exact hb_right_right_right
  9. L35
    exact hc_right_right_right

Library-wide reading audit

Original exact command ledger · 35 lines
  1. 0001intro p
  2. 0002intro a
  3. 0003intro b
  4. 0004intro c
  5. 0005intro hb
  6. 0006intro hc
  7. 0007cases hb
  8. 0008cases hb_right
  9. 0009cases hc
  10. 0010cases hc_right
  11. 0011cases hb_right_right
  12. 0012cases hb_right_right_left
  13. 0013cases hc_right_right
  14. 0014cases hc_right_right_left
  15. 0015trans 0
  16. 0016exact hb_right_right_left_right
  17. 0017symm
  18. 0018exact hc_right_right_left_right
  19. 0019exfalso
  20. 0020cases hc_right_right_right
  21. 0021apply hc_right_right_right_left
  22. 0022exact hb_right_right_left_left
  23. 0023cases hc_right_right
  24. 0024cases hc_right_right_left
  25. 0025exfalso
  26. 0026cases hb_right_right_right
  27. 0027apply hb_right_right_right_left
  28. 0028exact hc_right_right_left_left
  29. 0029specialize prime_field_inverse_functional (p)
  30. 0030specialize prime_field_inverse_functional (a)
  31. 0031specialize prime_field_inverse_functional (b)
  32. 0032specialize prime_field_inverse_functional (c)
  33. 0033apply prime_field_inverse_functional
  34. 0034exact hb_right_right_right
  35. 0035exact hc_right_right_right