status
plain-language theorem explainer
The status of an AlignmentProtocol is the status of its embedded Protocol component. Researchers checking cross-agent measurement comparability cite this accessor to determine whether an alignment is proved, conditional, or scaffolded. The definition is a direct field projection equipped with the simp attribute.
Claim. Let $A$ be an alignment protocol. The status of $A$ equals the status of the protocol component of $A$.
background
AlignmentProtocol is a structure that pairs a Protocol with an explicit list of invariants (such as dominant mode or total Z) that must be preserved for cross-agent comparability. The module supplies the protocol-level seam for comparing measurements across agents while recording invariants and requiring falsifiers for hypothesis or scaffold status. Upstream results include the status definition from RSNativeUnits (which records base units, $c=1$, and the phi-ladder) and foundational constants such as one from IntegersFromLogic and active edge count A from IntegrationGap.
proof idea
One-line wrapper that projects the status field from the protocol component of AlignmentProtocol.
why it matters
This definition supports status inspection in downstream results including card_eq_seven (BookerPlotFamily cardinality) and ml_zero_parameter_certificate (M/L derivation with zero external parameters). It completes the alignment scaffold in the Measurement domain, ensuring invariants are recorded for cross-agent use and linking to the requirement for falsifiers when status is hypothesis or scaffold.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.