Proposition: Interface audit

The product of Definition def:product satisfies C-I1–C-I9 on its declared sector, with the continuity assertions proved in Section sec:continuity.

Proof. For C-I1, every new positive coefficient is a finite sum of inherited admitted graphs or an admitted constant. Classical closure handles $C_0$; old coefficients are inherited. All required admission descendants are included in those statements.

C-I2 is the definition of $C_0$. C-I3 follows from the unchanged restriction

the simultaneous-gluing proof shows this restriction is well defined. C-I4 is the first-stage coefficient assignment.

For C-I5, the only new scalar coefficients are the inherited maps with kernel $U_c$, using the one parameter fixed at the start. Their observation compatibility is recorded below. No new parent is selected during descent or gluing.

C-I6 holds because no old coefficient is changed. C-I7 is respected because no convergence of unchanged sharp approximants is invoked. C-I8 follows from descent to actual spaces and unique gluing on the full declared domain. C-I9 is satisfied by the precisely delimited fixed-support continuity theorem; no actual-stage continuity is asserted.