active_bonds
plain-language theorem explainer
The active-bond set of a ledger state is defined as the empty finite set of bond identifiers. Downstream bond positivity and recognition-cost sums therefore range over nothing in this foundation layer. Anyone wiring RecognitionOperator states into the information/thermodynamics ledger cites this stub. The body is a constant empty Finset, ignoring the state argument.
Claim. For every ledger state $s$, the set of active bonds is the empty finite set $\emptyset \subseteq \mathbb{N}$ (bond identifiers).
background
In Foundation.RecognitionOperator, a ledger state is abbreviated to Signal8 (the eight-channel recognition signal forced by the octave structure). Bond identifiers are plain natural numbers. The operator layer exposes a small surface of bond data: which bonds are active, their multipliers, and positivity of those multipliers on the active set.
A richer ledger appears in Information.Thermodynamics: there a state carries an explicit finite set of active bonds, a multiplier map $\mathbb{N}\to\mathbb{R}$, and a positivity witness on that set. Total recognition cost is the sum of the $J$-cost over active bonds, and reciprocity skew sums absolute log-imbalances on the same set. The present definition is the foundation-side placeholder for that active-bond field: it always returns empty, so sums and membership proofs are vacuous until a nonempty model is supplied.
proof idea
No proof. The definition is the constant empty finite set of bond ids, with the ledger-state argument unused. Downstream bond_pos discharges positivity by simplifying the companion multiplier definition on that empty membership hypothesis.
why it matters
This stub is the active-bond hook that bond_pos and the information-thermodynamics stack read. RecognitionCost, reciprocity_skew, landauer_bound_holds, and the scaffold hypothesis H_ThermodynamicsVerified all quantify or sum over active bonds; with the empty set they hold vacuously and keep the Landauer/$J$-cost interface type-correct.
In the Recognition framework the $J$-cost (T5 uniqueness, RCL) lower-bounds information dissipation. The thermodynamic bound claims $J(m)\ge(\log m)^2/2$ on each active multiplier. Filling this definition with a genuine finite support is what turns those vacuous theorems into contentful ledger thermodynamics. Until then it only closes the API between the eight-tick foundation state and the information ledger.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.