CODA-FDA: Finite Descent Authority: Packets, Pipelines, and Seven Halt Guards

CODA-FDA: Finite Descent Authority A fluent proposal is easy to mistake for a finished decision. CODA-FDA makes that mistake testable. Its five-field packet names the finite carrier, admissible candidates, verifier, terminalizer, and failure discipline. A proposal has standing in the paper’s declared record model only when the pipeline actually returns a terminal and seven guards derived from evidence all hold. A confidence score, a claimed terminal label, or a conveniently filled form cannot replace that history. The seven guards ask whether the run was accepted, whether the same evidence replays deterministically, whether residual mass is exactly zero, whether a protected skeleton survived, whether every declared candidate was checked, whether a lift remains pending, and whether refusal is active. Each is a distinct way a seemingly complete result can fail. The manuscript shows that refusal cannot be overwritten by a later stage, that a terminal carries a path of intermediate results, and that one failed guard prevents the stated standing witness. The mathematical account has a sharp trust boundary. Record-level standing implies truth only under additional verifier-soundness and grant-soundness assumptions in a declared regime; an untrusted verifier supplies a countermodel. An optional exact rational ℓ¹ quotient calculation can inform the zero-residual guard, but algebraic zero is not a source of permission. The local Lean files prove scoped facts about the record model. They do not verify arbitrary callbacks or establish a real-world grantor’s legitimacy. The companion contains two complementary Python surfaces: a policy evaluator over supplied attestations and a finite execution harness that checks candidate certificates, stage snapshots, a declared lift registry, and repeated traces. Regression cases include substituted evidence, mutable aliases, omitted candidates, replay drift, and positive residuals hidden by a successful candidate. These tests make the boundaries visible without pretending to prove semantic verifier soundness. The separate CODA application has seven different local firewall checks; they are not this paper’s seven FDA guards.