{
  "schema": "theoremdb-agent-record-v1",
  "ref": "R865",
  "content_hash": null,
  "slug": "fib-formalization-four-corner-classification",
  "type": "formalization",
  "title": "Fibonacci support four-cycle classification",
  "summary": "Lean proves that every support square has corner sums q_(t-2), q_t, q_t, q_(t+1) and equal row and column increments q_(t-1).",
  "relevance": "For fib problem determinant range; fib problem nonzero support, record fib-formalization-four-corner-classification (“Fibonacci support four-cycle classification”) states a machine-checkable theorem or proof obligation. The record states: Lean proves that every support square has corner sums q_(t-2), q_t, q_t, q_(t+1) and equal row and column increments q_(t-1).",
  "relevance_source": "recorded",
  "body": "The proof is kernel-checked in the pinned world and has no local sorry. It first removes the duplicated initial Fibonacci value, proves the required index arithmetic, and then lifts the result to matrix coordinates.",
  "status": "draft",
  "evidence_grade": "unverified_formalization",
  "scope": null,
  "reproduction": {
    "schema": "theoremdb-reproduction-v1",
    "readiness": "partial",
    "kind": "formalization",
    "runtime": "lean-4.33.0-rc1/mathlib4@4608056c77c52468b80773e8dcd585ef821c7c5e+theoremdb@d575c4e2ff28345440c4f8a42bf0178bcb3f6f41b703a45d9d1cbb709036f0dc",
    "citation": {
      "url": "https://mathoverflow.net/questions/513340/is-the-determinant-of-this-fibonacci-sum-indicator-matrix-always-1-0-or/513372",
      "locator": "formal/lean/TheoremDB/Fibonacci/Graph.lean"
    },
    "missing": [
      "source",
      "command",
      "expected_output"
    ]
  },
  "formal_statement": "theorem fibonacci_support_four_corner_classification {x X y Y : ℕ} (_hx : x < X) (hy : y < Y) (hmiddle : x + Y ≤ X + y) (hA : IsFibonacci (x + y + 2)) (hB : IsFibonacci (x + Y + 2)) (hC : IsFibonacci (X + y + 2)) (hD : IsFibonacci (X + Y + 2)) : ∃ t : ℕ, 3 ≤ t ∧ x + y + 2 = positiveFib (t - 2) ∧ x + Y + 2 = positiveFib t ∧ X + y + 2 = positiveFib t ∧ X + Y + 2 = positiveFib (t + 1) ∧ X = x + positiveFib (t - 1) ∧ Y = y + positiveFib (t - 1) := by\n  -- Checked proof in formal/lean/TheoremDB/Fibonacci/Graph.lean",
  "source": {
    "url": "https://mathoverflow.net/questions/513340/is-the-determinant-of-this-fibonacci-sum-indicator-matrix-always-1-0-or/513372",
    "locator": "formal/lean/TheoremDB/Fibonacci/Graph.lean"
  },
  "models": [],
  "relations": [
    {
      "slug": "R863",
      "title": "Fibonacci odd square cover",
      "object_type": "formalization",
      "relation": "depends_on",
      "direction": "incoming"
    },
    {
      "slug": "R904",
      "title": "Lean definition of the Fibonacci-sum matrix",
      "object_type": "formalization",
      "relation": "depends_on",
      "direction": "outgoing"
    }
  ]
}