so
plain-language theorem explainer
Meta-claim in the T5 cost-uniqueness helpers: once the defect functional is fixed to J, it cannot be smuggled back in without breaking the build. Cited only as a formalization invariant around the J-cost module, not as a physics identity. No proof body is present; the declaration is effectively a named guardrail note.
Claim. After the defect functional is identified with the J-cost on positive reals, that identification is locked: reintroducing a distinct defect would make the development fail to build.
background
The module supplies functional-equation lemmas for the T5 cost-uniqueness argument in the forcing chain. T5 forces the unique symmetric cost $J(x)=(x+x^{-1})/2-1$ (equivalently $\cosh(\log x)-1$) on the positive reals.
Upstream, the defect functional is defined to equal $J$ for positive $x$, and vanishes at unity. Sibling material in this file treats the reciprocal-symmetric class $G$, the cosh-addition identity, and d'Alembert-type doubling lemmas that pin $J$ uniquely.
The local setting is therefore not a new physical law but bookkeeping around that uniqueness: the cost side of the chain must stay free of an independent defect once $J$ is forced.
proof idea
No proof body is supplied (zero lines). The declaration reads as a one-line named assertion rather than a tactic or term proof. Upstream edges resolve only to the defect definition and unrelated token matches (without, the), so there is no lemma chain to walk. Treat it as a documentation-level guard, not an algebraic reduction.
why it matters
In the Recognition forcing chain, T5 J-uniqueness is the step that removes freedom in the cost. A build-level claim that the defect cannot be reintroduced protects that step from silent regression while downstream action, Hamiltonian, and $\phi$-ladder developments consume $J$.
Reported consumers (conjugate momentum, Hamilton equations from EL, standard Lagrangian/EL, $\phi$-powers, astrophysical J-minimization) are almost certainly token-level so matches in docstrings, not real mathematical dependents. The declaration earns a page only as a formalization invariant next to the T5 helpers, not as a cited physics lemma. It does not itself advance T6--T8 ($\phi$, eight-tick, $D=3$).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.