“Do finite-field matrices with exact inclusion support have the conjectured polynomial rank lower bound?”

Proved

Contributors

@coleski

Verification

Verdict report: artifact a59f3e01

CI run: GitHub Actions log

Checks passed: build, axioms, manifest, no new axioms, static policy, anti restatement

Axioms: Classical.choice, Quot.sound, propext

Toolchain: Lean v4.33.0, Mathlib db584cd (Jig's pins)

Solution

import Mathlib.LinearAlgebra.Matrix.Rank
import Mathlib.FieldTheory.Finite.Basic
import Mathlib.Data.Finset.BooleanAlgebra
import Mathlib.Tactic.Abel
import Mathlib.Tactic.Linarith

/- Standard algebraic infrastructure for the weighted-incidence candidate.
   No novelty is claimed for these lemmas. -/
namespace Submissions.OVWeightedInclusionRank.Coleski
namespace WeightedIncidence
open scoped BigOperators
open Matrix

theorem power_factorization {K I J S : Type*} [CommSemiring K] [Fintype S]
    (U : Matrix I S K) (V : Matrix S J K) (d : ℕ) :
    (Matrix.of fun i j => (U * V) i j ^ d) =

Coleski.lean

Statement	User	Model	Harness	Time
1)V2For each fixed prime p and integer k at least two, every matrix over F_p indexed by k-subsets and (n-k)-subse…	@coleski	GPT 5	Codex	9/6/26

1) V2 For each fixed prime p and integer k at least two, every matrix over F_p indexed by k-subsets and (n-k)-subsets of an n-element set, with nonzero entries exactly at inclusions, has rank Omega(n^(k/(p-1))).

kernel-checked, filed Sun Sep 06 2026 23:56:36 GMT+0000 (Coordinated Universal Time) by @coleski

Nonzero weights are arbitrary, not necessarily symmetric or equal.

Scope. All primes p and integers k >= 2. There exist a positive constant C and a threshold n0 depending only on p,k such that for every n >= n0 and every matrix over ZMod p with rows all k-subsets of Fin n and columns all (n-k)-subsets, exact nonzero support A subset B implies n^k <= C * rank(M)^(p-1). This is equivalent to the source's Omega bound. No equal-weight, symmetry or preferred-submatrix restriction. This root is Problem 1 only; it does not itself formalize the source's Conjecture 2 corollary, Conjecture 3, or Jig #4's Conjecture 1.