Hall's condition survives on the complement of a critical subset

Identifier: F:hall-critical-subset-split
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 satisfying Hall's condition, and let t be a subset of s whose neighbourhood is no larger than t itself. Then the complement of t in s satisfies Hall's condition against the family with t's neighbourhood deleted from every member.

Formal statement

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

Dependencies

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

5 direct dependencies 2 direct dependents

Evidence

kernel-Nat.Hall.hallCondition_sdiff_of_critical

Kind: kernel-term
Status: checked

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

Checker command

test "$(cargo run -q -p axeyum-lean-kernel --release --example nat_theorem_inventory -- Nat.Hall.hallCondition_sdiff_of_critical 2>/dev/null | grep -xFc 'Nat.Hall.hallCondition_sdiff_of_critical	9	((x0 : AxNat.Finset) -> ((x1 : AxNat.Finset) -> ((x2 : ((x2 : AxNat) -> AxNat.Finset)) -> ((x3 : AxNat.Hall.HallCondition x0 x2) -> ((x4 : ((x4 : AxNat) -> ((x5 : Eq.{1} Bool (AxNat.Finset.memB x1 x4) Bool.true) -> Eq.{1} Bool (AxNat.Finset.memB x0 x4) Bool.true))) -> ((x5 : AxNat.le (AxNat.Finset.card (AxNat.Hall.unionOver x2 x1)) (AxNat.Finset.card x1)) -> AxNat.Hall.HallCondition (AxNat.Finset.sdiff x0 x1) (fun (x6 : AxNat) => AxNat.Finset.sdiff (x2 x6) (AxNat.Hall.unionOver x2 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. Mutation-verified: exchanging `t` and `sdiff s t` in the conclusion (and its matching binder) makes the kernel reject with `TypeMismatch` and kills all 11 tests in `nat_prelude::hall_theorem_tests` (measured 2026-09-05, exit 101).

footprint-Nat.Hall.hallCondition_sdiff_of_critical

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"
}