Row-profile census for diagonal-$2$ rows of an orbit-matrix candidate

import Mathlib.Data.Matrix.Basic
import Mathlib.Algebra.BigOperators.Fin

open scoped BigOperators

namespace Conway99

/-
  Row-profile census for diagonal-2 rows of a Conway99 orbit-matrix
  candidate. Machine-verified census (2026-09-08): eight off-diagonal
  entries with sum 12 and square-sum 28 form exactly the multisets
  {0,0,1,1,2,2,3,3} or {0,1,1,1,1,2,2,4}. Stated as fiber counts over the
  value classes 0..5 (entries above 5 are excluded by the square sum).
  Research infrastructure for `no_orbit_matrix_ten_of_no_four`; not an
  upload candidate until checked in the exact pinned environment.
-/
theorem diag_two_offdiag_profile
    (C : Matrix (Fin 9) (Fin 9) ℕ) (hsymm : ∀ i j, C i j = C j i)
    (hrow : ∀ i, ∑ j, C i j = 14)
    (hsq : ∀ i j, (∑ k, C i k * C k j) + C i j = (if i = j then 12 else 0) + 22)
    (i : Fin 9) (hi : C i i = 2) :
    ((((Finset.univ.erase i).filter (fun k => C i k = 0)).card = 2 ∧
      ((Finset.univ.erase i).filter (fun k => C i k = 1)).card = 2 ∧
      ((Finset.univ.erase i).filter (fun k => C i k = 2)).card = 2 ∧
      ((Finset.univ.erase i).filter (fun k => C i k = 3)).card = 2 ∧
      ((Finset.univ.erase i).filter (fun k => C i k = 4)).card = 0 ∧
      ((Finset.univ.erase i).filter (fun k => C i k = 5)).card = 0) ∨
     (((Finset.univ.erase i).filter (fun k => C i k = 0)).card = 1 ∧
      ((Finset.univ.erase i).filter (fun k => C i k = 1)).card = 4 ∧
      ((Finset.univ.erase i).filter (fun k => C i k = 2)).card = 2 ∧
      ((Finset.univ.erase i).filter (fun k => C i k = 3)).card = 0 ∧
      ((Finset.univ.erase i).filter (fun k => C i k = 4)).card = 1 ∧
      ((Finset.univ.erase i).filter (fun k => C i k = 5)).card = 0)) := by sorry

end Conway99