AgentId
plain-language theorem explainer
Agent identifiers in the recognition ledger are plain natural numbers. Anyone wiring bonds, channels, or multi-agent ledger state cites this type alias. It is a bare abbreviation of ℕ with no proof obligations.
Claim. An agent identifier is a natural number: $\mathrm{AgentId} := \mathbb{N}$.
background
The RecognitionOperator module sets up the discrete ledger that carries recognition dynamics: signals, bonds, channels, and a global phase. Agents are the endpoints of bonds; each bond links an ordered pair of agents.
Sibling aliases in the same block name the other ledger atoms (bond ids, eight-tick signals, ledger state fields). The module imports ComplexStructureForcing, so this sits inside the foundation layer that forces complex structure and the recognition operator, not inside the mass or coupling ladders.
No upstream lemmas are required: the alias is pure naming.
proof idea
No proof. The declaration is a one-line type abbreviation equating the agent-id sort with the natural numbers.
why it matters
Gives a stable name to the agent sort used by bond_agents, which (for now) returns a dummy pair of agent ids from a ledger state and bond id. Downstream ledger constructions that track who is bonded to whom depend on this alias rather than raw ℕ, so the multi-agent reading of the ledger stays explicit.
It does not itself touch T0–T8, the RCL, or the phi-ladder; it is infrastructure for the recognition operator’s state type.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.