BondId
plain-language theorem explainer
Bond identifiers are plain natural numbers used to index pairwise recognition links in a ledger state. Anyone working with active bonds, multipliers, agent pairs, or signed log flow cites this type alias. The declaration is a one-line abbreviation with no proof content.
Claim. A bond identifier is an element of $\mathbb{N}$.
background
In the Recognition Operator module, a ledger state packages the discrete data of a recognition step: time, Z-patterns, global phase, channels, and the collection of active bonds between agents. Bonds are the elementary pairwise links that carry multipliers, reciprocity skew, and signed log flow.
BondId is the index type for those links. It sits beside the sibling alias for agent identifiers and the LedgerState structure. Downstream fields such as the (currently empty) active-bond set, bond multipliers, and the map from a bond to its two agents are all typed over this identifier.
proof idea
Pure type abbreviation: BondId is defined to be ℕ. No lemmas, tactics, or obligations.
why it matters
This alias is the common index for every bond-level field on LedgerState: the active-bond finset, bond multipliers and their positivity certificate, the agent-pair map, reciprocity skew, and signed log flow. Those stubs are the scaffolding on which a nontrivial recognition operator (bond creation, cost updates, reciprocity) will be written. In the broader RS foundation the operator is meant to realize the discrete recognition step that sits under the forcing chain and the eight-tick structure; a stable bond index is the first bookkeeping step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.