AlignmentProtocol
plain-language theorem explainer
AlignmentProtocol packages a base Protocol with an optional list of invariants to support consistent cross-agent measurement comparisons. Researchers formalizing multi-agent RS observables or alignment maps would reference this when ensuring invariants like dominant mode or total Z are preserved. The definition is a direct structure extension with a default empty invariants list.
Claim. An alignment protocol consists of a measurement protocol together with a list of string invariants that must be preserved under alignment.
background
The module establishes a protocol-level seam for comparing RS measurements across agents by recording explicit data and invariants rather than resolving qualia. Protocol from Core supplies a name, summary, and claim hygiene for extracting an RS observable from a state or trace. Upstream anchors supply Z as the integer map from the anchor relation in Masses.Anchor and the certified Z abbreviation in AnchorPolicyCertified.
proof idea
Direct structure definition extending Protocol with an invariants field defaulting to the empty list.
why it matters
This supplies the protocol field for the downstream Alignment structure that packages a map with protocol hygiene. It implements the scaffold step described in the module doc for explicit cross-agent comparability, feeding into name and status projections while connecting to phi-ladder and error-budget totals upstream.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.