A formalized Lean 4 statement of the q-analog Erdős–Ko–Rado theorem, with a documented Mathlib substrate gap

v1.1 (2026-09-30), correction of a false statement. v1.0 stated the q-analog EKR bound without its hypothesis n ≥ 2k, in this description, in qekr_substrate.gap.md §1, and in the Lean signature of q_ekr (which assumed only 1 ≤ k ≤ n). As stated, the claim is false for 2k > n: any two k-subspaces then meet, so the whole Grassmannian is intersecting and exceeds a point-pencil (e.g. q = 2, n = 3, k = 2: 7 against 3). v1.1 assumes 2 * k ≤ n (the Frankl–Wilson range) in all three places, and in the prose restatements of the theorem in the Basic.lean module docstring and in gap.md (§1 gloss, §2(c)). The default lake build now compiles q_ekr (in v1.0 it did not), and check_axioms.lean prints [propext, sorryAx, Classical.choice, Quot.sound]. The proof is still a deliberate sorry, now on a true statement. Rebuilt from a clean unzip at Lean v4.29.0 / Mathlib 8a178386. The same files, differing only in line endings (41 of the 44 use CRLF here; the tag stores LF), are tagged v1.1 in the GitHub repository (https://github.com/papanokechi/unsolved-relay-2-erdos-ko-rado-q-analog-lean/tree/v1.1). SHA256SUMS.txt lists the hashes of this archive's files; verify against the Zenodo zip, not a checkout of the tag. This deposit is a formalized STATEMENT of the q-analog Erdős–Ko–Rado theorem together with an explicitly documented capability gap. It is NOT a formalized proof. The artifact, built in Lean 4 against Mathlib4 v4.29.0 (toolchain leanprover/lean4:v4.29.0, Mathlib SHA 8a178386ffc0, SHA-pinned), comprises: (i) QEkr.IsDimIntersectingOf, a q-analog of Mathlib's intersecting-families predicate that measures pairwise intersection by Module.finrank instead of Finset.card (fully proved API); and (ii) QEkr.q_ekr, a type-checked statement of the q-EKR (t = 1) bound: every 1-intersecting family of k-dimensional subspaces of 𝔽_q^n, n ≥ 2k, has cardinality at most that of a point-pencil through a fixed line. The proof of q_ekr is not formalized. Its body is a deliberate sorry marking an AEAL capability gap: the Mathlib v4.29.0 substrate required to discharge it is absent — specifically (a) q-binomial / Gaussian-binomial coefficients over 𝔽_q (zero declarations in Mathlib v4.29.0), (b) 𝔽_q subspace / Grassmannian counting (point-pencil enumeration and equinumerosity), and (c) the q-analog EKR extremal argument (Mathlib's only EKR is the classical finset version, which does not transfer to subspaces). lake build succeeds modulo exactly one intended sorry warning, and #print axioms QEkr.q_ekr lists sorryAx alongside propext, Classical.choice, and Quot.sound — the honest statement-not-proof signal, retained deliberately (not suppressed, not swapped for an axiom). The companion document capability/qekr_substrate.gap.md gives the full gap analysis, a dependency-ordered roadmap for a future formalizer, and the method-substitution history (Frankl–Wilson eigenvalue → compression → direct point-pencil counting, each substituted on a substrate failure). This is an honest partial result suitable as a short note / Mathlib-statement contribution — NOT the closed-proof Mathlib4 PR originally targeted.