Skip to content

v11.0.0

Choose a tag to compare

View all tags
@unpingable unpingable released this 16 Jul 00:55
· 69 commits to main since this release
v11.0.0
7cf3a6a

v11.0.0 — Occurrence-Exact Paid Recomposition

v11 introduces a stable, Mathlib-free theorem family for proof-relevant paid recomposition.

Ordered payments can now be checked occurrence by occurrence while retaining the exact removal equation and computed residue. Paid plans can move between global and catalog-relative forms without replacing the attempts, native receipts, expected-payment evidence, payment traces, or residue that were actually checked.

The central result is deliberately narrow:

Under exact attempt-level catalog completeness, paid global plans and paid catalog plans are equivalent. Endpoint-only completeness is insufficient.

This is a repository-integration theorem family, not a new cut connective, proof calculus, matching theorem, or planning algorithm.

Stable public API

The new stable root is:

LeanProofs.Witnessed.PaidRecomposition

It imports only:

LeanProofs.Witnessed.PaidRecomposition.Payment
LeanProofs.Witnessed.PaidRecomposition.Catalog

The stable import closure is transitively Mathlib-free and SCRATCH-free.

Occurrence-exact payment

PaymentTrace records an ordered sequence of exact ResourceChecker.removeAt equations. Each occurrence index refers to a position in the current wallet, and each successful step computes the next wallet exactly.

The public payment family includes:

  • PaymentTrace
  • PaymentRefusal
  • PaymentRefusal.sound
  • checkPayment
  • checkPayment_accepts_iff
  • PaymentTrace.length_conservation

checkPayment returns either an exact payment trace with computed residue or typed negative evidence that no trace exists for that submitted payment order and wallet.

Occurrence indices are context-relative positions, not persistent global token serials.

Exact catalog adequacy

Paid edges retain the exact attempt and its dependent native positive receipt.

PaidCatalogPlan retains the original global plan and adds exact catalog-membership evidence. Catalog conversion therefore cannot reconstruct, replace, or silently substitute:

  • the admitted attempt;
  • its native receipt;
  • the expected-payment map;
  • the payment trace;
  • or the computed residue.

The central catalog results are:

exact_catalog_adequate
exact_complete_globalizes_refusal

exact_catalog_adequate proves equivalence between nonempty catalog and global paid plans under ExactPaidCatalogComplete.

exact_complete_globalizes_refusal derives the corresponding scoped negative result: failure to realize a plan in an exact-complete catalog implies failure to realize one globally.

Three distinct claim scopes

v11 keeps three propositions separate:

  1. One submitted attempt or payment order is accepted or rejected.
  2. No accepted paid plan exists in one named catalog.
  3. No global paid realization exists under exact attempt-level catalog completeness.

A rejected submitted trace is not automatically a catalog refusal. A catalog refusal is not automatically global. The global conclusion requires an explicit ExactPaidCatalogComplete premise.

In particular:

ResourceCheckerExec.checkTrace = none

means only that the submitted trace was rejected. It does not identify an offender or prove catalog-relative or global nonexistence.

Independent evidence

The evidence modules remain public and separately buildable, but are excluded from the stable import graph.

Resource-trace application

Applications.ResourceTraceOneCrossing is a public-only, Mathlib-free end-to-end application.

It uses the resident ResourceCheckerExec.Trace Nat type and native checker equation directly, reconstructs the existing Checks and Derives witnesses, and retains the native receipt, expected-payment map, occurrence-indexed payment, and computed residue through catalog conversion.

Endpoint-completeness countermodel

Countermodels.EndpointCompleteness proves that endpoint coverage is too weak.

Its authorized and forged attempts share the same endpoints but differ in exact identity, dependent receipt content, and expected payment. A forged-only endpoint-complete catalog cannot realize the authorized global plan and is not exact-complete.

Finite-support annex

Applications.FiniteSupportOneCrossing remains annex evidence with an explicit SCRATCH dependency.

It retains native finite-support acceptance and refusal results, normalized derivations, positional provenance, exact payment residue, and the native excess-demand interpretation of the refused submission.

The earlier fixed three-cycle fixture was intentionally not promoted because it added no independent evidence beyond the generic checker, countermodel, and corpus applications.

Explicit nonclaims

v11 does not claim:

  • a new cut connective or proof calculus;
  • Hall, matching, 3DM, CSP, or complexity novelty;
  • general plan synthesis;
  • persistent global token serials;
  • a refusal transition or refusal debt-preservation theorem;
  • dynamic authority, resource creation, or temporal debt;
  • nontrivial injectivity or matching evidence from the singleton application.

PaidGlobalPlan.injectiveOn remains inherited plan plumbing.

PC-1 and PC-2 remain closed. Stateful bounded realization/refusal is the next formal frontier and is not part of this release.

Verification

The release passed the complete post-promotion verification envelope, including:

  • full and focused Lean builds;
  • the stable Witnessed target;
  • the separate PaidRecompositionEvidence target;
  • exact theorem and axiom footprint checks;
  • stable-root import-closure enforcement;
  • Mathlib-free and SCRATCH-free custody checks;
  • repository-wide axiom, native_decide, proof-hole, and placeholder audits;
  • citation metadata validation;
  • repository diff and whitespace checks.

The frozen stable footprint contains no sorryAx or Classical.choice. Its classified foundation is limited to the expected Lean core principles used by the existing list and quotient machinery.

Assets 2
Loading