P02 LayeredAligned 7 layers: boundary, bundle, bearer, correction, successor, basin, adversarial

Declarations: P02_layered_alignment_requires_correction

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 P02_layered_alignment_requires_correction
    {A : System} :
    LayeredAlignedDef A → CorrectionIntegrity A := fun h => h.2.2.2.2.1