FP0038

prime_field_add_grid_value_lookup

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

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

Exact expanded first-order arithmetic statement

forall p a b v. (exists pfa_gap_addlookup_column. pfa_gap_addlookup_column + S (b) = (p)) -> (exists pft_row_addlookup_grid pft_column_addlookup_grid. (((a*p+b) = pft_row_addlookup_grid * (p) + pft_column_addlookup_grid) /\ ((((exists pfa_gap_addlookup_gridoperationleft. pfa_gap_addlookup_gridoperationleft + S (pft_row_addlookup_grid) = (p)) /\ (((exists pfa_gap_addlookup_gridoperationright. pfa_gap_addlookup_gridoperationright + S (pft_column_addlookup_grid) = (p)) /\ ((((exists pfa_gap_addlookup_gridoperationresultbound. pfa_gap_addlookup_gridoperationresultbound + S (v) = (p)) /\ ((exists pfa_offset_left_addlookup_gridoperationresultcongruence pfa_offset_right_addlookup_gridoperationresultcongruence. ((pft_row_addlookup_grid) + (pft_column_addlookup_grid)) + (p) * pfa_offset_left_addlookup_gridoperationresultcongruence = (v) + (p) * pfa_offset_right_addlookup_gridoperationresultcongruence)))))))))))) -> (((exists pfa_gap_addlookup_resultleft. pfa_gap_addlookup_resultleft + S (a) = (p)) /\ (((exists pfa_gap_addlookup_resultright. pfa_gap_addlookup_resultright + S (b) = (p)) /\ ((((exists pfa_gap_addlookup_resultresultbound. pfa_gap_addlookup_resultresultbound + S (v) = (p)) /\ ((exists pfa_offset_left_addlookup_resultresultcongruence pfa_offset_right_addlookup_resultresultcongruence. ((a) + (b)) + (p) * pfa_offset_left_addlookup_resultresultcongruence = (v) + (p) * pfa_offset_right_addlookup_resultresultcongruence)))))))))

Constructive proof overview

Generated structural guide

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

The unchanged tactic script uses 2 declared prerequisites and contains 36 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

division_remainder_unique Alpha theorem; checked-use authorized mul_comm Alpha theorem; checked-use authorized

Direct dependents

FP0039 prime_field_add_table_lookup

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

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.

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