v13 custody correction: theorem/frontier status is unchanged. Finished Witnessed material is divided between exact stable roots and public evidence; live scaffolding named below moves to skunkworks. The v4-v7 checker substrate, including
FiniteSupportChecker, now lives underLeanProofs.CustodyIndexed. SeeV13-RELEASE-LEDGER.md.
v14 ownership note: four Witnessed substrate modules are intentionally multi-rooted into the Admissibility Calculus for the BreakGlass instance. WDC remains an independently scoped exact root; multi-root ownership does not turn the Witnessed family by itself into the full v14 Calculus.
Status: POST-2.0 REGISTER. Direction #1 (admitting-class normalization) has shipped in
v2.0.0 (peeled tag target b4bd02b, 2026-06-29):
AbstractNormalization.normal_form_iff_of_commutes is model-independent and axiom-free;
CommutesNecessity.commutes_is_necessary proves the commutation law is load-bearing;
Normalization.bridge_path_normal_form is now the freshness instance with its name,
signature, and [propext] footprint unchanged. Post-2.0 additive slices have now
landed for direction #2 (ND-style positive-fragment cut-elimination in Formula,
plus a Gentzen sequent presentation in Gentzen with position-general left
rules — repaired after HeadOnlyGentzenCutFailure proved cut-elimination false for
the head-only shape; the Deriv → Seq Hauptsatz over the repaired calculus is still
unproven) and direction #3 (canonical resource/residue
non-suppression, now including the v11 occurrence-exact paid-recomposition
integration family), and direction #4 has an initial consolidation/refusal-witness
slice landed. The larger proof-theory claims named below remain fenced unless
explicitly opened later.
Release boundary. The public-surface packaging gate shipped in 1.4.0. The reserved structural WDC milestone shipped in 2.0.0. Future frontier items do not inherit the integer just because they are adjacent; each needs its own formal delta, proof receipt, and release decision. Runtime consumption is not a prerequisite for theorem work.
Provenance: synthesized 2026-06-26 from a multi-model pass (Claude + ChatGPT), then located against the actual ratified surface. The directions are real and the ranking is advisory, not a commitment. Each item’s promotion requires its own formal delta, proof receipt, and custody decision. Name and formalize early; ratify lazily.
Every entry sits exactly where ../experiments/no_free_lift_wiring/RATIFICATION-v1.3.md already says “one direction
only,” “model-scoped,” or “not claimed.” The fences are the treasure map: each is
open because it is hard, not because it is speculative.
Normalization as an admitting-class theorem (LANDED in 2.0.0; NOT universal).
bridge_path_normal_form no longer depends on the freshness model for its proof shape:
it is the (CarryStep, WeakenStep) instance of
AbstractNormalization.normal_form_iff_of_commutes, whose only bridge-system hypothesis
is the local commutation law Commutes C W. The necessity counterexample proves that
hypothesis is load-bearing. This does not prove universal normalization, uniqueness
of representatives, full cut-elimination for arbitrary formula systems, or a confluent
rewrite system for arbitrary bridge graphs; the landed positive-fragment cut-elimination
lives separately in LeanProofs.Witnessed.Formula.
Formula.lean — ND-style positive-fragment cut-elimination LANDED.
Supplies Formula.atom, Formula.top, conjunction, disjunction, cut-free
derivations (CutFree), explicit-cut derivations (Deriv.cut), syntactic
cut_elimination, and cut-free cut_admissible. This is natural-deduction
style (intro/elim, no left rules), so its “cut” is hypothesis substitution — a
real theorem, but it never performs a principal-cut reduction.Gentzen.lean — real LJ-style sequent PRESENTATION LANDED. A
single-succedent calculus with genuine left/right rules (andL/orL/topL
decompose formulas in the context), cut-free Seq, with-cut Deriv, the trivial
inclusion deriv_of_seq : Seq → Deriv, soundness (seq_sound zero-axiom,
deriv_sound propext) against a shallow Holds semantics, and an embedding
deriv_of_formula_cutFree : Formula.CutFree → Gentzen.Deriv.HeadOnlyGentzenCutFailure.cut_elimination_fails
exhibits [atom 0, atom 1 ∧ atom 2] ⊢ atom 1, derivable with head-only cut but not
head-only cut-free (exhaustive over the rules), because head-only andL cannot
reach a buried conjunction. Slice B′ then repaired the live calculus: Gentzen.Seq
/ Gentzen.Deriv now use position-general left rules (pre ++ _ :: post),
re-proving soundness, and Gentzen.buried_conjunction_now_cutfree (zero-axiom)
proves the former obstruction witness is now cut-free — the regression receipt that
the repair works. The head-only failure is preserved only as an archived record
(HeadOnlyGentzenCutFailure), NOT a claim about the live calculus. All machine-checked,
propext-or-zero-axiom.What remains (B″). The actual Deriv → Seq cut-elimination over the repaired
position-general Seq is still unproven — it is a genuine cut-elimination proof
(principal-cut reductions, well-founded measure), not free. Until it lands,
deriv_of_formula_cutFree still lands in Deriv (with cut), so the corpus does not
yet show ND-provable ⇒ cut-free-Gentzen-provable and gets no subformula property. All
of this is the additive positive fragment {∧, ∨, ⊤} over WDC atoms and paid bridges;
it does not claim implication, negation, quantifiers, classical logic, a full
subformula theorem, or cut-elimination for arbitrary future formula systems.
Next slice (B″) = attempt Deriv → Seq now that Seq is structurally honest.
Canonical resource non-suppression (LANDED residue slice; not global linear logic).
LeanProofs.Witnessed.ResourceSequent now supplies ResourceFormula.claim,
ResourceFormula.bridge, ResourceFormula.residue, resource derivations with residual
output, residue_preserved, and erases_to_sequent. ResourceChecker promotes the
deterministic validation relation Checks with checks_sound, checks_complete,
checks_iff_derives, and validated_denial_sound. This cashes non-suppression as
residue preservation: residue inputs cannot silently vanish through derivation or
checker validation. It does not claim full linear logic, global no-weakening,
global no-contraction, or a complete custody/refusal resource calculus.
Executable gate (LANDED, Slice A): ResourceCheckerExec runs Checks as a
Bool-computing pass over an untrusted derivation trace (base step + pinned bridge
indices), recomputing the residual via removeAt; checkTrace_sound forces a real
Derives, checkTrace_iff_derives characterizes acceptance. It checks, it does
not search (no rule/split branching) and is a validation pass, not a decidability
decision. The trace is an untrusted input witness syntax, not the deleted
output-ResourceCertificate.
Adversarial corpus (LANDED, Slice C): LaunderingCorpus runs named laundering
specimens through the executable gate — missing-token, spent-token-does-not-fund-
next-crossing, floor-fact-is-not-spend-authority, residue-cannot-be-omitted,
ordinary-reachable-is-not-executable — each a refusal of a validity-to-authority
laundering move, with a positive control. Not a parser suite: verdict-named refusals.
Deferred (not on the public surface): a serializable ResourceCertificate
datatype. The witnessed object is the Checks relation, not a metadata shape;
a datatype is not validated merely because Checks is sound/complete. Re-admit
certificates only as (a) a proof-carrying ValidatedResourceCertificate bundling
a Checks proof, or (b) executable certificate data accepted by a Bool checker
with its own soundness/adequacy theorem. Until then the unchecked shape stays in
the sibling skunkworks at
~/git/skunkworks/formalization/Calculi/Scratch/UncheckedResourceCertificate.lean
(the v12 source path was
LeanProofs/Scratch/UncheckedResourceCertificate.lean) — keeping
“certificate exists + Checks valid ⇒ certificate is witnessed” off the
public surface.
Reachability / witnessed refusal (initial consolidation slice LANDED). The
composition_classification gate remains RETIRED (naive exclusivity failed;
naive_exclusivity_fails is a recorded finding in
../experiments/no_free_lift_wiring/COMPOSITION-CLASSIFICATION-TARGET.md / the playground repo, not a theorem on
the ratified surface). The honest replacement is reachability under declared steps plus
witnessed obstruction when reachability fails. Landed slice: ReachabilityClosure now
carries Prop-valued closed-lane witnesses (ClosedLaneRefusal / WitnessedRefusal),
WitnessedReachability adapts WDC PaidFrom to the generic Reach vocabulary and
proves the current authority/freshness WDC embedding is lane-separated, and
LocalBoundary consumes the generic reach invariant via adapters rather than proving
another isolated reach induction. Remaining work: characterize any additional bridge
graph lanes forced by future adapters, and retire/adapter-localize duplicate RTC shapes
as those consumers stabilize. No classifier, no trichotomy, no exclusivity claim.
refusal_composes_two_hop to n-hop and characterize boundaries that break
propagation (a refusal that won’t compose across a boundary is a laundering seam —
the negative result is the stronger one). Live scaffolding is in skunkworks
(MultiConsumerAdoption / QuorumCustody / ShardedCustody); the older
ConsumerRelative* fossils remain available in v12/Git history.
Refusal-legibility was not required for 1.4.0, 2.0.0, or v11; it remains a post-release frontier.Status: PROMOTED STABLE THEOREM FAMILY; FROZEN v11.0.0 BOUNDARY.
The stable Mathlib-free root LeanProofs.Witnessed.PaidRecomposition imports
only Payment and Catalog.
Frozen release claim:
Ordered payments admit proof-relevant, occurrence-indexed checking with exact computed residue. Under exact attempt-level catalog completeness, paid global plans and paid catalog plans are equivalent without replacing native receipts, expected-payment evidence, payment traces, or residue. Endpoint-only completeness is insufficient.
The types keep three scopes separate:
checkPayment accepts or refuses one submitted payment order; a resident
ResourceCheckerExec.checkTrace equation likewise concerns one submitted
trace only.¬ Nonempty (PaidCatalogPlan ... catalog ...) refuses a plan only relative
to that named catalog.exact_complete_globalizes_refusal reaches global nonexistence only from
catalog-relative refusal plus ExactPaidCatalogComplete; equivalently,
exact_catalog_adequate gives catalog/global existence equivalence under
that exact attempt-level premise.Evidence remains outside the stable import graph. Public-only
Applications.ResourceTraceOneCrossing retains a resident
ResourceCheckerExec.Trace Nat and its native positive equation through both
catalog conversions, reconstructing the resident resource derivation while
preserving the exact expected map, occurrence-indexed payment, and residue.
Public Countermodels.EndpointCompleteness is the premise-ablation witness:
authorized and forged attempts share endpoints but differ in exact identity,
dependent positive content, and expected payment, so endpoint coverage cannot
globalize paid refusal. Applications.FiniteSupportOneCrossing is public
evidence over LeanProofs.CustodyIndexed.FiniteSupportChecker; it supplies
native positive and negative forcing cases plus accepted-path
obligation-residue preservation. The fixed three-cycle enumeration was
intentionally not promoted because it adds no independent evidence.
The v11 boundary makes no new cut-connective or proof-calculus claim and no
Hall, matching, 3DM, CSP, complexity, or general plan-synthesis claim.
Occurrence indices are positions in the current submitted context, never
persistent serial identities. ResourceCheckerExec.checkTrace = none is only
rejection of that submitted trace. The PaidGlobalPlan.injectiveOn field is
inherited plan plumbing; the singleton corpus demonstrates no nontrivial
injectivity or matching fact. Catalog refusal has no transition semantics in
this family, hence there is no refusal non-transition theorem, refusal
debt-preservation theorem, dynamic-authority theorem, resource-creation
theorem, or temporal-debt theorem. PC-1 (heterogeneous certificates as a new
connective) and PC-2 (static admission as new matching/planning machinery)
remain closed.
Next frontier, not begun here: stateful bounded realization/refusal. It would require explicit transition semantics rather than reinterpreting the absence of transitions in v11 as a theorem. Dynamic authority, resource creation, and temporal debt remain outside that frontier until separately opened and specified.
Do not try to make the model→world conditional a theorem. A Lean stack proving when Lean proofs transfer to the world is the stack minting the receipt that governs the stack — a category error by doctrine. Keep it a fence. The seductiveness of the depth is the tell.
Dynamics — the Δt / PersistenceModel side (metastable decay, scalar-reward
collapse, the Δh-sink correction): Lyapunov functions, basins of attraction,
well-orderings on decay. The same honesty discipline applied to analysis instead of
proof theory. Listed so it is on the register; not ranked against the proof-theory line.
For slice discipline: composition-closure (#4) remains bounded and useful before heavier proof theory. For research leverage: the landed #2 result is the positive formula/Gentzen fragment; broader cut-elimination for richer future formula systems remains a separate proof-theoretic prize. A third edge, if the witnessed-clock lead (below) is live: it adds a term to the judgment (new constructor/cases, perhaps a new termination-measure component), so it must precede any broader cut-rank argument over that judgment, or the argument must be written to anticipate clock-carrying constructors.
The packaging release (1.4.0) deliberately spent a minor bump and left the integer for a
structural WDC result. v2.0.0 earned that integer through direction #1: model-independent
admitting-class normalization plus the necessity counterexample showing the commutation
law is load-bearing. It did not claim the later additive positive-formula
cut-elimination slice, the resource/residue slice, universal normalization, full
substructural non-suppression, or an API break.
Numbering reconciliation at v11. The repository’s post-v2 campaign series uses integer release numbers for bounded public theorem architectures as well as for proof-theoretic milestones. The classification below therefore measures proof-theoretic depth, not whether a repository tag may use an integer. V11 is earned as an occurrence-exact repository-integration theorem family with an exact premise-ablation countermodel; it is not represented as a new calculus or a new proof-theoretic connective.
Future structural WDC milestones still need a real change in what the calculus proves, or a breaking change forced by such a result. Current proof-theoretic milestone leads are:
Packaging, documentation, additional public surfaces, and model-scoped extensions do not by themselves earn a structural WDC milestone. Repository version/tag eligibility is decided by the bounded claim and release ledger for that campaign.
A 2026-06-27 multi-model pass surfaced a structural candidate and an operational adapter
track. Its 1.5–1.7 labels are historical planning labels, not current release-number
promises. Full synthesis (with the validator tool-theory and
the non-collapse table) lives in an internal working note, not part of this public
surface — working/tooltheory/validator-as-bounded-witness.md in the papers working tree
(may not resolve for an external reader). Sorted here by the rule above —
does it change the calculus, or carry it to the world?
The find: the untrusted-generator / deterministic-checker split is the corpus doctrine as
an executable architecture — validate : Policy → RuntimeFacts → WitnessCert → Except
Error Derivation with validate_sound is signed-is-not-witnessed at the wire. That is an
adapter track, named-not-started, and it does not change what the calculus proves:
Freshness,
not a core rewrite).The later-major lead, now separate from shipped v2.0.0 — witnessed clocks / temporal custody:
A freshness bound over a reported timestamp is not witnessed freshness; timestamp authority must itself be witnessed, or Δt validation launders time through assertion. Timestamp-signed is not timestamp-witnessed.
t_gen is attacker-controlled until witnessed. The hard question is what it means for a
timestamp to carry witness authority rather than assertion, and what refuses when it
doesn’t (trusted clock? skew? replay? does staleness refuse / degrade / re-witness?). This
connects the Δt paper series to the witnessed-derivation work. It is 2.0-class only
if solving it forces the derivation judgment to carry clock authority as a first-class
term — a breaking change forced by stronger math. Until then it stays a named frontier, not
a number.