CODA-FOC: Finite Obstruction Calculus: Exact Quotient Diagnostics, Dual Witnesses, Two-Stage Coherence, and Transport

CODA-FOC: Finite Obstruction Calculus How much of a defect can an allowed repair actually remove? CODA-FOC answers in a declared finite-dimensional cochain packet. A first repair map changes a defect vector, a compatible next-defect map tests coherence, and an optional second repair map determines what can be removed one stage higher. Strictly positive coordinate weights turn both leftover questions into weighted ℓ¹ quotient distances, Φ₁ and Γ₂. The packet condition d₁d₀ = 0 ensures an exact first-stage repair cannot itself create a next-stage defect. Those two numbers yield three distinct diagnoses. Both vanish for an exact repair. A positive Φ₁ with zero Γ₂ is a coherent residual: something remains, but it passes the next coherence test. A positive Γ₂ is a nonclosed defect. The paper proves that the relevant minima are attained in its finite real setting, develops primal and dual certificates for the optimum, and studies what happens under direct sums and compatible transport. The operator-norm bound states exactly how much a mapped leftover may grow; it does not say that transport preserves every distinction or permission. Small exact rational examples let readers check the ideas without trusting a floating-point optimizer. The Python companion verifies primal and dual witnesses, rejects forged or shape-invalid certificates, and replays a finite registry of proposed corrections. Its vertex-enumeration solver has exponential worst-case cost. The Lean development covers algebraic and logical kernels; the full weighted linear-programming duality argument is given in the manuscript, not mechanized there. The point of the three labels is disciplined diagnosis. A residual can be retained and explained; a nonclosed defect can be refused or investigated. Neither label chooses an action or grants authority. The claim ledger identifies the hypotheses, proof mode, and finite tests behind each result, so a checkable example stays an example rather than becoming an unrestricted theorem.