Unimodality of q-Fibonomial Coefficients for n = 4

Bergeron, Ceballos, and Küstner conjectured that q-Fibonomial coefficients are unimodal. Recent work of Connelly, Ito, Martinez, Shevchenko, and Yang proves the conjecture for all slices with n ≤ 3. We prove the complete n = 4 slice: for every integer m ≥ 0, the q-Fibonomial coefficient binom{m+4}{4}F,q is a polynomial with nonnegative, symmetric, unimodal coefficients. Writing a = Fₘ₊₁ and b = Fₘ₊₂, the proof reduces every first-half coefficient difference to four shifted copies of the restricted partition function p(n) = [q^n]/((1-q)(1-q^2)(1-q^3)). The exact period-six formula 12p(n) = (n+3)^2 + ε(n), with bounded periodic error, yields a uniform smoothing theorem for b ≥ a ≥ 14; the finitely many remaining Fibonacci cases are exact. The proof is independent of the general q-Fibonomial polynomiality and positivity theorem. A companion Lean 4 formalization kernel-checks the exact universal theorem with no unresolved mathematical interface. The unrestricted q-Fibonomial unimodality conjecture remains open. Additional notes / claim boundary: Mathematical status: M5 — exact n = 4 target proved. Formal-verification status: FC4 — the exact universal theorem is kernel-checked in Lean 4 with zero sorry/admit and no unresolved mathematical interface. The formalization depends only on the standard Lean axioms propext, Classical.choice, and Quot.sound. Novelty wording is intentionally limited to: APPARENTLY NEW WITHIN THE LITERATURE SEARCHED THROUGH 11 SEPTEMBER 2026. This is not a claim of certified global historical priority. Independent human peer review is pending. The unrestricted q-Fibonomial unimodality conjecture, including n ≥ 5, remains open.