FP003B

prime_field_multiply_grid_value_lookup

Actual quotient/remainder uniqueness identifies both row-major coordinates of a multiply table entry.

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. ∀ a. ∀ b. ∀ v. Lt(b,p) → FpMulGridValue(p,a · p + b,v) → FpMul(p,a,b,v)

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

Definition DAG

FpMul(p,a,b,c) · 1FpMulGridValue(p,i,v) · 1Lt(a,b) · 1

Actual proof prerequisites

division_remainder_unique · checked external prerequisitemul_comm · checked external prerequisite
Original expanded first-order statement 
forall p a b v. (exists pfa_gap_multiplylookup_column. pfa_gap_multiplylookup_column + S (b) = (p)) -> (exists pft_row_multiplylookup_grid pft_column_multiplylookup_grid. (((a*p+b) = pft_row_multiplylookup_grid * (p) + pft_column_multiplylookup_grid) /\ ((((exists pfa_gap_multiplylookup_gridoperationleft. pfa_gap_multiplylookup_gridoperationleft + S (pft_row_multiplylookup_grid) = (p)) /\ (((exists pfa_gap_multiplylookup_gridoperationright. pfa_gap_multiplylookup_gridoperationright + S (pft_column_multiplylookup_grid) = (p)) /\ ((((exists pfa_gap_multiplylookup_gridoperationresultbound. pfa_gap_multiplylookup_gridoperationresultbound + S (v) = (p)) /\ ((exists pfa_offset_left_multiplylookup_gridoperationresultcongruence pfa_offset_right_multiplylookup_gridoperationresultcongruence. ((pft_row_multiplylookup_grid) * (pft_column_multiplylookup_grid)) + (p) * pfa_offset_left_multiplylookup_gridoperationresultcongruence = (v) + (p) * pfa_offset_right_multiplylookup_gridoperationresultcongruence)))))))))))) -> (((exists pfa_gap_multiplylookup_resultleft. pfa_gap_multiplylookup_resultleft + S (a) = (p)) /\ (((exists pfa_gap_multiplylookup_resultright. pfa_gap_multiplylookup_resultright + S (b) = (p)) /\ ((((exists pfa_gap_multiplylookup_resultresultbound. pfa_gap_multiplylookup_resultresultbound + S (v) = (p)) /\ ((exists pfa_offset_left_multiplylookup_resultresultcongruence pfa_offset_right_multiplylookup_resultresultcongruence. ((a) * (b)) + (p) * pfa_offset_left_multiplylookup_resultresultcongruence = (v) + (p) * pfa_offset_right_multiplylookup_resultresultcongruence)))))))))

Complete tactic proof in conservative notation

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

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

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 v
  5. L5
    intro hb
  6. L6
    intro hg
02Separate the logical casesL7–12

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

  1. L7
    cases hg
  2. L8
    cases hg_witness
  3. L9
    cases hg_witness_witness
  4. L10
    cases hg_witness_witness_right
  5. L11
    cases hg_witness_witness_right_right
  6. L12
    cases hg_witness_witness_right_right_right
03Establish heqL13–22

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply division remainder unique.

  1. L13
    have heq : x = a /\ x1 = b
  2. L14
    specialize division_remainder_unique (p)
  3. L15
    specialize division_remainder_unique (a * p + b)
  4. L16
    specialize division_remainder_unique (x)
  5. L17
    specialize division_remainder_unique (x1)
  6. L18
    specialize division_remainder_unique (a)
  7. L19
    specialize division_remainder_unique (b)
  8. L20
    apply division_remainder_unique
  9. L21
    specialize mul_comm x
  10. L22
    specialize mul_comm p
04Calculate and transport equalitiesL23–23

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

  1. L23
    rewrite mul_comm at hg_witness_witness_left
05Use earlier factsL24–27

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

  1. L24
    exact hg_witness_witness_left
  2. L25
    exact hg_witness_witness_right_right_left
  3. L26
    specialize mul_comm a
  4. L27
    specialize mul_comm p
06Calculate and transport equalitiesL28–29

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

  1. L28
    rewrite mul_comm
  2. L29
    refl
07Use earlier factsL30–30

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

  1. L30
    exact hb
08Separate the logical casesL31–31

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

  1. L31
    cases heq
09Calculate and transport equalitiesL32–35

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

  1. L32
    rewrite heq_left at hg_witness_witness_right
  2. L33
    rewrite heq_left at hg_witness_witness_right
  3. L34
    rewrite heq_right at hg_witness_witness_right
  4. L35
    rewrite heq_right at hg_witness_witness_right
10Use earlier factsL36–36

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

  1. L36
    exact hg_witness_witness_right

Library-wide reading audit

Original defined command ledger · 36 lines
  1. 0001intro p
  2. 0002intro a
  3. 0003intro b
  4. 0004intro v
  5. 0005intro hb
  6. 0006intro hg
  7. 0007cases hg
  8. 0008cases hg_witness
  9. 0009cases hg_witness_witness
  10. 0010cases hg_witness_witness_right
  11. 0011cases hg_witness_witness_right_right
  12. 0012cases hg_witness_witness_right_right_right
  13. 0013have heq : x = a /\ x1 = b
  14. 0014specialize division_remainder_unique (p)
  15. 0015specialize division_remainder_unique (a * p + b)
  16. 0016specialize division_remainder_unique (x)
  17. 0017specialize division_remainder_unique (x1)
  18. 0018specialize division_remainder_unique (a)
  19. 0019specialize division_remainder_unique (b)
  20. 0020apply division_remainder_unique
  21. 0021specialize mul_comm x
  22. 0022specialize mul_comm p
  23. 0023rewrite mul_comm at hg_witness_witness_left
  24. 0024exact hg_witness_witness_left
  25. 0025exact hg_witness_witness_right_right_left
  26. 0026specialize mul_comm a
  27. 0027specialize mul_comm p
  28. 0028rewrite mul_comm
  29. 0029refl
  30. 0030exact hb
  31. 0031cases heq
  32. 0032rewrite heq_left at hg_witness_witness_right
  33. 0033rewrite heq_left at hg_witness_witness_right
  34. 0034rewrite heq_right at hg_witness_witness_right
  35. 0035rewrite heq_right at hg_witness_witness_right
  36. 0036exact hg_witness_witness_right