Theorem: IX-Free-2 release

Relative to Assumptions ass:carrier–ass:parent, the prescribed degree-four coefficients descend to actual functionals. All declared new coefficients glue with the locked first stages and the unchanged full old product on the named domain $D_{\mathrm{decl}}$.

For every fixed real common parent $c$, the resulting truncated partial product satisfies C-I1–C-I9. Its two associations of $B_f,W_g,B_{f^{\prime }}$ agree through order ${\hslash }^3$, and it has partial-product reversal and actual-functional presentation independence. Moreover,

Fixed-support test-family continuity holds on the named domains. Actual-stage continuity is not asserted.

The release outcome is Constructed.

Proof. Theorem thm:pinjective evaluates both degree-four relation kernels. Theorem thm:degree4 proves descent.

Lemma lem:sharpcharge supplies the explicit sharp charge witness, while Proposition prop:zerocharge establishes the comparison zero-charge classes. Theorem thm:separation proves all required separations. Proposition prop:newdirect handles the entire new domain, including the locked first stages. Theorem thm:oldgluing handles its whole-sum old overlap. Corollary cor:cglue evaluates the gluing parameter set.

Definition def:product gives one partial product, and Proposition prop:interfaces audits the copied contract. Theorem thm:coherence, Theorem thm:reversal, Proposition prop:presentation, and Theorem thm:F9a prove the remaining assertions.