# Update 2026-07-13: census + PSD certificate now KERNEL-CHECKED in Lean

Two of the three legs of delta_3 = 117/2192 are now verified by the Lean kernel:

1. UPPER (census): `Research/Census548.lean` + `Census548Norm.lean` — the 548-bead
   periodic word's finite residue-pair census, score_eq depends on [propext] only.
2. LOWER (PSD certificate): `Research/PSDCheck548.lean` — both sectors of the
   548-cell dual certificate are symmetric diagonally dominant (sym_sector_dd,
   anti_sector_dd), verified by kernel-reduced integer arithmetic.

To re-verify: cd lean && lake build   (uses the pinned toolchain/manifest)

Remaining for full end-to-end: the discrete-to-continuum reduction (in progress).
