other

FIMPACT

Lean spine source

Declarations: reachability_not_correction_capacity, auxiliary_reachability_preserves_correction_reachability

From the machine-checked spine in formal/ (Mathlib + spine imports). Not self-contained for Lean 4 Web — use the repo or a local lake build.

theorem reachability_not_correction_capacity :
    FieldFinite.ReachabilityPreserved
        FieldFinite.reachabilityWithoutCorrectionBefore
        FieldFinite.reachabilityWithoutCorrectionAfter ∧
      ¬ FieldFinite.CorrectionCapacityPreserved
        FieldFinite.reachabilityWithoutCorrectionBefore
        FieldFinite.reachabilityWithoutCorrectionAfter :=
  FieldFinite.reachability_preserved_not_correction

theorem auxiliary_reachability_preserves_correction_reachability
    {Option : Type} (m : FieldFinite.ReachabilityInterface Option)
    (haux : FieldFinite.AuxiliaryReachabilityPreserved m)
    (hiface : FieldFinite.CorrectionOptionsTrackedByAuxiliary m) :
    FieldFinite.CorrectionReachabilityPreservedByInterface m :=
  FieldFinite.auxiliary_reachability_preserves_correction_options m haux hiface