other

Embedded agency positive_margin_implies_epsilon_boundary green_named_path_with_bypass_not_integrity

Lean spine source

formal/AlignmentProofSpine/Field/Finite/CompositePathBypass.lean

Declarations: green_named_path_with_bypass_not_integrity, MB1_defeater_toy_nonstationary_shift, positive_margin_implies_epsilon_boundary

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 green_named_path_with_bypass_not_integrity :
    ∃ a : PathAudit,
      AuditsNamed a ∧
        PathLegitimate a ∧
        CompositeBypasses a ∧
        ¬ CorrectionIntegrityReal a := by
  refine ⟨⟨.named, true, true⟩, rfl, rfl, rfl, ?_⟩
  simp [CorrectionIntegrityReal]

/-- Green path alone (without no-bypass) does not imply integrity. -/

theorem MB1_defeater_toy_nonstationary_shift :
    ∃ s : MB1DefeaterToySample,
      MB1DefeaterToyEpsilonCertified s ∧ ¬ MB1DefeaterToyBoundaryConditionHolds s :=
  ⟨⟨true, true⟩, rfl, by simp⟩

/-- Same shape with the named nonstationary signal made explicit. -/

theorem positive_margin_implies_epsilon_boundary
    {b : Boundary} {margin distortion est : Int}
    (hleak : b.leakage ≤ margin - 2 * distortion - 2 * est)
    (_hpos : PositiveBoundaryMargin margin distortion est)
    (hdist : 0 ≤ distortion) (hest : 0 ≤ est) :
    EpsilonBoundary margin b := by
  unfold EpsilonBoundary
  have hsub : margin - 2 * distortion - 2 * est ≤ margin := by omega
  exact Int.le_trans hleak hsub