FP0042

prime_field_add_table_commutative

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.

Public research checkpoint: original HA and independently compiled Lean verified; not Alpha-enrolled, no Alpha checked-use authority; not Stable

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

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.

Public research checkpoint: original HA and independently compiled Lean verified; not Alpha-enrolled, no Alpha checked-use authority; 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. The literal dependency-closed bundle is checked by original HA and the independently compiled Lean verifier. Public delivery grants no Alpha checked-use authority or 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