Prove2Me

Two-corner homology bound with incoming and outgoing ranks

Proved
Smooth4Algebra.unsaturated_corner_budget

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

homologicalalgebralinearalgebra

Let d:V→Vd:V\to V be square-zero in finite dimension over a field. Let EE and FF be two split, distinct linear blocks with inclusions and projections that are identities on their own block and zero on the other. Assume the outgoing/incoming ranks of EE are at most c−c_- and r+r_+, and those of FF are at most r−r_- and c+c_+. Then

dim⁡H(V,d)≥max⁡(0,dim⁡E−r+−c−)+max⁡(0,dim⁡F−r−−c+).\dim H(V,d)\ge\max(0,\dim E-r_+-c_-)+\max(0,\dim F-r_--c_+).

This is the linear-algebra form of the unsaturated opposite-corner bound. In a bifiltered application, the corner-incidence argument must separately establish the four stated rank bounds.

Preamble
import Definitions.Def_Smooth4AlgebraHomology
set_option autoImplicit false
Formal statement
theorem Smooth4Algebra.unsaturated_corner_budget
    {K V E F : Type*} [Field K] [AddCommGroup V] [Module K V]
    [FiniteDimensional K V] [AddCommGroup E] [Module K E]
    [FiniteDimensional K E] [AddCommGroup F] [Module K F]
    [FiniteDimensional K F]
    (d : V →ₗ[K] V) (h_square : d.comp d = 0)
    (incE : E →ₗ[K] V) (incF : F →ₗ[K] V)
    (projE : V →ₗ[K] E) (projF : V →ₗ[K] F)
    (hE : projE.comp incE = LinearMap.id)
    (hF : projF.comp incF = LinearMap.id)
    (hEF : projE.comp incF = 0) (hFE : projF.comp incE = 0)
    (rPlus rMinus cPlus cMinus : ℕ)
    (hEout : Module.finrank K (LinearMap.range (d.comp incE)) ≤ cMinus)
    (hEin : Module.finrank K (LinearMap.range (projE.comp d)) ≤ rPlus)
    (hFout : Module.finrank K (LinearMap.range (d.comp incF)) ≤ rMinus)
    (hFin : Module.finrank K (LinearMap.range (projF.comp d)) ≤ cPlus) :
    (Module.finrank K E - rPlus - cMinus) +
      (Module.finrank K F - rMinus - cPlus) ≤
        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 KK and every three finite-dimensional KK-vector spaces V,E,FV,E,F, each given as an additive commutative group with a KK-module structure, let d:V→Vd:V\to V be KK-linear with d∘d=0d\circ d=0, and let uE:E→Vu_E:E\to V, uF:F→Vu_F:F\to V, pE:V→Ep_E:V\to E, and pF:V→Fp_F:V\to F be KK-linear maps satisfying pE∘uE=id⁡Ep_E\circ u_E=\operatorname{id}_E, pF∘uF=id⁡Fp_F\circ u_F=\operatorname{id}_F, pE∘uF=0p_E\circ u_F=0, and pF∘uE=0p_F\circ u_E=0. For any natural numbers r+,r−,c+,c−r_+,r_-,c_+,c_- satisfying dim⁡Kim⁡(d∘uE)≤c−\dim_K\operatorname{im}(d\circ u_E)\leq c_-, dim⁡Kim⁡(pE∘d)≤r+\dim_K\operatorname{im}(p_E\circ d)\leq r_+, dim⁡Kim⁡(d∘uF)≤r−\dim_K\operatorname{im}(d\circ u_F)\leq r_-, and dim⁡Kim⁡(pF∘d)≤c+\dim_K\operatorname{im}(p_F\circ d)\leq c_+, the inequality ((dim⁡KE−r+)−c−)+((dim⁡KF−r−)−c+)≤dim⁡K(ker⁡d/(ker⁡d∩im⁡d))\bigl((\dim_K E-r_+)-c_-\bigr)+\bigl((\dim_K F-r_-)-c_+\bigr)\leq\dim_K\bigl(\ker d/(\ker d\cap\operatorname{im}d)\bigr) holds. The quotient views the intersection inside ker⁡d\ker d, and this intersection equals im⁡d\operatorname{im}d because d2=0d^2=0. Every subtraction in the two summands is natural-number subtraction truncated at zero, so the summands are respectively max⁡{dim⁡KE−r+−c−,0}\max\{\dim_K E-r_+-c_-,0\} and max⁡{dim⁡KF−r−−c+,0}\max\{\dim_K F-r_--c_+,0\} with integer expressions inside the maxima. Any of the spaces or bounds may be 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