FP0044

prime_field_multiply_table_commutative

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

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

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

Constructive proof overview

Generated structural guide

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

The unchanged tactic script uses 3 declared prerequisites and contains 34 exact native proof lines.

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

Proof neighborhood

Direct dependencies

FP003D prime_field_multiply_table_reflect FP000F prime_field_multiply_commutative FP003C prime_field_multiply_table_lookup

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

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.

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