PFP X: Exact Host Checking of Model Verdicts on Small Finite Algebraic Challenges - Lattice Holonomy and Six Formal-Mathematics Pilots

PFP X: Exact Host Checking of Model Verdicts on Small Finite Algebraic Challenges - Lattice Holonomy and Six Formal-Mathematics Pilots This methods preprint separates model proposals from exact host checks on finite algebraic objects. It supplies a complete Python checker for finite-group connections on open and periodic square lattices, with explicit edge orientation, group validation, plaquette products, torus cycle holonomies and certificate obligations. Identity-link skipping is a gauge-dependent optimization. Fresh replay of five retained C017 cases reproduces the expected verdicts and checks all 15 retained solution records: 13 parsed certificates and two parser-error wrappers, with 10 accepted and 5 rejected overall. Ten further historical responses retain labels and reasons only. Six formal-mathematics pilots report three models on ten cases per cell; the package preserves the original reports and recounts their acceptance flags offline. The author's published annotation marks answer-bearing identifiers in 36 of 60 reconstructable panel cases, and a prior checker replay shows that constant refusal passes all ten in two original harnesses. These counts do not measure unaided performance or identify a causal prompt effect. The package includes source provenance, negative controls, a 24-question study companion with an instructor key and executable capstone, and one Lean identity-link lemma. The current review records executed checks separately from historical reports; the pinned Lean build and fresh C045–C050 checker execution were not run.