The Δt framework’s informal theory contained three category errors where prose was collapsing distinct claim types into single sentences. Machine-checked formalization forced each claim to declare its type, then proved or falsified it on those terms.
Three slogans died. Four corrected statements replaced them. The theory is sharper and says less.
The 15-domain cybernetic failure taxonomy has a static pipeline graph with exactly four terminal nodes: Δg (gain mismatch), Δa (actuation mismatch), Δx (scale inversion), and Δh (hysteresis). These organize into three terminal families, not one.
Every non-terminal domain is classified by which terminals it can reach:
Role labels are structurally coherent for 10 of 11 roles. One mismatch (Δx labeled “cross-scale transmission” but structurally terminal) is left unresolved as data.
“Δh is the universal sink.” False as a graph-topological claim. Δs and Δk cannot reach Δh through any pipeline path. The signal family dead-ends at gain/actuation. The coupling family dead-ends at scale inversion.
The branching precursors (Δn, Δo, Δb, Δp, Δr) are dual-channel degraders. Each precursor event burns two budgets simultaneously:
Closure family is selected by whichever budget exhausts first. This depends on the interaction of burn profile (which precursor) and pre-existing budget asymmetry (system condition), not on precursor type alone.
The formally verified results:
“Precursor type determines closure family.” False. A system with weakened authority coupling is primed for hysteresis regardless of whether the precursor is model-heavy or governance-heavy. The selector is the budget asymmetry, not the event identity.
Once authority-consequence coupling breaks (Δc), hysteresis (Δh) is driven by cumulative rollback depletion under detached commits. The model has five states (aligned, detachedShort, detachedWarn, hysteretic, restructured) and five events (detach, commit, idle, reattach, externalRepair).
The formally verified results:
| Mechanism | Result | |
|---|---|---|
| Internally recoverable | Reattach while capacity remains | Original baseline restored |
| Externally repairable | External restructuring | New operational regime, reduced capacity |
| Locked in | No internal event exits hysteretic | Requires external intervention |
“Prolonged contiguous detachment is necessary for reset failure.” False. Repeated short detachment episodes, each individually recoverable, can accumulate into irrecoverability. Episode recoverability does not imply lifetime recoverability.
“Repair restores baseline.” False. External repair produces RESTRUCTURED, not ALIGNED. The system is operable again but not equally resilient. Repair restores operability, not original rollback margin.
This is not paper-claim cashout. It’s substrate — formal infrastructure that future Governor (agent_gov) work and any “no laundering” claim can cite. Doesn’t fit the slogan-killing pattern of Layers 1–3 because it’s not retroactively sharpening prose; it’s pinning an algebraic skeleton from scratch.
Four modules in LeanProofs/Admissibility/:
Authority.lean — verdict algebra. authorityVerdict : Basis × Precedence × Standing → AuthorityVerdict. Authorized iff all three dimensions green.StateTransition.lean — partitioned governance state (PolicyStore, EvidenceStore, GapStore, RevocationStore). Only Step.amendPolicy mutates PolicyStore. StepAllowed predicate gates raw mutation by per-step standing predicates.Derivation.lean — read-side bridge. GovState × Actor × AuthorityClaim → component verdicts, with revocation-shaped safety consequence (revoked_basis_never_authorized).Execution.lean — AuthorizedStep bundles a step with both StepAllowed (mutation standing) and authorityAuthorized (claim verdict) by construction. Load-bearing theorem: revoked basis cannot produce an AuthorizedStep.Governance-state mutation requires both mutation standing and an authorized claim verdict, and a revoked basis cannot produce an executable authorized step.
claimForStep resolution (deferred to Governor implementation; pre-committing the resolver is ontology bait).AuthorityClaim schema (kept abstract).appendEvidence / applyUpdate semantics).Derivation.deriveStanding (claim invocation) and StateTransition.*Standing predicates (state mutation).Governor (agent_gov) operationally implements this kernel’s pattern. The Lean modules don’t replace Governor; they pin the algebraic skeleton so a concrete Governor instantiation can cite “no laundering” with a formal warrant rather than a slogan.
The informal Δt framework theory was compressing three distinct claim types into single sentences:
All three conflations made the theory sound stronger than it was. The formalizations force the distinctions.
The corrected theory has a layered structure:
Each layer has its own claim type. Structural claims stay structural. Dynamic claims stay dynamic. Restorative claims stay restorative. They don’t get to share a sentence.
Formalization did not confirm the informal theory. It forced the informal theory to stop cheating.
The theory’s center of gravity was “Δh captures everything eventually.” That was doing three jobs at once: a graph claim, a persistence claim, and a restorative claim. Each job needed a different model. Each model, once built, killed part of the original slogan while sharpening the part that survived.
The machine didn’t make the theory more impressive. It made it more honest. That turned out to be the same thing.