FP0044

prime_field_multiply_table_commutative

The actual finite multiply table is symmetric under exchanging row and column.

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. ∀ a. ∀ b. ∀ v. FpMulPrefix(p,B,C,p · p) → Lt(a,p) → Lt(b,p) → BetaAt(B,C,a · p + b,v) → BetaAt(B,C,b · p + a,v)

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

Definition DAG

FpMulPrefix(p,b,c,l) · 1Lt(a,b) · 2BetaAt(b,c,i,x) · 2

Actual proof prerequisites

prime_field_multiply_table_reflectprime_field_multiply_commutativeprime_field_multiply_table_lookup
Original expanded first-order statement 
forall p B C a b v. (forall pft_index_multiplycomm_table. (exists pfa_gap_multiplycomm_tableprefix. pfa_gap_multiplycomm_tableprefix + S (pft_index_multiplycomm_table) = ((p) * (p))) -> exists pft_value_multiplycomm_table. (((((exists ff_h_pft_multiplycomm_tablepointentry. ff_h_pft_multiplycomm_tablepointentry + S (pft_value_multiplycomm_table) = S ((S (pft_index_multiplycomm_table)) * C)) /\ exists ff_q_pft_multiplycomm_tablepointentry. B = ff_q_pft_multiplycomm_tablepointentry * S ((S (pft_index_multiplycomm_table)) * C) + (pft_value_multiplycomm_table))) /\ ((exists pft_row_multiplycomm_tablepointvalue pft_column_multiplycomm_tablepointvalue. (((pft_index_multiplycomm_table) = pft_row_multiplycomm_tablepointvalue * (p) + pft_column_multiplycomm_tablepointvalue) /\ ((((exists pfa_gap_multiplycomm_tablepointvalueoperationleft. pfa_gap_multiplycomm_tablepointvalueoperationleft + S (pft_row_multiplycomm_tablepointvalue) = (p)) /\ (((exists pfa_gap_multiplycomm_tablepointvalueoperationright. pfa_gap_multiplycomm_tablepointvalueoperationright + S (pft_column_multiplycomm_tablepointvalue) = (p)) /\ ((((exists pfa_gap_multiplycomm_tablepointvalueoperationresultbound. pfa_gap_multiplycomm_tablepointvalueoperationresultbound + S (pft_value_multiplycomm_table) = (p)) /\ ((exists pfa_offset_left_multiplycomm_tablepointvalueoperationresultcongruence pfa_offset_right_multiplycomm_tablepointvalueoperationresultcongruence. ((pft_row_multiplycomm_tablepointvalue) * (pft_column_multiplycomm_tablepointvalue)) + (p) * pfa_offset_left_multiplycomm_tablepointvalueoperationresultcongruence = (pft_value_multiplycomm_table) + (p) * pfa_offset_right_multiplycomm_tablepointvalueoperationresultcongruence)))))))))))))))) -> (exists pfa_gap_multiplycomm_a. pfa_gap_multiplycomm_a + S (a) = (p)) -> (exists pfa_gap_multiplycomm_b. pfa_gap_multiplycomm_b + S (b) = (p)) -> (((exists ff_h_pft_multiplycomm_source. ff_h_pft_multiplycomm_source + S (v) = S ((S (a*p+b)) * C)) /\ exists ff_q_pft_multiplycomm_source. B = ff_q_pft_multiplycomm_source * S ((S (a*p+b)) * C) + (v))) -> (((exists ff_h_pft_multiplycomm_target. ff_h_pft_multiplycomm_target + S (v) = S ((S (b*p+a)) * C)) /\ exists ff_q_pft_multiplycomm_target. B = ff_q_pft_multiplycomm_target * S ((S (b*p+a)) * C) + (v)))

Complete tactic proof in conservative notation

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

34 script commands · 4 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 (3)
prime field multiply table reflectprime field multiply commutativeprime field multiply table lookup
01Fix variables and assumptionsL1–10

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 a
  5. L5
    intro b
  6. L6
    intro v
  7. L7
    intro htable
  8. L8
    intro ha
  9. L9
    intro hb
  10. L10
    intro hat
02Use earlier factsL11–20

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

  1. L11
    specialize prime_field_multiply_table_reflect (p)
  2. L12
    specialize prime_field_multiply_table_reflect (B)
  3. L13
    specialize prime_field_multiply_table_reflect (C)
  4. L14
    specialize prime_field_multiply_table_reflect (b)
  5. L15
    specialize prime_field_multiply_table_reflect (a)
  6. L16
    specialize prime_field_multiply_table_reflect (v)
  7. L17
    apply prime_field_multiply_table_reflect
  8. L18
    exact htable
  9. L19
    specialize prime_field_multiply_commutative (p)
  10. L20
    specialize prime_field_multiply_commutative (a)
03Use earlier factsL21–30

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

  1. L21
    specialize prime_field_multiply_commutative (b)
  2. L22
    specialize prime_field_multiply_commutative (v)
  3. L23
    apply prime_field_multiply_commutative
  4. L24
    specialize prime_field_multiply_table_lookup (p)
  5. L25
    specialize prime_field_multiply_table_lookup (B)
  6. L26
    specialize prime_field_multiply_table_lookup (C)
  7. L27
    specialize prime_field_multiply_table_lookup (a)
  8. L28
    specialize prime_field_multiply_table_lookup (b)
  9. L29
    specialize prime_field_multiply_table_lookup (v)
  10. L30
    apply prime_field_multiply_table_lookup
04Use earlier factsL31–34

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

  1. L31
    exact htable
  2. L32
    exact ha
  3. L33
    exact hb
  4. L34
    exact hat

Library-wide reading audit

Original defined command ledger · 34 lines
  1. 0001intro p
  2. 0002intro B
  3. 0003intro C
  4. 0004intro a
  5. 0005intro b
  6. 0006intro v
  7. 0007intro htable
  8. 0008intro ha
  9. 0009intro hb
  10. 0010intro hat
  11. 0011specialize prime_field_multiply_table_reflect (p)
  12. 0012specialize prime_field_multiply_table_reflect (B)
  13. 0013specialize prime_field_multiply_table_reflect (C)
  14. 0014specialize prime_field_multiply_table_reflect (b)
  15. 0015specialize prime_field_multiply_table_reflect (a)
  16. 0016specialize prime_field_multiply_table_reflect (v)
  17. 0017apply prime_field_multiply_table_reflect
  18. 0018exact htable
  19. 0019specialize prime_field_multiply_commutative (p)
  20. 0020specialize prime_field_multiply_commutative (a)
  21. 0021specialize prime_field_multiply_commutative (b)
  22. 0022specialize prime_field_multiply_commutative (v)
  23. 0023apply prime_field_multiply_commutative
  24. 0024specialize prime_field_multiply_table_lookup (p)
  25. 0025specialize prime_field_multiply_table_lookup (B)
  26. 0026specialize prime_field_multiply_table_lookup (C)
  27. 0027specialize prime_field_multiply_table_lookup (a)
  28. 0028specialize prime_field_multiply_table_lookup (b)
  29. 0029specialize prime_field_multiply_table_lookup (v)
  30. 0030apply prime_field_multiply_table_lookup
  31. 0031exact htable
  32. 0032exact ha
  33. 0033exact hb
  34. 0034exact hat