TH0001

hensel_predecessor_annihilates_residue

The predecessor of every positive modulus gives a witnessed subtraction-free negative residue.

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

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 original first-admission records.

Historical partial components only: this chapter proves exact natural polynomial Taylor remainders, bounded corrections, and one-step divisibility lifts. G095 is now closed in the separate Alpha-v27 hensel-lifting branch for integer polynomials, unrestricted input roots, unique canonical representatives, and every positive prime power. Full G095 proof · Alpha v27

Exact theorem in conservative defined notation

∀ k. ∀ q. ModEq(S k,q + k · q,0)

Every linked abbreviation expands hygienically to the identical original native formula.

Definition DAG

ModEq(m,a,b) · 1

Actual proof prerequisites

mod_eq_predecessor_cancel · checked external prerequisitezero_add · checked external prerequisite
Original expanded first-order statement 
forall k q. (exists hgcrt_mod_left_pth_negative hgcrt_mod_right_pth_negative. (q + k * q) + (S k) * hgcrt_mod_left_pth_negative = 0 + (S k) * hgcrt_mod_right_pth_negative)

Complete unchanged native tactic proof

All 9 lines are the exact independently kernel-checked original script.

Read the argument

Proof checkpoints

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

Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.

01Fix variables and assumptionsL1–2

Work with arbitrary variables or the premises of the current implication.

  1. L1
    intro k
  2. L2
    intro q
02Use earlier factsL3–5

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

  1. L3
    specialize mod_eq_predecessor_cancel k
  2. L4
    specialize mod_eq_predecessor_cancel 0
  3. L5
    specialize mod_eq_predecessor_cancel q
03Establish hzL6–9

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply zero add.

  1. L6
    have hz : 0 + q = q
  2. L7
    apply zero_add
  3. L8
    rewrite hz at mod_eq_predecessor_cancel
  4. L9
    exact mod_eq_predecessor_cancel

Library-wide reading audit

Original defined command ledger · 9 lines
  1. 0001intro k
  2. 0002intro q
  3. 0003specialize mod_eq_predecessor_cancel k
  4. 0004specialize mod_eq_predecessor_cancel 0
  5. 0005specialize mod_eq_predecessor_cancel q
  6. 0006have hz : 0 + q = q
  7. 0007apply zero_add
  8. 0008rewrite hz at mod_eq_predecessor_cancel
  9. 0009exact mod_eq_predecessor_cancel