name
plain-language theorem explainer
The definition projects the name string from the protocol component of an alignment protocol structure. Researchers formalizing cross-agent measurement comparability in Recognition Science cite it to access protocol identifiers during invariant checks. The body is a direct field accessor equipped with the simp attribute for automatic rewriting.
Claim. For an alignment protocol $A$ formed from a base protocol together with a list of invariants that must be preserved for cross-agent comparability, let $name(A)$ denote the name string of the base protocol.
background
The module scaffolds explicit data structures for comparing measurements across agents without resolving qualia or ethics. An alignment protocol consists of a base protocol plus an optional list of invariants (for example dominant mode or total Z) that must remain unchanged under alignment operations. Upstream results supply the active edge count per tick (equal to 1) from both IntegrationGap and Masses.Anchor, together with the actualization operator that selects the minimal J-cost configuration from the possibility set.
proof idea
The definition is a one-line field projection that returns the name component of the protocol field inside the alignment protocol structure. The simp attribute registers it for automatic simplification in later proofs.
why it matters
This accessor supports the protocol-level seam for cross-agent alignment by exposing the identifier needed for invariant preservation. It belongs to the scaffold that records explicit data and invariants before any hypothesis or theorem status is assigned, consistent with the framework requirement that falsifiers accompany non-proved claims. No downstream uses are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.