Rigidify Before Quotient: Boundary Semantics and Coassociativity in the Connes–Kreimer Hopf Algebra

This record contains the manuscript: Rigidify Before Quotient: Boundary Semantics and Coassociativity in the Connes–Kreimer Hopf Algebra. The Connes–Kreimer coproduct is usually formulated after boundary identities and auxiliary presentations have been forgotten, although its coassociativity proof must reconstruct insertion and contraction data that those quotients may erase. This manuscript isolates that mismatch in Lean 4. On a flat graph carrier, edge and external-leg retargeting are shown to be non-injective already for singleton multisets. A boundary-resolved graph carrier with persistent edge and leg identities is then introduced. Under identity uniqueness, resolved retargeting is injective on ambient submultisets, while forgetting the persistent identities recovers exactly the flat collapse maps. The retained boundary data support an outer-forest double-sum reindex without the two flat boundary-reconstruction interfaces and a native resolved coproduct on a canonical externally saturated proper-forest carrier (W''). Under explicitly stated finiteness, invariance, contraction-preservation, contraction-reflection, power-counting, and representation premises, generator-wise coassociativity is proved. External-leg saturation and the Parent/de-contraction data are constructed rather than assumed. Separately, generator-wise local nilpotency of the reduced convolution operator proves the right antipode identity and yields the conditional flat Hopf-algebra packaging. All cited Lean declarations are sorry-free, admit-free, and free of project-specific axioms. The manuscript includes an exact declaration-level axiom audit, a minimal executable import path, theorem-to-file tables, frozen source anchors, and a reproducibility protocol. The result is specific to the Connes–Kreimer graph construction. It does not claim a general quotient-descent theorem, and realization of the remaining divergence interface for a concrete quantum field theory is a separate theorem. Formalization and reproducibility archive:https://doi.org/10.5281/zenodo.21543358 Source repository:https://github.com/miosync-masa/ck-hopf-formalization