LemmaStatement: AI-adaptedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-02

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced — the exact statement appears in a cited source; only wording and notation differ.
AI-adapted — a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated — a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Hall's condition passes to the strict and tight induction subinstances

Statement

Let $(X,Y)$ satisfy Hall's condition. If $|X|\ge2$ , then exactly one of the following usable reductions holds.

Strict case: if $|N(S)|>|S|$ for every nonempty proper $S\subset X$ , then for every edge $xy$ the graph obtained by deleting $x$ and $y$ satisfies Hall's condition on $X\setminus\{x\}$ .
Tight case: if some nonempty proper $S\subset X$ has $|N(S)|=|S|$ , then both the subgraph on $S\cup N(S)$ and the subgraph on $(X\setminus S)\cup(Y\setminus N(S))$ satisfy Hall's condition on their respective left parts.

Facts & Assumptions

Given: A finite bipartite graph with parts $(X,Y)$ satisfying Hall's condition.

[F1]

Hall's condition says $|N(T)|\ge |T|$ for every left subset $T\subseteq X$ (Bipartite neighbourhoods, Hall's condition and systems of distinct representatives).

Proof

technique · direct

1.1

In the strict case, let $xy$ be an edge and $T\subseteq X\setminus\{x\}$ ; if $T$ is nonempty then $T$ is proper in $X$ , so $|N(T)|>|T|$ and deleting $y$ leaves at least $|T|$ neighbours.

1.2

Thus the graph with $x,y$ deleted satisfies Hall's condition on $X\setminus\{x\}$ , including $T=\varnothing$ .

2.1

In the tight case, $T\subseteq S$ has $|N(T)\cap N(S)|=|N(T)|\ge|T|$ , while $T\subseteq X\setminus S$ with fewer than $|T|$ neighbours outside $N(S)$ would make $|N(T\cup S)|<|T\cup S|$ ; both induced subinstances therefore satisfy Hall.

step 1.2

3.1

Steps 1.1--2.1 establish the strict and tight reductions.

step 1.2step 2.1∎

Remarks

The two alternatives are exhaustive by whether a nonempty proper left subset is tight; the one-vertex case is kept in Hall's theorem rather than forced into this reduction.

Depends on

Used by

Hall's marriage theorem for a finite bipartite graph Theorem

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 15 results over 9 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources

F. Gotti, Matching and Hall's Theorem (standard reference, not scraped)