FP002E

prime_field_zero_extended_inverse_functional

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 explicit zero convention and genuine nonzero inverses together define a functional total table operation.

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. ∀ a. ∀ b. ∀ c. FpZeroExtendedInv(p,a,b) → FpZeroExtendedInv(p,a,c) → b = c

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

Definition DAG

FpZeroExtendedInv(p,a,b) · 2

Actual proof prerequisites

prime_field_inverse_functional
Original expanded first-order 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

Complete tactic proof in conservative notation

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

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.

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