LocallyAdditive
plain-language theorem explainer
Local additivity is the explicit hypothesis that a size-indexed real cost on bounded complexes splits under disjoint union: the cost of A ⊔ C equals the sum of the costs. Gap-2 discrimination (D2) cites it to rule out log|Aut| as such a cost. The definition is a plain Prop, forced because the raw letter-cost API allows ambient-dependent charges.
Claim. A size-indexed real-valued cost $h$ on bounded complexes is locally additive when, for all bounds $B,B'$ and complexes $A,C$ of those sizes, $h(B+B', A \sqcup C) = h(B,A) + h(B',C)$.
background
Gap 2 (label erasure Jacobian, lane C4) separates two gates. D1 is the statability gate: a relabeling-invariant labeled weight pushes forward with Jacobian factor involving $1/|\mathrm{Aut}|$, so the Gibbs weight is the size-only piece of that Jacobian rather than a substrate assumption. D2 is the discrimination gate: one must show that no locally additive real cost can equal $\log|\mathrm{Aut}|$ on every complex.
The raw letter-cost interface admits ambient-dependent charges, so additivity under disjoint union is not automatic and must be named. Bounded complexes are the directed/ordered carriers used throughout the gap modules; disjoint union $A \sqcup C$ raises the size index to $B+B'$. Automorphisms are incidence-preserving index bijections on that directed carrier (component swap is included; edge reversal is not).
Upstream cost notions (J-cost on recognition events, multiplicative-recognizer derived cost, rung-coarsen sums) supply the ambient language of real costs, but the locality predicate itself is purely algebraic on the complex category.
proof idea
Definitional: the body is the universal quantification stating equality of $h$ on the disjoint union with the sum of the separate values. No lemmas are applied; no tactics run. Downstream theorems either assume the predicate (D2) or discharge it by simp on the zero cost.
why it matters
This predicate is the explicit locality hypothesis required by D2. The parent theorem no_local_additive_cost_realizes_log_aut uses it to prove that no such $h$ can realize $\log|\mathrm{Aut}|$ at every complex: the witness $A = \mathrm{dust},1$ gives $|\mathrm{Aut}(A \sqcup A)| = 2 \cdot |\mathrm{Aut},A|^2$ by the $S_2$ wreath factor, so $\log|\mathrm{Aut}(A \sqcup A)| = \log 2$ while $2\log|\mathrm{Aut},A| = 0$.
A fugacity-robust corollary follows: no disjoint-multiplicative numerator times count fugacities can convert the gauge weight into uniform-on-iso-classes, because the $S_2$ factor cannot be absorbed. The hostile probe locallyAdditive_is_explicit confirms the predicate is non-vacuous (the zero cost satisfies it).
In the module's scoped headline, D2 is gate G2 toward flag 8; the module does not close flag 8. Local additivity is the precise cut that separates genuine local costs from the non-additive automorphism logarithm that appears in the erasure Jacobian.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.