other

Grounding drift class_certificate_not_deployment_safety

Lean spine source

formal/AlignmentProofSpine/Field/Finite/Nonrealizability.lean

Declarations: class_certificate_not_deployment_safety, epistemic_coverage_finite_shape_not_deployment_safety

From the machine-checked spine in formal/ (core modules are Mathlib-free;Field/Finite/ may import Mathlib). Not self-contained for Lean 4 Web — use the repo or a local lake build.

theorem class_certificate_not_deployment_safety :
    ∃ (π : ToyPolicy) (S : PlausibleSet) (μ : ToyEnv),
      ClassCertificate S ∧
        RobustUnderAmbiguity π S ∧
        Nonrealizable μ ∧
        ¬ SafeIn μ π := by
  refine ⟨.deploy, narrowClass, .offClassUnsafe, ?_, deploy_robust_on_narrow_class, ?_,
    off_class_unsafe_for_deploy⟩
  · intro μ hmem
    have : μ = .inClassSafe := by
      simp [narrowClass] at hmem
      exact hmem
    subst this
    simp [InRepresentedClass, representedClass]
  · simp [Nonrealizable, Realizable, InRepresentedClass, representedClass]

/-- Contrast: once the true environment is added to the plausible set,
    robustness *does* force safety there (instance of the transfer theorem). -/

theorem epistemic_coverage_finite_shape_not_deployment_safety :
    ∃ (π : FieldFinite.ToyPolicy) (S : FieldFinite.PlausibleSet) (μ : FieldFinite.ToyEnv),
      FieldFinite.ClassCertificate S ∧
        FieldFinite.RobustUnderAmbiguity π S ∧
        FieldFinite.Nonrealizable μ ∧
        ¬ FieldFinite.SafeIn μ π :=
  FieldFinite.class_certificate_not_deployment_safety