{
  "todos": [
    {
      "content": "Read LiMoments.lean current state (defs + \u00a71\u2013\u00a74)",
      "status": "completed",
      "activeForm": "Reading LiMoments.lean"
    },
    {
      "content": "\u00a75: iteratedDeriv_zpow_neg_one + iteratedDeriv_seriesTerm",
      "status": "completed",
      "activeForm": "Proving per-term derivative lemmas"
    },
    {
      "content": "\u00a75: seriesTerm_deriv_summableLocallyUniformlyOn (M-test)",
      "status": "completed",
      "activeForm": "Building the M-test bound"
    },
    {
      "content": "\u00a75: iteratedDeriv_seriesFun_zero",
      "status": "completed",
      "activeForm": "Proving termwise derivation of seriesFun at 0"
    },
    {
      "content": "\u00a76: gFun_eventuallyEq_zero + capstone sigmaP_eq_neg_iteratedDeriv_gFun_div",
      "status": "in_progress",
      "activeForm": "Proving the capstone"
    },
    {
      "content": "Root-import LiTightR + LiMoments, full build, axiom audit",
      "status": "pending",
      "activeForm": "Building and auditing"
    },
    {
      "content": "Journal/db/STATE/NGUYEN updates + commit (ii\u2032-3b DONE)",
      "status": "pending",
      "activeForm": "Closing ii\u2032-3b"
    }
  ]
}

{
  "oldTodos": [
    "content='6-c-i: scaffolding (rectangle decomposition, path integrability, symmetry helpers, Z2hat mono)' status='in_progress' active_form='Building 6-c-i scaffolding'",
    "content='6-c-ii: I_III left-vertical bound \u2264 4T((2/3)Z2hat+10.5 log+48) + 40\u00b71.3352' status='pending' active_form='Proving the I_III left-vertical bound'",
    "content='6-c-iii: I_I right-vertical bound \u2264 IIMaj n' status='pending' active_form='Proving the I_I right-vertical bound'",
    "content='6-c-iv: mid-horizontal segment machine \u2264 (e\u2074+1)(NI + 5.5(10.5 log+48))' status='pending' active_form='Building the mid-horizontal segment machine'",
    "content='6-c-v: full horizontal assembly (mid + dog-leg tails, both sides)' status='pending' active_form='Assembling the full horizontal bounds'",
    "content='ii\u2032-6-d: the fold (pinch + 2\u03c0 factor + sfBoundProp)' status='pending' active_form='Folding into sfBoundProp'"
  ],
  "newTodos": [
    "content='6-c-i: scaffolding (rectangle decomposition, path integrability, symmetry helpers, Z2hat mono)' status='completed' active_form='Building 6-c-i scaffolding'",
    "content='6-c-ii: I_III left-vertical bound \u2264 4T((2/3)Z2hat+10.5 log+48) + 40\u00b71.3352' status='in_progress' active_form='Proving the I_III left-vertical bound'",
    "content='6-c-iii: I_I right-vertical bound \u2264 e^{1/3}\u00b7IIMaj n (F-E form)' status='pending' active_form='Proving the I_I right-vertical bound'",
    "content='6-c-iv: mid-horizontal segment machine \u2264 (e\u2074+1)(NI + 5.5(10.5 log+48))' status='pending' active_form='Building the mid-horizontal segment machine'",
    "content='6-c-v: full horizontal assembly (mid + dog-leg tails, both sides)' status='pending' active_form='Assembling the full horizontal bounds'",
    "content='ii\u2032-6-d: the fold (pinch + 2\u03c0 factor + sfBoundProp)' status='pending' active_form='Folding into sfBoundProp'"
  ],
  "cleared": false
}