Operationalizing ε, α, k — the knobs in practice
Parent: recursive-harness
gate-theory and safe-recursion-theorem hang on three Greek letters that look unmeasurable. The move that brings them down to earth: you never have the abstract metric — you have executable checks, and every theoretical quantity becomes a counter over checks.
δ (tolerance) = the strictness of an executable acceptance bundle
You never measure "distance to the waypoint" in an abstract metric. The gate IS a bundle of executable checks — tests, type checks, lint, invariant assertions, numeric tolerances. "Inside the δ-neighborhood" ⟺ all checks pass. δ is the bundle's strictness: more and tighter checks = smaller δ. Each check is a one-sided certificate — a failure proves you're genuinely outside; passing proves only "inside the ball", never perfection. The dial: acceptance criteria per stage (stage-anatomy); tightening costs more P×C per gate.
α (confidence) = the gate's MEASURED false-accept rate
α is not chosen — it is measured, by calibrating the gate against known-bad artifacts. This is exactly mutation testing: seed known bugs into the artifact, count how many the gate catches; the miss rate is an estimate of α. Two tiers: mechanical gates (compiler, type checker, deterministic tests) have α ≈ 0 — confidence is free there; semantic gates (LLM-as-judge, review) have unknown AND correlated α — calibrate them with seeded errors, and wherever possible push the check down into mechanical form (the Lean-style small-trusted-kernel move). This is the practical answer to honest-caveats #3: keep the union bound Σα honest by making the critical gates mechanical.
k (contraction) = the residual trend across repair rounds
Define the observable residual = the failing-check count (or error magnitude) after repair round n. The empirical contraction factor is the ratio . Sustained k̂ < 1 = the loop is converging; k̂ ≥ 1 for two consecutive rounds = divergence detected → backjump / re-plan / abort (gate-deviation-is-observable-delta, conflict-learning-and-backjumping). This converts the unprovable hypothesis "text-state steps contract" (honest-caveats #1) into a monitored quantity: you don't prove k < 1 — you watch k̂ and act the moment it isn't.
P×C = the budget counters
P×C on the ground = tokens, wall-time, and retry counts allotted per node. The leaf test is "small enough to one-shot and verify within budget"; the decomposition gate checks each child's budget is strictly smaller than the parent's and that the children sum within it.
Understandability — the knob behind the knobs (forming)
Should the gate also be understandable? Yes — on two sides, and it is load-bearing, not aesthetic:
- Gate-side: understandability = calibratability. You can only mutation-test a gate whose intent you understand (you must know what it is supposed to catch to seed the right bugs). An opaque gate (an un-audited LLM judge) has an α you cannot measure and a Goodhart drift you cannot detect — every number on the dashboard below turns fictional. A gate you can't read is a gate you can't trust.
- Artifact-side: understandability = tomorrow's ε. An artifact that passes every check but is incomprehensible raises the next round's per-step error (the executor errs more on opaque state) and carries hidden future P×C (maintenance). Worse, it outruns the owner's variety — and by requisite variety, an owner who can no longer model the artifact has stopped being its regulator (good-regulator-theorem).
So understandability is a precondition for the other knobs being real, not a fourth knob beside them.
How to gate it without a semantic judge: the round-trip reconstruction test. Give the explanation artifact (doc/spec) to a fresh executor with no access to the original code, ask it to re-derive the interface/behavior, then diff mechanically against the real artifact (do the types match? do tests written from the doc pass against the code?). Low reconstruction loss = the explanation is faithful and sufficient = understandable. Generation is fallible but the verdict is mechanical (the certificate pattern), and it calibrates like any gate: seed doc↔code mismatches and measure how many the round-trip catches. In Ashby terms: understandability = the artifact compresses losslessly into the owner's model — the round-trip is a direct test of that compression.
The dashboard
| theory knob | on the ground | how measured | tighten by |
|---|---|---|---|
| δ | acceptance-check bundle | which checks pass | add/tighten checks |
| α | gate false-accept rate | mutation testing / seeded bugs | mechanize the check |
| k | repair convergence | residual ratio | better verification, smaller steps |
| P×C | node budget | token/time/retry counters | decompose further |
None of the Greek letters needs the abstract metric — each becomes a counter over executable checks; that is how the theorems come down from the air.