FP0042

prime_field_add_table_commutative

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

The actual finite add 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_addcomm_table. (exists pfa_gap_addcomm_tableprefix. pfa_gap_addcomm_tableprefix + S (pft_index_addcomm_table) = ((p) * (p))) -> exists pft_value_addcomm_table. (((((exists ff_h_pft_addcomm_tablepointentry. ff_h_pft_addcomm_tablepointentry + S (pft_value_addcomm_table) = S ((S (pft_index_addcomm_table)) * C)) /\ exists ff_q_pft_addcomm_tablepointentry. B = ff_q_pft_addcomm_tablepointentry * S ((S (pft_index_addcomm_table)) * C) + (pft_value_addcomm_table))) /\ ((exists pft_row_addcomm_tablepointvalue pft_column_addcomm_tablepointvalue. (((pft_index_addcomm_table) = pft_row_addcomm_tablepointvalue * (p) + pft_column_addcomm_tablepointvalue) /\ ((((exists pfa_gap_addcomm_tablepointvalueoperationleft. pfa_gap_addcomm_tablepointvalueoperationleft + S (pft_row_addcomm_tablepointvalue) = (p)) /\ (((exists pfa_gap_addcomm_tablepointvalueoperationright. pfa_gap_addcomm_tablepointvalueoperationright + S (pft_column_addcomm_tablepointvalue) = (p)) /\ ((((exists pfa_gap_addcomm_tablepointvalueoperationresultbound. pfa_gap_addcomm_tablepointvalueoperationresultbound + S (pft_value_addcomm_table) = (p)) /\ ((exists pfa_offset_left_addcomm_tablepointvalueoperationresultcongruence pfa_offset_right_addcomm_tablepointvalueoperationresultcongruence. ((pft_row_addcomm_tablepointvalue) + (pft_column_addcomm_tablepointvalue)) + (p) * pfa_offset_left_addcomm_tablepointvalueoperationresultcongruence = (pft_value_addcomm_table) + (p) * pfa_offset_right_addcomm_tablepointvalueoperationresultcongruence)))))))))))))))) -> (exists pfa_gap_addcomm_a. pfa_gap_addcomm_a + S (a) = (p)) -> (exists pfa_gap_addcomm_b. pfa_gap_addcomm_b + S (b) = (p)) -> (((exists ff_h_pft_addcomm_source. ff_h_pft_addcomm_source + S (v) = S ((S (a*p+b)) * C)) /\ exists ff_q_pft_addcomm_source. B = ff_q_pft_addcomm_source * S ((S (a*p+b)) * C) + (v))) -> (((exists ff_h_pft_addcomm_target. ff_h_pft_addcomm_target + S (v) = S ((S (b*p+a)) * C)) /\ exists ff_q_pft_addcomm_target. B = ff_q_pft_addcomm_target * S ((S (b*p+a)) * C) + (v)))

Constructive proof overview

Generated structural guide

The actual finite add 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

FP003A prime_field_add_table_reflect FP000B prime_field_add_commutative FP0039 prime_field_add_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 add table reflectprime field add commutativeprime field add 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_add_table_reflect (p)
  2. L12
    specialize prime_field_add_table_reflect (B)
  3. L13
    specialize prime_field_add_table_reflect (C)
  4. L14
    specialize prime_field_add_table_reflect (b)
  5. L15
    specialize prime_field_add_table_reflect (a)
  6. L16
    specialize prime_field_add_table_reflect (v)
  7. L17
    apply prime_field_add_table_reflect
  8. L18
    exact htable
  9. L19
    specialize prime_field_add_commutative (p)
  10. L20
    specialize prime_field_add_commutative (a)
03Use earlier factsL21–30

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

  1. L21
    specialize prime_field_add_commutative (b)
  2. L22
    specialize prime_field_add_commutative (v)
  3. L23
    apply prime_field_add_commutative
  4. L24
    specialize prime_field_add_table_lookup (p)
  5. L25
    specialize prime_field_add_table_lookup (B)
  6. L26
    specialize prime_field_add_table_lookup (C)
  7. L27
    specialize prime_field_add_table_lookup (a)
  8. L28
    specialize prime_field_add_table_lookup (b)
  9. L29
    specialize prime_field_add_table_lookup (v)
  10. L30
    apply prime_field_add_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_add_table_reflect (p)
  12. 0012specialize prime_field_add_table_reflect (B)
  13. 0013specialize prime_field_add_table_reflect (C)
  14. 0014specialize prime_field_add_table_reflect (b)
  15. 0015specialize prime_field_add_table_reflect (a)
  16. 0016specialize prime_field_add_table_reflect (v)
  17. 0017apply prime_field_add_table_reflect
  18. 0018exact htable
  19. 0019specialize prime_field_add_commutative (p)
  20. 0020specialize prime_field_add_commutative (a)
  21. 0021specialize prime_field_add_commutative (b)
  22. 0022specialize prime_field_add_commutative (v)
  23. 0023apply prime_field_add_commutative
  24. 0024specialize prime_field_add_table_lookup (p)
  25. 0025specialize prime_field_add_table_lookup (B)
  26. 0026specialize prime_field_add_table_lookup (C)
  27. 0027specialize prime_field_add_table_lookup (a)
  28. 0028specialize prime_field_add_table_lookup (b)
  29. 0029specialize prime_field_add_table_lookup (v)
  30. 0030apply prime_field_add_table_lookup
  31. 0031exact htable
  32. 0032exact ha
  33. 0033exact hb
  34. 0034exact hat