FP0001

prime_field_mod_of_equal

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

Equality gives genuine balanced modular congruence.

Exact expanded first-order arithmetic statement

forall p a b. a = b -> (exists pfa_offset_left_equal pfa_offset_right_equal. (a) + (p) * pfa_offset_left_equal = (b) + (p) * pfa_offset_right_equal)

Constructive proof overview

Generated structural guide

Equality gives genuine balanced modular congruence.

The unchanged tactic script uses 1 declared prerequisite and contains 8 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

mod_eq_refl Alpha theorem; checked-use authorized

Direct dependents

FP0014 prime_field_add_zero_right FP0016 prime_field_multiply_one_right FP0018 prime_field_multiply_zero_right

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

8 script commands · 3 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.

01Fix variables and assumptionsL1–4

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 heq
02Calculate and transport equalitiesL5–5

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L5
    rewrite heq
03Use earlier factsL6–8

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

  1. L6
    specialize mod_eq_refl (p)
  2. L7
    specialize mod_eq_refl (b)
  3. L8
    apply mod_eq_refl

Library-wide reading audit

Original exact command ledger · 8 lines
  1. 0001intro p
  2. 0002intro a
  3. 0003intro b
  4. 0004intro heq
  5. 0005rewrite heq
  6. 0006specialize mod_eq_refl (p)
  7. 0007specialize mod_eq_refl (b)
  8. 0008apply mod_eq_refl