AlignmentProtocol
plain-language theorem explainer
AlignmentProtocol packages a measurement Protocol with an optional list of string invariants to enforce cross-agent comparability of RS observables. Researchers defining Alignment maps in the RSNative layer cite it when specifying hygiene conditions for multi-agent data. The declaration is a structure definition with a default empty invariants list and requires no proof.
Claim. An alignment protocol consists of a measurement protocol $P$ together with a list of string invariants $I$ (default empty) that must be preserved under alignment.
background
The module supplies the protocol-level seam for comparing measurements across agents. It records explicit invariants for meaningful comparison but does not solve qualia or ethics issues. Protocol (from Core) is the structure holding a stable name, optional summary, and claim hygiene for extracting an RS observable from a state or trace. Z (from Masses.Anchor and AnchorPolicyCertified) supplies the integer map used by the anchor relation; total (from DiscreteVorticity and RiemannHypothesis.ErrorBudget) sums scalar fields or error components over finite windows; that (from PhiLadderLattice) is a hypothesis structure for phi-ladder Poisson summation.
proof idea
Structure definition with one defaulted field; no lemmas or tactics are applied.
why it matters
It supplies the protocol field to the downstream Alignment structure. The module documentation states that alignment is made explicit data with recorded invariants and that falsifiers are required for hypothesis or scaffold status. It operationalizes the cross-agent seam without invoking T0-T8 forcing steps or the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.