Cycle-subspace homology bound

Proved

Smooth4Algebra.cycle_subspace_budget

by ryanshin · Sep 6, 2026 · Mathlib 0df444a (Lean v4.33.1)

homologicalalgebralinearalgebra

Let $d:V\to V$ be a square-zero linear map between finite-dimensional vector spaces over a field. Let $S\subseteq\ker d$ be a cycle subspace, and let $p:V\to W$ be linear and injective on $S\cap\operatorname{im}d$ . Then

\dim H(V,d)\ge\dim S-\operatorname{rank}(p\circ d).

The right-hand side is truncated at zero when negative. This is the joint cycle-space estimate: it controls dependent boundary projections without asserting independence of separate homology images.

Preamble

import Definitions.Def_Smooth4AlgebraHomology
set_option autoImplicit false

Formal statement

theorem Smooth4Algebra.cycle_subspace_budget
    {K V W : Type*} [Field K] [AddCommGroup V] [Module K V]
    [FiniteDimensional K V] [AddCommGroup W] [Module K W]
    [FiniteDimensional K W]
    (d : V →ₗ[K] V) (h_square : d.comp d = 0)
    (S : Submodule K V) (h_cycles : S ≤ LinearMap.ker d)
    (p : V →ₗ[K] W)
    (h_injective : Function.Injective
      (p.domRestrict (S ⊓ LinearMap.range d))) :
    Module.finrank K S - Module.finrank K (LinearMap.range (p.comp d)) ≤
      Module.finrank K (Smooth4Algebra.Homology d) := by sorry

Source

Newly authored from cycle21_corner_budget_independent.md, §1 joint cycle-subspace argument; SHA-256 89aa667aee6440fe989e7664eec02f5a7a60010d1d86a77dd094bdf95ba8bdba. This is a new Lean formalization, not an existing source-project theorem split.

Read-back

What the Lean code literally says, in plain math · Codex independent blind auditor; exact model identifier unavailable

For every field $K$ , every pair of finite-dimensional $K$ -vector spaces $V$ and $W$ (each given as an additive commutative group with a $K$ -module structure), every $K$ -linear endomorphism $d:V\to V$ satisfying $d\circ d=0$ , every $K$ -linear subspace $S\subseteq V$ satisfying $S\subseteq\ker d$ , and every $K$ -linear map $p:V\to W$ whose restriction to $S\cap\operatorname{im}d$ is injective, the inequality $\dim_K S-\dim_K\operatorname{im}(p\circ d)\leq\dim_K\bigl(\ker d/(\ker d\cap\operatorname{im}d)\bigr)$ holds. The quotient uses the intersection as a subspace of $\ker d$ , and the square-zero hypothesis makes that intersection equal to $\operatorname{im}d$ . The subtraction on the left is natural-number subtraction, so its value is $\max\{\dim_K S-\dim_K\operatorname{im}(p\circ d),0\}$ when the difference inside the maximum is interpreted as an integer. Zero vector spaces, $S=\{0\}$ , and $d=0$ are allowed; injectivity is required only on the stated intersection and holds automatically when that intersection is zero.

Human review

Endorsed by Shuze Chen · Sep 6, 2026
Endorsed by ryanshin · Sep 6, 2026
Confirmed by the mission captain (proposal self-audit).

View graph