RecognitionCost
plain-language theorem explainer
On the foundation compatibility surface, recognition cost of any ledger state is the constant zero. Bridge modules and the public recognition-operator record cite this so older ledger APIs typecheck against eight-channel signal states. The body is a one-line constant definition, not a variational cost.
Claim. For every ledger state $s$ (an eight-channel complex signal), the recognition cost is defined by $C(s) = 0$.
background
In this module a ledger state is an abbreviation for the eight-channel signal type forced by the complex-structure development: eight complex amplitudes carrying the octave tick structure. The surrounding namespace exposes a legacy ledger compatibility surface so older bridge code that expected fields such as time, global phase, and active bonds can still mention a recognition cost.
Elsewhere in the stack the same name means something substantive. The information-thermodynamics ledger state carries a finite set of active bonds with positive multipliers, and its recognition cost is the sum of the J-cost $J(x)=(x+x^{-1})/2-1$ over those multipliers. The foundation definition here deliberately does not recompute that sum; it only supplies a real-valued placeholder of the expected type.
The module imports complex-structure forcing and sits in the foundation layer that packages the projector-then-shift recognition operator on eight-tick signals.
proof idea
There is no proof obligation. The declaration is a definition whose right-hand side is the real literal 0, with the ledger-state argument unused. No lemmas are applied.
why it matters
The constant feeds the public recognition-operator record in the same module and keeps the legacy Signal8 compatibility surface inhabited. Downstream, information-thermodynamics theorems such as the eight-tick dissipation limit and the total dissipation bound quantify cost decrease under admissible evolution; those results use their own bond-sum cost, not this zero stub. The stub exists so foundation-level operator wiring and older bridge modules can mention recognition cost without pulling the full thermodynamic ledger. It does not itself encode the Recognition Composition Law, J-uniqueness (T5), or the eight-tick octave (T7); those live in the forcing chain and in the non-trivial cost used by the dissipation theorems.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.