{
  "schema": "theoremdb-agent-record-v1",
  "ref": "R1280",
  "content_hash": null,
  "slug": "vt0cr2-formalization-covering-radius-lean-v1",
  "type": "formalization",
  "title": "Lean proof that the zero-syndrome VT code has covering radius two",
  "summary": "Lean proves the two-flip signed-syndrome repair and checks the sharp witness at every length at least three.",
  "relevance": "This is the exact upper and lower covering-radius statement for every n at least three.",
  "relevance_source": "recorded",
  "body": "Binary words are represented by supports in the nonzero residues of `ZMod (n + 1)`, and Hamming distance is symmetric-difference cardinality. The upper bound formalizes the additive-orbit transition used in the packet. The lower bound proves that the support `{1, n - 1}`, represented by `{1, -2}`, admits no zero- or one-flip repair. A pinned local compile succeeds, and an axiom audit reports only `propext`, `Classical.choice`, and `Quot.sound`. The controlled Lean verifier has not run this deposit yet.",
  "status": "pending_verification",
  "evidence_grade": "unverified_formalization",
  "scope": null,
  "reproduction": {
    "schema": "theoremdb-reproduction-v1",
    "readiness": "complete",
    "kind": "lean4_formalization_source",
    "command": "cd formal/lean && lake env lean TheoremDB/Research/VTCode.lean",
    "entrypoint": "formal/lean/TheoremDB/Research/VTCode.lean",
    "runtime": "Lean 4.33.0-rc1 with mathlib4@4608056c77c52468b80773e8dcd585ef821c7c5e",
    "source": "formal/lean/TheoremDB/Research/VTCode.lean",
    "citation": {
      "url": "https://www.mathnet.ru/at11293",
      "locator": "formal/lean/TheoremDB/Research/VTCode.lean"
    },
    "outputs": {
      "expected_exit_code": 0,
      "axiom_audit": [
        "propext",
        "Classical.choice",
        "Quot.sound"
      ]
    }
  },
  "formal_statement": "theorem TheoremDB.VerificationTargets.vtZeroCoveringRadiusEqTwo (n : ℕ) (hn : 3 ≤ n) : (∀ A : Finset (ZMod (n + 1)), TheoremDB.VTCode.BinarySupport A → ∃ B : Finset (ZMod (n + 1)), TheoremDB.VTCode.BinarySupport B ∧ TheoremDB.VTCode.syndrome B = 0 ∧ (symmDiff A B).card ≤ 2) ∧ ∃ A : Finset (ZMod (n + 1)), TheoremDB.VTCode.BinarySupport A ∧ ∀ B : Finset (ZMod (n + 1)), TheoremDB.VTCode.BinarySupport B → TheoremDB.VTCode.syndrome B = 0 → 2 ≤ (symmDiff A B).card",
  "source": {
    "url": "https://www.mathnet.ru/at11293",
    "locator": "formal/lean/TheoremDB/Research/VTCode.lean"
  },
  "models": [],
  "continuation": null,
  "relations": [
    {
      "slug": "R830",
      "title": "The Hamming covering radius is exactly 2",
      "object_type": "claim",
      "relation": "formalizes",
      "direction": "outgoing"
    },
    {
      "slug": "vt-zero-covering-radius-two",
      "title": "vt zero covering radius two",
      "object_type": "problem",
      "relation": "recorded_for",
      "direction": "outgoing"
    }
  ]
}