Target Realization
Open construct-lifecycle crux — given target P, can we build a system that tracks P? Lean model only (ConstructionCrux); not an MB bridge.
Lifecycle role: construct (open spine interface — not an MB* matrix column).
Given an alignment target , can we construct a system that robustly tracks ? This is distinct from:
- Identification (what is ? — MB2 / bundle identifiability)
- Certification (does evidence license that tracks ? — safety-case layers,
CertifiedAsRealizing)
Lean types the separation in AlignmentConstruction.lean: Realizes vs CertifiedAsRealizing; ConstructionCrux / TargetRealizable is not axiomatized. fin_certification_without_construction exhibits that a certification schema can be satisfied while no finite toy realizes the target.
CEV is not a special bridge: constitutionalTarget / cevConstitution parameterize an AlignmentTarget on the same interface (MB8 is a gravestone only).
Book: introduction (three questions); ch33 (certification without construction). Lifecycle: Alignment lifecycle (construct phase). Field evidence: /field/coverage/.