Reflective Non-Exhaustion: Certification, Realization, Fibers, and Obstruction

Central claim. We state and defend a summit-level claim from a machine-checked program in Lean 4: canonical certification does not, in general, exhaust realization. When a formal architecture has a bare certification layer, an enriched realization layer, and a sound comparison map: E B, collapse at the bare carrier may coexist with nontrivial realized structure above it; the residue is organized by non-injective comparison, nontrivial fibers, sections, and obstruction laws. Suite support. The claim is supported by six completed kinds of discharge: the internal origin theorem in Infinity Compression; external transfer across twelve benchmark families; an algebraic obstruction theorem for group extensions; an arithmetic bridge through embedding problems; a topological discharge via