Exact interfaces for modular autocatalytic reaction networks: amplification prices, catalyst-aware cores, degradation onset, and boundary traces

Modular reasoning about an autocatalytic reaction network is trustworthy only when the environment cannot exploit information that a module summary discarded. We develop, and verify in Lean 4, a layered theory of exact interfaces for finite reaction networks with explicit catalysis. Three foundation results each identify the smallest object that composes. (i) For the maximum amplification factor (MAF), the compositional invariant is not the scalar optimum but the threshold-indexed family of strict species-price certificates; reaction addition, species aggregation, disjoint union, and shared-species coupling act on these price cones by exact set operations, and a two-species example with MAF values $2,2,2,4$ shows that no scalar rule can exist. (ii) Autocatalytic child-selection cores of a network with explicit catalysis are recovered exactly from its ordinary cores: a target core differs from a vertex-contained ordinary anchor by a vertex-disjoint pack of alternating matching-exchange paths, and an executable enumerator built on this fact returns precisely the child-selection cores without traversing the ambient edge powerset. (iii) For species-specific degradation at diluted onset, the growth, critical, and extinction regions of the degradation orthant are exactly the projective images $d\lessgtr Av/v$ of positive compositions $v$, with the Perron mode constructed rather than assumed, and a finite actuator support can extinguish the system precisely when the unactuated principal block already admits a strict extinction certificate.

Interactions between factors of a source network are then organised on a typed factor–species incidence graph: amplification synergy forces a signed cycle, fixed-threshold feasibility is exactly a disjunction over factors on an incidence forest, and degradation loads of independent branches add at a shared root, so that two individually extinct branches can jointly grow. Finally we define the exact boundary trace of a module, prove that trace equality is precisely indistinguishability by every boundary context, characterise when a coarser summary is safe (injectivity on the realized traces), and give an exact junction-tree message theorem in which running intersection together with a scope-extensionality condition repairs otherwise invalid existential witness gluing; separator width bounds message arity. The MAF price-cone profile, a thermodynamic interval interface, and a finite Type-II passive tail are exact interfaces; the scalar MAF and two thermodynamic verdict vectors are certified information losses. Every stated result is compiled with warnings treated as errors in a frozen Lean 4.30 / Mathlib environment.