FP0001

prime_field_mod_of_equal

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

Equality gives genuine balanced modular congruence.

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

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

Proof neighborhood

Direct dependencies

mod_eq_refl Stable 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. 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

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