The rank-eight run for \(h=(1,3,5)\) produces an actual matrix with 25 nonzero Laurent-polynomial entries. Its checked leading and adjacent-correction grades are
It checks normalized lifts, actual matrix identities, native traces 1, and amplified ambient traces \(0,0,1\). The odd \(p=3\) example \(h=(1,2,4)\) has levels \(144,24,4\) and native trace zero.
These finite outputs have contracts, scripts, input pins, results, and execution records in the release. The critical exponents, simplicity, full-character existence, and arbitrary-length statements use the separate ordinary mathematical arguments.
Rebuilding the synchronized readers. From the checkpoint root, run python tools/build_readers.py -{}-output PATH, with PATH outside the checkpoint. The builder stages every style, include and figure dependency, compiles the readers, and resolves the cross-document destinations. The vector plates are preserved source assets. Their Python generator remains available, but figure regeneration is not claimed by this reader build.
Scope
A bounded matrix run cannot establish the universal realization claim. No fresh Lean certificate for Blocks 166–167 is asserted by this guide.