pith. machine review for the scientific record. sign in
def definition def or abbrev high

status

show as:
view Lean formalization →

The status definition extracts the protocol status field from an AlignmentProtocol by direct delegation to its embedded Protocol. Downstream modules in cosmology, chemistry, and aesthetics cite it to retrieve status without unpacking the structure. It is implemented as a one-line field projection.

claimFor an alignment protocol $A$, the status is defined by $status(A) := status(A.protocol)$, where the right-hand side is the status of the underlying protocol component.

background

The module defines the protocol-level seam for cross-agent measurement comparison. An AlignmentProtocol is a structure extending Protocol with an explicit list of invariants (e.g., dominant mode or total Z) that must be preserved under alignment. The local setting records alignment as explicit data (map plus protocol) and requires falsifiers for any hypothesis or scaffold status.

proof idea

The definition is a one-line field projection that directly accesses the status component of the embedded protocol field inside AlignmentProtocol.

why it matters in Recognition Science

This accessor supports the cross-agent alignment scaffold and feeds parent results such as card_eq_seven in NarrativeGeodesic and ml_zero_parameter_certificate in ObservabilityLimits. It fills the measurement-domain seam step, enabling invariant checks across agents while leaving qualia comparability open. It aligns with the framework requirement that alignment data remain explicit.

scope and limits

formal statement (Lean)

  27@[simp] def status (A : AlignmentProtocol) : Status := A.protocol.status

proof body

Definition body.

  28
  29end AlignmentProtocol
  30
  31/-- An alignment map from one agent’s coordinate system to another’s. -/

used by (40)

From the project-wide theorem graph. These declarations reference this one in their body.

… and 10 more

depends on (12)

Lean names referenced from this declaration's body.