proof

P40 Safety-case leaves

Lean spine source

formal/AlignmentProofSpine/Certification.lean

Declarations: P40_unsupported_leaf_blocks_root

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 P40_unsupported_leaf_blocks_root
    {n : Nat} {supported : Fin n → Prop} {requiresLeaf : Fin n → Fin n → Prop}
    {leaf root : Fin n}
    (h : requiresLeaf leaf root)
    (hunsup : ¬ supported leaf) :
    ¬ FiniteProvenDef supported requiresLeaf root := fun hp => hunsup (hp leaf h)