Strict slack lets one value be deleted from every neighbourhood

Identifier: F:hall-noncritical-single-value-deletion
Proof route: kernel-lean
External status: proved
Axiom footprint: Empty

Recorded description

Let a family of finite sets be indexed by a finite set s in which every nonempty subset has strictly fewer elements than its neighbourhood. Then for any value v, s still satisfies Hall's condition against the family with v deleted from every member.

Formal statement

theorem Nat.Hall.hallCondition_sdiff_singleton_of_strict : ((x0 : AxNat.Finset) -> ((x1 : AxNat) -> ((x2 : ((x2 : AxNat) -> AxNat.Finset)) -> ((x3 : ((x3 : AxNat.Finset) -> ((x4 : ((x4 : AxNat) -> ((x5 : Eq.{1} Bool (AxNat.Finset.memB x3 x4) Bool.true) -> Eq.{1} Bool (AxNat.Finset.memB x0 x4) Bool.true))) -> ((x5 : AxNat.lt AxNat.zero (AxNat.Finset.card x3)) -> AxNat.lt (AxNat.Finset.card x3) (AxNat.Finset.card (AxNat.Hall.unionOver x2 x3)))))) -> AxNat.Hall.HallCondition x0 (fun (x4 : AxNat) => AxNat.Finset.sdiff (x2 x4) (AxNat.Finset.singleton x1))))))

Dependencies

The graph shows direct ledger edges. Follow a node to open its artifact page.

6 direct dependencies 1 direct dependents

Evidence

kernel-Nat.Hall.hallCondition_sdiff_singleton_of_strict

Kind: kernel-term
Status: checked

Supports: theorem Nat.Hall.hallCondition_sdiff_singleton_of_strict : ((x0 : AxNat.Finset) -> ((x1 : AxNat) -> ((x2 : ((x2 : AxNat) -> AxNat.Finset)) -> ((x3 : ((x3 : AxNat.Finset) -> ((x4 : ((x4 : AxNat) -> ((x5 : Eq.{1} Bool (AxNat.Finset.memB x3 x4) Bool.true) -> Eq.{1} Bool (AxNat.Finset.memB x0 x4) Bool.true))) -> ((x5 : AxNat.lt AxNat.zero (AxNat.Finset.card x3)) -> AxNat.lt (AxNat.Finset.card x3) (AxNat.Finset.card (AxNat.Hall.unionOver x2 x3)))))) -> AxNat.Hall.HallCondition x0 (fun (x4 : AxNat) => AxNat.Finset.sdiff (x2 x4) (AxNat.Finset.singleton x1))))))

Checker command

test "$(cargo run -q -p axeyum-lean-kernel --release --example nat_theorem_inventory -- Nat.Hall.hallCondition_sdiff_singleton_of_strict 2>/dev/null | grep -xFc 'Nat.Hall.hallCondition_sdiff_singleton_of_strict	10	((x0 : AxNat.Finset) -> ((x1 : AxNat) -> ((x2 : ((x2 : AxNat) -> AxNat.Finset)) -> ((x3 : ((x3 : AxNat.Finset) -> ((x4 : ((x4 : AxNat) -> ((x5 : Eq.{1} Bool (AxNat.Finset.memB x3 x4) Bool.true) -> Eq.{1} Bool (AxNat.Finset.memB x0 x4) Bool.true))) -> ((x5 : AxNat.lt AxNat.zero (AxNat.Finset.card x3)) -> AxNat.lt (AxNat.Finset.card x3) (AxNat.Finset.card (AxNat.Hall.unionOver x2 x3)))))) -> AxNat.Hall.HallCondition x0 (fun (x4 : AxNat) => AxNat.Finset.sdiff (x2 x4) (AxNat.Finset.singleton x1))))))')" -ge 1

Evidence notes

Admitted through `Kernel::add_declaration`, which re-derives the type from the proof term; the checker greps the inventory's exact row, so any single wrong token in the rendered type makes it exit 1.

footprint-Nat.Hall.hallCondition_sdiff_singleton_of_strict

Kind: exhaustive-enumeration
Status: checked

Supports: axiom_footprint: [] -- the Nat prelude's trusted surface is empty

Checker command

cargo run -q -p axeyum-lean-kernel --release --example nat_axiom_inventory -- --require-axiom-free nat

Evidence notes

`nat_axiom_inventory` reports `nat: axiom=0 opaque=0 quotient=0 total_trusted=0`, and this theorem is declared inside `build_nat_prelude`, so it cannot rest on a trusted declaration the Nat environment does not contain. Demonstrated to discriminate: `--require-axiom-free axreal` against the SAME kernel build exits 1 (`axreal trusted surface = 30, expected 0`), so the flag is not satisfied unconditionally.

Provenance

{
  "date": "2026-09-05",
  "established_by": "lane hall-theorem (ADR-1644): proved in `crates/axeyum-lean-kernel/src/nat_prelude/hall_theorem.rs` and admitted through `Kernel::add_declaration`",
  "source": "proved in-tree; no import, no replay"
}