Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Native sparse-paving matching obstruction

Abstract

A specified basis fails exactly when its admissible target union is a circuit-hyperplane.

Definition 1.1 (admissibleUnion).

Formalization. D5/S3/Combinatorics/Matroids/SparsePavingMatchingObstruction.admissibleUnion (✓ std3).

Source. Repository-derived.

Commentary.

The admissible targets are the union over the specified source set: a target belongs if at least one source element has its sum outside the source ground. The empty source set gives the empty union. Its complement in the target ground is the set of translations keeping every source element inside the source ground.

Definition 1.2 (BasisMatches).

Formalization. D5/S3/Combinatorics/Matroids/SparsePavingMatchingObstruction.BasisMatches (✓ std3).

Source. Repository-derived.

Commentary.

The target-base existential ranges over all actual bases of the independently specified native target matroid. An equivalence of subtypes is a bijection between the source set and that target base. No representation, common ground, ordering, sign condition, or translation invariance of independence is required.

Theorem 1.3 (basiswise_obstruction).

Proof. Machine-checked in Lean as D5/S3/Combinatorics/Matroids/SparsePavingMatchingObstruction.basiswise_obstruction (✓ std3). ∎

Source. Repository-derived.

Commentary.

Let M and N be finite loopless native matroids on a torsion-free abelian group, of common positive rank r and equal ground cardinality m. Only N and its dual are required to be paving. The circuit and flat predicates, and the extended natural rank, are those of the actual N. The equation rho(C) + 1 = r states the hyperplane rank without truncated subtraction. All four consequences are conditional on failure, so rank one, full-rank grounds, and rank-zero duals remain within the quantified domain. Zero may belong to the source ground.

For each nonempty source subset X, the complement U of its admissible union satisfies X + (U union {0}) contained in the source ground. The pinned torsion-free Cauchy-Davenport theorem gives card(X) + card(U) at most m; zero contributes exactly once because it is excluded from the target ground. Subtracting from the target cardinality proves Hall’s inequalities, including the empty-subset case separately.

Apply the pinned finite Hall theorem to obtain distinct admissible representatives. In a sparse-paving matroid, dual paving bounds every nonspanning set by r elements: otherwise its complementary set is smaller than the dual rank and is independent, contradicting the native dual-rank identity. Paving then identifies any dependent r-element representative image as a circuit and a flat. If an admissible target lies outside that image, replace the representative at an index admitting it. A circuit with one element deleted spans the same flat, so adjoining the outside target gives an independent r-element set and hence an actual base. Thus failure forces the entire admissible union to equal the circuit-hyperplane. The converse follows because a base-sized injective image inside that union would equal the dependent circuit.

Looplessness excludes a singleton circuit, giving r at least two. If m equals r, the rank equation contradicts the circuit-hyperplane condition. Complementary cardinalities give card(U) = m - r. Applying the same sumset estimate again makes the contained sumset have cardinality m, so it equals the source ground. The additive bound, dual-rank formula, and Hall theorem are reused library inputs; the native representative repair and their source-domain composition are the formalized inference. No claim of external novelty is made.

References