lean

Changelog

Release history for the Lean Proofs stack. Zenodo versions, where present, live under concept DOI 10.5281/zenodo.20369489. Git tags, GitHub releases, and Zenodo deposits are separate operator-controlled receipts and must be verified independently; a GitHub release does not by itself prove that the corresponding Zenodo version exists. As checked 2026-07-20, the v11–v14 portion of the public series contains v11, v13, and v14 but no v12 version record.

16.0.0 — Governed Transition Boundaries (2026-07-28)

Adds one public-evidence surface answering, for selected targets and selected source views, whether a single total decoder recovers the target from the view, correctly for every source.

• Generic core (four axiom-free receipts): explicit factorizations compose; they imply the public ViewSemantics.Determines fibre-constancy relation; a target-distinguishing collision blocks them; and a carrier derived solely by deterministic postprocessing of an insufficient view does not restore them. The converse is not claimed.
• Declared finite representation: an exhaustive functional-dependency and attribute-selection calculation over 1,024 declared sources and 128 duplicate-free coordinate selections, with a unique least target-determining selection and exactly two determining masks.
• Five separately scoped witnesses — fixed-policy authorization refusal, selected-context validation, bounded capacity realizability, occurrence-link observation, and modeled hidden-relation nonidentifiability. Each is bounded to its own fixture.
• The generic statements are standard function-factorization and view-determinacy facts; the finite result is a fixed-table dependency calculation. The contribution is their mechanically checked synthesis. No novelty or priority is claimed.
• Custody: 283 public Lean sources (115 stable, 167 public evidence, one aggregate) across twelve stable roots and 142 ownership relations; 283/283 target-owned across 30 registered targets. Stable roots, their import lists, and scripts/stable-surfaces.tsv are unchanged from v15.
• Two new gates: a 29-receipt exact footprint replay and a 10-source crossing gate that byte-pins every new file by SHA-256 and Git blob.
• The v15 ATLAS classification and its four negative results remain authoritative and unchanged.

V16 establishes no new generic factorization theorem, general authorization theory, temporal validity, general amalgamation, causal attribution, attestation correctness, universal transition-relative semantics, canonical global carrier, target-independent least representation, cross-surface composition, or runtime conformance. The v16.0.0 tag, GitHub release, and Zenodo deposit are built on this tree; the version DOI is recorded from Zenodo after the release creation mints it.

15.0.0 — Cross-Calculus Atlas (2026-07-24)

This formal-methods release studies governed computation across three independent semantic domains. It records receipt-indexed correspondence without a shared bridge algebra: the exact public Continuity Admission rename, StaticRole through R3, and checked mappings for selected Governed Transport, Execution Custody, and Continuity Admission edges in the final PJ Atlas surface.

• PJ preserves the primary calculus mappings and exact judgment indices.
• Exact-receipt anti-minting remains receipt-fiber-local and non-definitional; positive collapse controls remain public.
• StaticRole is a qualified partial held-out instance with local dependence structure; it makes no phenomenology, consciousness, prediction-success, or personal-identity claim.
• Inquiry and Preparation remain frozen independent comparison-only neighbors outside the PJ primary surface.
• This is the first tagged release to archive the governed-transport public surface: the GT-4A stable root and the C03 evidence admission, publicly admitted 2026-07-20/21 after the v14 tag, with 704 declarations (460 stable, 244 evidence) receipted in docs/GT4A-PUBLIC-COMPATIBILITY-RECEIPT_2026-07-20.md.
• FRONTIER-NOT-COMPOSITIONAL, NO-USEFUL-OWNERSHIP-COMMONALITY, CONTEXT-TRANSPORT-NOT-GENERIC, and ONLY-DOMAIN-SPECIFIC-RESIDUAL-THEORIES remain authoritative.

V15 establishes no shared bridge algebra, generic frontier composition, generic ownership, generic context transport, universal calculus, runtime conformance, JCP implementation, or operational AG/NQ realization. The v15.0.0 tag, GitHub release, and Zenodo deposit are built on this tree; the version DOI is recorded from Zenodo after the release creation mints it.

14.0.0 — Governed Admissibility Calculus (2026-07-18)

Assembles the capital-C Admissibility Calculus in seven separately reviewed rungs, each extracted from the sibling research tree with source-equality receipts.

• Rung 1: PathVerdict functorial domain transport (Domains) and carried-id located diagnostics (Located) join the path-verdict root; exact 36-receipt footprint gate.
• Rung 2: the import-free GovernedFamily signature under the new Admissibility.Calculus construction namespace — claim-indexed witness/refusal DATA, separate standing/custody/obligation books, derived authority, a total evidence-returning checker, and the claim-erasure impossibility theorem.
• Rung 3: the Weathering and BoundedPaidReachability instances with their one-owner native seams; the paid native API (Run/Provenance/Resource/Warrant/State/Action/Step) frozen.
• Rung 4: the exact dependent refusal-packet spine — bare SpineEncoding versus LosslessEncoding with both inverse laws; the superseded reason-only contract survives as a compiled collapse counterexample in research custody.
• Rung 5: the closed seven-entry indexed comparison framework (dependent law selection, same-map preservation/loss receipts, receipt-bearing capabilities, typed native-source gaps); the concrete proof-carrying ledger over pinned native sources remains receipt-bound research evidence.
• Rung 6: the stored-decision crossing — decide once, preserve both native outcomes, derive verdicts, located obstructions, and comparison receipts solely from the stored pair — with its witnessed Weathering/bounded-paid inhabitant and its vacuity/empty-obligation fences shipped in the same surface.
• Rung 7: the origin/history-bound BreakGlass terminal instance — lifecycle-origin namespacing, kind-indexed references, receipt-committed book-attested audit history, verdict-level exceptional/ordinary and settlement/audit separations, and a stored crossing. Public footprint accepted explicitly: 101 receipts = 3 axiom-free + 19 opaque-substrate-only + 4 +propext + 67 +Quot.sound + 8 +Classical.choice.
• The public Calculus root freezes 191 receipts (rungs 2–7); the exact custody counts are in the release ledger, and a cross-repository description-coherence gate guards the prose against the code.
• The capital-C name was adopted only after all seven rungs closed, resolving the v10 reservation. A plain-language summary of the research program is added at docs/PLAIN-LANGUAGE-SUMMARY.md.

Frozen inventory: docs/V14-RELEASE-LEDGER.md; per-rung receipts: docs/V14-READINESS-LEDGER.md; claims: CLAIM-REGISTER.md #19–#25.

13.0.0 — Repository Custody Migration (2026-07-17)

No new mathematical campaign. This custody-only compatibility release corrects module paths, terminal roles, exact roots/targets, and whole-tree enforcement after a 271-file audit showed that ANNEX, Scratch, and candidate labels no longer described the repository honestly.

• Rehome the unchanged v4-v7 public substrate under LeanProofs.CustodyIndexed and PathVerdict under LeanProofs.Admissibility.PathVerdict.
• Distinguish exact-root stable API from terminal public evidence; public evidence is finished and citable without becoming a compatibility promise.
• Remove superseded fossils, including the duplicate Admissibility CarryLaws/NoFreeLift modules, the empty LeanProofs/Basic.lean scaffold, and the standalone taxonomy-lean-sketch.lean probe. Retire the duplicate experiments/no_free_lift_wiring Lean source while preserving all exact v12/Git provenance.
• Transfer all 53 of 53 live incubations to the sibling skunkworks. Its 26-check migration audit passes, including all four returns in the explicit Mathlib incubation lane; the public originals are deleted.
• Replace the partial custody checker with fail-closed whole-tree registries and exact stable/evidence closure checks. It passes the actual tree exactly: 179 public files (82 stable, 96 evidence, one aggregate), ten stable roots, and 98 ownership relations. The strengthened target gate passes across two Lake projects with 23 public targets, 23 exact local closures, 19 Mathlib-free current-tree targets, 463 local ownerships, one pinned-external target, and one locked boundary, and reverse-closes role-compatible target ownership over all 179/179 public sources; the downstream fixture’s 19-job bare build passes. The final public and sibling suites pass, including a clean 149-job sibling build, all four Mathlib incubations, and the sibling’s 29-check CI. The exact deletion audit accounts for 38 public rehomes, 53 skunkworks transfers, 23 archived experiment sources, 20 fossils, and four separately recorded deletions, with zero unaccounted files. The integrity audit finds 171 retained/rehomed theorem sources token-equivalent to v12 and eight new import-only roots; v13 adds no theorem body.

Release inventory, compatibility decisions, and verification receipts: docs/V13-RELEASE-LEDGER.md.

12.0.0 — Judgment Orientation (2026-07-16)

Raw custody is a sequence; effective exact-origin contribution is its finite-support join-semilattice projection.

• Promoted the five Mathlib-free theorem modules Core, Attribution, Provenance, OriginSupport, and Bridge under the exact stable LeanProofs.JudgmentOrientation root. The first four originated in skunkworks commit 4f8e076; Bridge was authored during promotion review.
• Added structural inquiry/judgment confinement, privileged change-point attribution, exact-origin replay accounting, an abstract finite-support join-semilattice, operational trace/state projections, and explicit information-loss boundaries.
• Bridge proves that an endpoint-visible difference in an orientation-invariant observation across an attributed mixed trace localizes to a privileged step whose caller-supplied origin is contained in the effective support of the trace’s privileged provenance. Attribution is structural — AttributedStep.privileged carries its Occurrence — and the converse is refuted by a no-op witness in the annex.
• Kept Streetlamp, source-blind laundering, accumulator-repair, four-relay, payload-conflict, and bridge fixtures in a separately imported ANNEX.
• Added scripts/check-judgment-orientation-footprint.sh and its CI step: a fail-closed gate asserting the exact axiom footprint of thirteen frozen receipts across the five-module family, matching the Witnessed and PaidRecomposition gate pattern.
• Replaced the scratch-era reducible quotient carrier with a private EffectiveSupport representation, and renamed MayOrient.paid to MayOrient.admitted so reusable standing is not mislabeled as linear spend.
• Added exact build and custody wiring without changing the 1.x AdmissibilityKernels import list.
• Corrected the inherited v11 paid-recomposition custody registry: the unchanged NoFreeLift → Derivation → Sequent → ResourceSequent → ResourceChecker foundation was already in the stable eight-module import closure and is now classified PUBLIC-SHIPPED. This is classification-debt repair, not new v12 mathematics or capability.
• Hardened the paid-recomposition gate so the ANNEX finite-support evidence may directly import exactly the singleton LeanProofs.Scratch.FiniteSupportChecker, with no additional direct Scratch imports hidden on the same or another import line.

Release inventory and verification boundary: docs/V12-RELEASE-LEDGER.md.

11.0.0 — Occurrence-Exact Paid Recomposition (2026-07-15)

Exact occurrence payment and exact-attempt catalog custody, without replacing the evidence that was actually checked.

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.

• Occurrence-exact payment — PaymentTrace carries the exact ResourceChecker.removeAt equation for each context-relative occurrence and therefore computes a precise residue. PaymentRefusal.sound rules out a trace for the same submitted order and wallet; checkPayment is total, checkPayment_accepts_iff reflects trace existence, and PaymentTrace.length_conservation records the resource count.
• Exact catalog adequacy — paid edges retain the exact attempt and its dependent native positive receipt. ExactPaidCatalogComplete ranges over admitted attempts, not plans or search output. Catalog-to-global conversion forgets only membership; exact completeness supplies membership in the reverse direction. exact_catalog_adequate proves the resulting existence equivalence and exact_complete_globalizes_refusal derives the scoped global-refusal corollary.
• Evidence, outside the stable import graph — Applications.ResourceTraceOneCrossing is a Mathlib-free, public-only end-to-end application retaining the resident ResourceCheckerExec receipt, expected map, payment, and residue. Countermodels.EndpointCompleteness separates authorized and forged attempts with identical endpoints and proves endpoint coverage insufficient. Applications.FiniteSupportOneCrossing retains native positive and negative finite-support checker results as annex evidence with an explicit SCRATCH dependency. The fixed three-cycle fixture was intentionally not promoted because it adds no independent evidence.
• Custody and build surface — the stable LeanProofs.Witnessed.PaidRecomposition root imports only Payment and Catalog; it is Mathlib-free and transitively SCRATCH-free. Applications and countermodels remain separately buildable evidence and are excluded from the stable root. The paid-recomposition footprint gate fixes this import and theorem/axiom boundary.

Claim scopes. One native checker equation accepts one submitted attempt. ¬ Nonempty (PaidCatalogPlan ...) rejects realization only in the named catalog. Global nonexistence follows only when an ExactPaidCatalogComplete premise is supplied.

Non-claims. No new cut connective or proof calculus; no Hall, matching, 3DM, CSP, or complexity novelty; no general plan synthesis; occurrence indices are context-relative positions, not persistent serials; ResourceCheckerExec.checkTrace = none means only rejection of that submitted trace; no refusal transition, refusal debt-preservation, dynamic authority, resource creation, or temporal debt. The singleton corpus application supplies no nontrivial injectivity or matching evidence: injectiveOn is inherited plan plumbing. PC-1 and PC-2 remain closed. Stateful bounded realization/refusal is the next frontier and is not part of v11.

Release inventory and verification boundary: docs/V11-READINESS-LEDGER.md.

10.0.0 — View Semantics and Bounded Projection (2026-07-14)

Distinguishability as a first-class axis: view refinement changes what is distinguishable without minting transition authority.

10.0.0 lands the view-semantics campaign: a canonical distinguishability core over finite view systems, an exact characterization of deterministic bounded projection, a sound-and-complete finite checker with typed certificates, and a custody adapter proving that greater visibility constructs no authority. The bounded release claim, gate receipts, and verification envelope are in docs/V10-READINESS-LEDGER.md.

• ViewSemantics core (UNRATIFIED-CANDIDATE, Mathlib-free) — View, Indistinguishable, fine-to-coarse Refines, Determines, NotFullyDetermining, FiberwiseAmbiguous; the weak/strong boundary with inhabited (non-vacuous) witnesses and a closed three-world non-converse; composition laws (compose_indistinguishable_iff, refines_compose_iff, compose_mono, determines_compose_iff) with finiteJoin exposing the finite-family API; rooted counterexamples showing weak nondetermination is not closed under composition while declared disclosure bounds compose.
• Bounded projection — OperationallySufficient stays existential (the general-safe fence); deterministic bounded sufficiency has an exact refinement-sandwich characterization (deterministicallyBoundedSufficient_iff_refinement_sandwich) and constructive existence boundaries that choose the required-action projection, never the budget; all four disclosure × sufficiency audit cells are inhabited.
• Sixth-atom adjudication (negative, scoped) — the axis adapter imports the resident bridge Atom/Family ontology rather than recreating it; no_resident_bridge_pair_pays_all_five shows the literal all-five bridge premise is uninhabited in the resident ontology; disclosure is recorded as an orthogonal view-context axis, deliberately not a sixth family atom (disclosure_is_orthogonal_to_resident_bridge_ontology).
• Finite checker — ViewAudit returns two independent typed results: PolicyCertificate / ActionConflict (conflicts carry an inhabited observation fiber and a rejecting same-fiber world per action) and BoundCertificate / ForbiddenDistinction (concrete worlds equal under the budget, unequal under the view); checkActionability_*_iff and checkDisclosure_*_iff prove soundness and reflection in both directions; all four quadrants execute without native_decide and without a collapsed validity bit.
• Authorized-trace custody adapter — DynamicTraceAdapter.AuthorizedRun consumes an existing v9 AuthorizedTrace; observation refinement and join preserve the exact evidence and step sequence; separation receipts (full_visibility_does_not_override_revoked_basis, full_visibility_does_not_supply_missing_authority) reuse the v9 walls: visibility constructs no AuthorizedStep, DynamicStep, or AuthorizedTrace.
• Non-XOR application — BindingSourceAblation factors its TraceDetermined predicate exactly through canonical Determines via the quotient governed-trace view: intact trace fibers remain ambiguous about viability coupling; actual gate ablation strictly refines the observation and determines it. Existing specimens MosaicRelease and CompartmentConflict are retained as directly-checked SCRATCH compatibility wrappers over the canonical core; ConsequencePartition, CollapsedSurface, and WitnessInvariance are bridged by generic adapters; the P25 observation adapter is confined to an explicit Mathlib island.
• Build/audit surfaces — new lean_lib roots ViewSemantics and ViewSemanticsApplications join the default (Mathlib-free) targets; ViewSemanticsMathlibIslands builds explicitly; CI builds all three and runs scripts/check-viewsemantics-footprint.sh (36 receipts axiom-free; BindingSourceAblation exactly [propext, Quot.sound]; P25 exactly [propext, Classical.choice, Quot.sound]; the trace adapter adds no new foundation) and scripts/check-viewsemantics-isolation.sh (shared and application closures Mathlib-free and custody-separated).
• Compatibility cleanup — removes the deprecated LeanProofs.Admissibility.CalculusOne import shim and its calculus_one_compiles marker. The shim was scheduled for removal in 2.0 but retained through v9; v10 completes that breaking cleanup. Downstream imports must use LeanProofs.Admissibility.AdmissibilityKernels and Admissibility.Kernels.kernels_compile.
• Release control — removes the workflow that automatically created a GitHub release when lean-toolchain changed. Toolchain updates can no longer mint an unintended GitHub release or Zenodo deposit; releases remain explicit operator actions.
• Also landed since v9, outside the release claim — SCRATCH incubations (RegulatorRecovery, SelfEntrenchment, BorrowedSpend, SignalAuthority, StatusConversionBinding, CommitmentStanding, ConsolidationController, AffectiveCouplingClassification, expanded NoSilentProjection) and the 2026-07-14 formalization-leads-code doc/header sweep. These ship in the archive because the archive is the tree; they carry SCRATCH custody and testify for nothing.

Non-claims. No information-flow, noninterference, probabilistic-leakage, side-channel, runtime-compliance, or transition-authority claim is made. All ViewSemantics material is UNRATIFIED-CANDIDATE and unwired: the release archives the tree; it is not a custody promotion, and no runtime’s compliance is testified to until a runtime artifact cites named theorems. Inventory: docs/V10-READINESS-LEDGER.md.

9.0.0 — Dynamic Traces and Profile Semantics (2026-07-09)

Dynamic execution over static witnesses, and checker-facing profile semantics.

9.0.0 opens the dynamic-claims campaign: state-threaded traces in which every hop carries the exact static AuthorizedStep witness it consumes — no global Admissible judgment, no free composition — plus a minimal profile-checker semantics specimen for the RRP admissibility-gate prototype (its first named runtime correspondence target).

• DynamicTrace (ANNEX) — DynamicStep wraps the static execution bridge (target state is executeAuthorizedStep, never guessed); AuthorizedTrace threads steps; revoked basis and revoked standing block dynamic steps (revoked_basis_blocks_dynamic_step, revoked_standing_blocks_dynamic_step); mutation-side standing without claim-side authority blocks (step_allowed_without_authority_blocks_dynamic_step); actor-indexed variants (any-actor traces, schedules, traceHopsByActor with actor-attribution theorems); corrective traces; non-amend traces preserve the policy store (non_amend_trace_preserves_policy).
• FreshnessDynamicTrace (ANNEX) — connects dynamic steps to the public metric-time freshness kernel: a stale, expired, not-yet-valid, incoherent, non-preceding, or divergence-excessive observation cannot discharge the current obligation (one theorem per failure mode).
• 1.0 surface, additive — Execution.revoked_standing_cannot_be_authorized_step lifts the derivation-level revoked-standing consequence to the execution layer; kernel manifest updated. No existing 1.0 signature changed.
• RRPProfileSpecimen (UNRATIFIED-CANDIDATE, unwired) — finite symbolic model of profile-checker semantics (Receipt/Claim/ClaimRule/ EffectRule/Profile, deriveClaims, decision): claims derive only through admitting rules; effects require claims; missing / cannot-testify / stale / revoked evidence refuses; profile_id cannot substitute for profile_digest; a requester’s self-witnessed receipt does not testify. Proves nothing about the RRP Python/Rust checkers — it pins the semantics they are supposed to have. RRP citation identifies the intended contract and may enter custody review; it does not prove RRP conformance by itself and is not a prerequisite for formalization.
• DeferredWitness reflection lemma proved (ANNEX) — firstViolation_none_iff_lawful: the executable violation classifier agrees exactly with LawfulCompletion (previously documented as left to the host environment), plus firstViolation_isSome_iff_not_lawful.
• Build/audit surfaces — Mathlib import-surface split: AdmissibilityCustodyAnnex (cheap, Mathlib-free custody target, now in default targets) vs AdmissibilityMathlibIslands (explicit Finset-backed heavy island); default lake build no longer includes the root LeanProofs aggregate (build it explicitly); scripts/check-mathlib-free-targets.sh walks the cheap target’s static import closure and fails closed on Mathlib or heavy-island reach.
• Nine further specimen laws (all UNRATIFIED-CANDIDATE, unwired, formalization leading implementation) — StandingProfileSpecimen (schedule / operator ack / model output are not standing; revocation reaches the derivation; standing is (actor, project)-scoped and non-transferable), WLPAppendAckSpecimen (append acks and publication receipts are custody evidence, never claim authority; volume is not conversion), BridgeCustomsSpecimen (pairwise crossing: source permit alone is no target permit, the bridge claim carries the cap and cannot widen, promotion is digest-addressed, refusals do not cross), ActorTraceSpecimen (actor A’s hop is not actor B’s standing absent an explicit directional transfer rule; a truncated trace is no evidence), LocalBoundaryPressure (concrete hostile instance: dropping MergeAdmissible.left_sound accepts a merge that leaks in one step — the load-bearing field named by construction), ScopedCertification (the quis custodiet seam: certification force is claim-class × scope confined; delegation does not compose for free; self-claims mint nothing; challenge ≠ revocation, filed ≠ admitted; universal authority unrepresentable by construction; the bootstrap — “this profile is rightly active here” — explicitly NOT formalized), SpendabilitySpecimen (the LA seam: eligibility is contractible and never payment, capacity is linear, deposits cite admission, replays refuse, counts conserve — conserved ≠ safe; fork residue: revocation blocks the future, unwinds no effect, refunds no count, erases no record), CustodyFreshnessSpecimen (fresh-here ≠ fresh-there: freshness reads the producer clock only; custody hops never refresh; an absent producer clock is never fresh; the tempting “recently checked somewhere” evaluator is modeled and refuted by inhabited countermodels), TemporalBasis (time assurance for the NQ seam, written before NQ implements its temporal track: freshness is admitted elapsed time under a declared witness contract; a fresh packet does not refresh old testimony; a timestamp proves existence, not current truth; silence never clears; late success is not timely success; a retired source does not come back by time passing; two clocks are not an order without a shared or bridged basis; no GlobalTrustedTime).
• CI widened to the release envelope — explicit lake build LeanProofs AdmissibilityMathlibIslands step plus the repo audit scripts, so “CI green” means “release claim green” after the default-target split.
• Docs wiring (no Lean edits) — three crosswalks with custody classes in every citation and scratch never testifying: docs/RRP-LEAN-CROSSWALK.md (RRP gate doctrine → theorems); docs/AG-TRANSITION-KERNEL-CROSSWALK.md (inverse index into the transition-kernel’s own LEAN_OBLIGATIONS.md ledger, plus folklore corrections against live AG/LA doctrine); docs/NQ-NIGHTSHIFT-CROSSWALK.md (deferring to NQ’s ROADMAP_EXPECTATIONS_FROM_LEAN_KERNEL.md pinning discipline; maps refusal shape, not vocabulary — the runtime and Lean lifecycles are deliberately different cuts).
• Scratch (fenced) — PathVerdict tier-1 extraction continues (StandardObstructions, EvidencePromotionCoverage).

Non-claims: not a unified dynamic calculus and not process semantics or runtime authority (per-hop static witnesses are the whole point); ANNEX modules remain outside the 1.0 compatibility claim; the ten specimen-law candidates (RRP profile, Standing, WLP, bridge, actor trace, boundary pressure, scoped certification, spendability, custody freshness, temporal basis) are candidate formal laws for their runtime seams — they do not testify for RRP or any runtime’s compliance by themselves. Citation/adoption identifies the intended contract. A conformance claim requires an explicit scope and exact correspondence map, executable preservation and transport evidence, and revision-bound qualification receipts. A formal refinement proof may strengthen covered obligations but does not waive those artifacts. Lean custody is independently reviewed; none of these reviews is permission to begin formalization. No JSON/digest/transport/PKI is modeled anywhere in them. Inventory: docs/V9-RELEASE-LEDGER.md.

8.0.0 — Sequent Admissibility Island (2026-07-06)

A Mathlib-free proof-theory specimen/library release.

8.0.0 lands a kernel-checked single-succedent intuitionistic sequent calculus over {atom, ⊥, ∧, ∨, →} in which no structural rule is primitive and all four — weakening, contraction, exchange, cut — are admissible, together with a multiplicity-faithful textbook presentation proved derivability-equivalent to it. The modules live under LeanProofs/ProofTheory/ (custody class UNRATIFIED-CANDIDATE; own Mathlib-free ProofTheory lean_lib, build-graph enforced).

• MembershipG3 — contexts read by membership/subset; one monotone theorem (Γ ⊆ Δ) subsumes weakening/contraction/exchange, size-preserving; general identity derivable (initGen); cut as a computable cut-free transformer (degree-primary, size-secondary induction); consistency and disjunction_property immediate (cut-free by construction).
• TextbookG3ip — multiset-faithful G3ip as lists-quotiented-by-permutation (erasing left rules, multiplicity real, contraction not absorbed); admissible size-preserving exchange; size-nonincreasing inversion package (invAnd/invOr/invImp) funding admissible contraction (contractT).
• Equivalence — textbook_iff_membership (the specimen→textbook direction pays the contraction bill); cut/weakening/identity for the textbook calculus transport as corollaries (cutT, weakenT, initGenT).
• Audit — Audit.lean prints #print axioms receipts in the build: zero user axiom declarations, everything ≤ {propext, Quot.sound}, zero Classical.choice (fully constructive). Two core-library constructivity footguns caught and documented (LeanProofs/ProofTheory/SCARS.md).

Non-claims: not a governance kernel or doctrine unifier (“admissible” is literal Gentzen admissibility, the referent the vocabulary borrows; no Tier/Verdict/cap coupling, no typeclass, no unifier; build coverage is not promotion); not Mathlib Multiset-typed; not height-preserving cut; no proof search; no semantics/completeness; no runtime enforcement. Inventory: docs/V8-RELEASE-LEDGER.md.

7.0.0 — Artifact Authority Profiles (2026-07-02)

A Lean proof release for custody-aware authority semantics.

7.0.0 proves the profile discipline: profiles are local, crossings are paid, receipts are not fungible across obligations, and coverage cannot be minted. Local profiles do not compose for free — holding two profiles’ local material is not holding their cross-profile authority (profile_does_not_compose_for_free); conversion requires a declared paid bridge receipt, with which the crossing composes (cross_profile_conversion_requires_bridge). Stage ascent pays each rung: a stage-n profile does not authorize stage n+1 (profile_stage_noncollapse), and any ascent holds every intermediate rung receipt in custody at any derivation depth (ascent_pays_every_rung). The generic evidence-jurisdiction screen (JurisdictionRespecting, minted on a two-instance family repeat, per-vocabulary and local) makes receipt species non-fungible: the prior local walls are recovered as exact instances (two iffs), receipt cross-use is caught, and the once-escaped relation-promotion attack is caught (relation_promotion_fails_jurisdiction_screen). Coverage cannot be minted: derived evidence funds no obligation its origin could not fund (derived_evidence_covers_no_more), and in single-scoped frames covering k distinct obligations costs k distinct held receipts (coverage_costs_receipts, with an exact-price witness). Coverage through custody is legitimate when paid — the theorem is no bulk discount, not suspicion of broad custody. Non-claims: no shared custody language (no “Constellation Custody Protocol”); no master profile or universal schema (the master screen’s own false positive is demonstrated in-release); no WLP semantics (envelope-only, untouched); no runtime/JSON/AG integration; no profile registry; no issuer-level provenance-correlated portfolio accounting (the named v7.x remainder); no graded “too much coverage” policy screen. Screening, not enforcement. All modules Custody-Class: SCRATCH, CI-covered; footprints ≤ [propext, Quot.sound], no Classical.choice. Release inventory: docs/V7-RELEASE-LEDGER.md.

6.0.0 — Finite Custody Checking (2026-07-02)

A Lean proof release for custody-aware authority semantics.

6.0.0 makes the v5 payment discipline finitely checkable. A Lean-native checker takes a liberal derivation tree and a finite context and returns a typed result — ok with a positional occurrence trace, or a typed refusal naming an offender (CheckResult; no bare Bool on the final surface). The checker is sound (check_ok_sound/checkCtx_ok_sound: ok implies a valid linear derivation over the given context, with read-spine, position-distinct, context-provenant trace) and complete (check_complete) — a decision procedure, not a semi-decision — and its verdict is decided by finitely many count comparisons over the read spine (firstDeficient_decides_check), closing the executable finite-support boundary v5 explicitly left unclaimed. Refusals are never mislabels: the offender’s total demand genuinely exceeds supply (check_refusal_excess), and the offender is genuinely demanded. Beneath the checker, traced and untraced normalization provably agree — same verdicts, the same offender on refusal, residuals equal up to label projection (tracing_preserves_verdicts, linearizeT_ok_projects, linearizeT_forgery_projects): tracing is testimony about payment, never a change to who gets paid. The canonical tagging bridge (untraced_runs_trace_canonically) lifts any plain-context run to a traced run at zero semantic cost. The resident C2 screen layer (DecidableScreens) is claimed into this release surface: executable Bool screens with soundness iffs against the v4 Prop screens — screening as computation, soundness as theorem. Non-claims: not a CLI, not a runtime checker, not Bridge Foundry, not an artifact profiler; not a derivability decision procedure (checks a given tree; no proof search); not a checker for arbitrary future structural systems; not a master admissibility layer; offender identity across the two refusal reporters not claimed. All modules Custody-Class: SCRATCH, CI-covered; footprints ≤ [propext, Quot.sound], no Classical.choice. Release inventory: docs/V6-RELEASE-LEDGER.md.

5.0.0 — Custody-Preserving Normalization (2026-07-01)

A Lean proof release for custody-aware authority semantics.

5.0.0 delivers the normalization layer for the v4 sequent skeleton, with the custody inversion as its thesis: classical normalization removes detours and preserves derivability; custody-preserving normalization removes only policy-licensed detours and refuses when removal would erase payment. A liberal structural derivation normalizes into the custody discipline iff its reads can be paid by occurrences — per-label occurrence counting decides normalization exactly (linearize_ok_iff_counts_suffice); refusal is a typed forgery whose named offender is itself a genuine excess-demand witness (forgery_offender_is_excess). Successful normalization conserves occurrences for every measure (linearize_ok_conserves), preserves the custody chain (chainOf_linearize), and carries a positional occurrence trace proving who paid: each read funded by a distinct original-context occurrence, no occurrence paying twice, nothing paying that was not there (OccurrenceTrace). The same liberal syntax, priced by two disciplines, gets two verdicts: Cartesian derives, linear refuses (cartesian_statable_but_linearly_refused). The starting point is made honest by the already-normal theorem (all_derivs_read_rooted): under the v4 discipline there are no cut redexes — the detours v5 prices are structural (weakening/contraction/exchange), entering as explicit nodes (StructuralNormalization). Non-claims: not full Gentzen cut elimination; not a full structural-rule algebra (node-form linear rules are named follow-up); not runtime; traced-twin coherence and the executable finite-support checker are v6 lane. All modules Custody-Class: SCRATCH, CI-covered, ≤ [propext, Quot.sound], per-slice adversarial audits; see docs/V5-RELEASE-LEDGER.md.

4.0.0 — Custody-Indexed Sequents (2026-07-01)

A Lean proof release for custody-aware authority semantics.

4.0.0 introduces a parameterized indexed-sequent skeleton: the proof discipline for crossing the v3 lifecycle calculi without silently erasing custody. Generalizes the post-v3 sequent ladder (S0–S4) into a proof theory where: structural read discipline is explicit (contraction priced across Cartesian and linear context instances — one rule, one assumption, derivable under one policy and refused under the other); bridge composition preserves provenance (composition_cannot_erase_bridge_evidence); index connectivity does not imply derivability (bridges connect judgments, not indices); route provenance matters (diamond instance; unfunded routes stay closed); master shapes are screened on both faces (MasterFree for universal indices, EvidenceCurrencyFree for universal evidence stamps, each with a detection pair and named screening limits); and derived evidence cannot become universal bridge currency (funding never widens along derivation; universality is inherited, never minted). The capstone, eentail_iff_read_rooted (zero-axiom): derivability with derived evidence is EQUIVALENT to read-rooted normal form — every cross-index derivation roots in read evidence whose original scope funded it.

Custody: the campaign modules (BridgeSequent, ExecutionSequent, ExecutionObligationSequent, BridgeCompositionSequent, CustodyIndexedSequent, StructuralPolicySequent, EvidenceCalculusSequent) remain Custody-Class: SCRATCH — fenced sequent discipline, not promoted kernel authority — and are CI-covered as their own build target (CustodyIndexedSequents; build coverage ≠ promotion). LeanProofs.lean unchanged. No master Admissible; no default bridge transitivity; no runtime claim; structural coverage is read discipline, NOT the full structural-rule algebra; full Gentzen cut elimination is not claimed — the explicit follow-up is v5: Custody-Preserving Normalization.

Inventory with audited theorem receipts: docs/V4-RELEASE-LEDGER.md. Campaign trail: docs/CHANGELOG-scratch-campaign.md.

v3 proved the family. v4 proves the family can be crossed without silently erasing custody.

3.0.0 — Bounded Lifecycle Calculi (2026-07-01)

A Lean proof release for custody-aware authority semantics.

3.0.0 completes the bounded lifecycle-calculi family: the six existing ANNEX bounded calculi (TemporalCustody, SurfaceProjection, RefusalDenial, BoundaryArtifact, ObligationResidue, SafetyPreservation) are joined by three promoted family members — ExecutionCustody (stage separation: ticket accepted / commit attempted / executed / safe / discharged do not collapse), BootKernel (genesis: witnessed settlement, anti-skip wall, no signed-root shortcut, accumulation-is-not-escalation), and CheckpointSettlement (occurrence-linear compaction: mints nothing, conserves live multiplicity, discharges no unknown commit, upgrades no observation to safety) — plus MeasureAccounting (generic conservation engine, support module).

Promotion custody: Scratch → BoundedCalculi/ ANNEX release surface by operator decision 2026-07-01. No promoted kernel/import boundary changed: LeanProofs.lean imports neither BoundedCalculi nor Scratch; the aggregate BoundedCalculi.lean remains a compile marker (checkability/coexistence only — not coherence, not composition, not global admissibility). There is no master Admissible judgment and no default bridge transitivity.

Deferred, named-not-claimed: custody-indexed sequents (v3.x campaign; Sequents 0–3 exist as fenced scratch under LeanProofs/Scratch/ — indexed bridge cut, zero-axiom syntactic no-free-cross-cut, execution-ticket linear sequent, obligation/receipt books; Sequent 4, bridge composition, unbuilt by design) and the longer-horizon custody-indexed Gentzen system (v4, if earned).

Gate record: full build green; audit-axioms / audit-native-decide / check-mathlib-pin / check-witnessed-footprint all exit 0; no sorry/admit; footprints ≤ [propext, Quot.sound], re-attested post-move. Inventory: docs/V3-RELEASE-LEDGER.md. Campaign trail: docs/CHANGELOG-scratch-campaign.md.

v3 proves the family. v3.x starts proving the crossings.

2.0.0 — WDC: model-independent normalization and audit fence (2026-06-29)

2.0.0 promotes Witnessed Derivation Calculus normalization from a freshness-model theorem to a model-independent admitting-class theorem, and hardens the repo’s custody fence.

On the version. This major bump marks the reserved WDC structural milestone — 1.4.0 deliberately spent a minor “to leave the integer 2.0 owed” for exactly this proof-theoretic strengthening (criterion #1 in docs/WITNESSED-FRONTIER-REGISTER.md), which has now landed. The public surface is additive / non-breaking: existing 1.x imports are intended to remain unaffected — bridge_path_normal_form keeps its name, signature, and [propext] footprint. The integer marks the milestone, not an API break.

WDC 2.0 — the structural theorem

• LeanProofs/Witnessed/AbstractNormalization.lean — normal_form_iff_of_commutes (axiom-free): the carry-then-weaken normal-form factorization holds for ANY two-family paid bridge satisfying the local commutation law Commutes C W, independent of the freshness model (Nat, <, b−a).
• LeanProofs/Witnessed/CommutesNecessity.lean — commutes_is_necessary (axiom-free): the commutation law is load-bearing — a concrete system where it fails admits a paid path with no carry-then-weaken factorization. The theorem is genuinely conditional.
• Normalization.bridge_path_normal_form rerouted to be the (CarryStep, WeakenStep) instance of the abstract theorem (perm_weaken_carry discharges Commutes). Name, signature, and [propext] footprint unchanged. Prose: “canonical form” → “normal-form factorization” (existence of the split, not a unique canonical representative).

Audit fence (see docs/AUDIT-POLICY.md)

The repository is not axiom-free; it is axiom-classified. WDC promoted receipts remain footprint-attested.

• Footprint gate hardened (scripts/check-witnessed-footprint.sh): set -euo pipefail, explicit failure if the lake env lean probe fails; 12 ratified receipts attested.
• Repo axiom classifier (scripts/audit-axioms.sh + axiom-policy.tsv): every axiom/constant classified — 23 signature, 0 interface-law, 8 specimen, 0 forbidden, 0 unclassified.
• native_decide classifier (scripts/audit-native-decide.sh): confined to finite-witness modules; forbidden in WDC / kernels / structural receipts.
• mathlib pinned in lakefile.toml to the manifest SHA, with a drift gate (scripts/check-mathlib-pin.sh). Moving mathlib is now explicit.

TaxonomyGraph

• Removed the persistence_normalizes placeholder axiom (a True-bodied claim-shaped stand-in) — demoted to a non-asserting TemporalAttractorSubstrate socket. It was the lone forbidden axiom; the repo axiom census is now 0 forbidden.
• Downgraded the unconditional temporal Δh claim to OPEN (CLAIM-REGISTER #1): static topology neither proves nor refutes it; a conditional version needs an explicit dynamics substrate.
• Promoted the static closure-partition result as the headline: {Δg, Δa}, {Δx}, and {Δh} are three distinct terminal closure families under the declared edge graph. Δh is a terminal family, not the universal sink.
• Edge-policy sensitivity: no_reach_of_closed_lane (axiom-free) packages the negative result as “src inside a forward-closed lane, dst outside ⇒ unreachable”; fenced counterfactual edges (Δm→Δc, Δx→Δc) prove the static result FLIPS under one admitted handoff edge — i.e. it is edge-policy-relative, not universal over all policies.

Boundary / Admissibility

Boundary-related reachability work in this release is supporting infrastructure, not the reason for the 2.0 integer. It claims no Boundary composition calculus, no trichotomy, and no exhaustiveness theorem; RefusedByClosedLane ⇒ ¬Composable is proved in one direction only. A Boundary milestone, if earned later, gets its own name.

Experimental / scratch (not part of the promoted surface)

• A quarantined Persistence Attractor roadmap (experiments/persistence_attractor/NOTES.md) and scratch packaging (LeanProofs/Scratch/PersistenceAttractor.lean, unimported, no axiom/sorry/native_decide). No dynamic Δh theorem is claimed in this release.

Compatibility

Major version marks the reserved WDC structural milestone. Existing 1.x public imports are intended to remain unaffected; the theorem surface is additive/non-breaking.

1.4.0 — Witnessed Derivation Calculus (2026-06-27)

1.4.0 promotes the ratified Witnessed Derivation Calculus into the canonical public surface as the Mathlib-free LeanProofs.Witnessed.* library — no longer only under experiments/. Supersedes v1.3.0-rc1. The stable 1.x Admissibility Kernels surface is untouched.

On the version. The project’s planning docs frame this as “the 2.0 boundary” (V2.0-EXIT-CRITERIA.md), and it ships as 1.4.0 on purpose. Semver is a consumer contract: this release is purely additive — nothing in the 1.x surface breaks — so it is a minor bump, not a major one. The milestone (a second ratified formal object lands in the public surface) gets its volume here and in the release title, not in the integer. A future 2.0 is reserved for a structural strengthening of the calculus — see the “What Would Make This 2.0” gate in docs/WITNESSED-FRONTIER-REGISTER.md.

• A1 — enforced Mathlib-free boundary. New Witnessed lean_lib in lakefile.toml (roots = ["LeanProofs.Witnessed"]). No module under LeanProofs/Witnessed/ imports Mathlib, so lake build Witnessed cannot reach it — the axiom-footprint cleanliness is build-graph-enforced, not merely re-checked.
• Port. The 12-module ratified cone (7 spine + 5 successor) copied from experiments/no_free_lift_wiring/{Wired,Successor}/ into LeanProofs/Witnessed/, namespaced LeanProofs.Witnessed.*, wired into LeanProofs.lean (default target). Renames: Wired.Authority → AuthorityModel (study copy, kept off the [1.0] Admissibility.Authority name), WitnessedDerivation → Derivation, Tightened → Discipline, DisciplineObstruction → Obstruction, tightened_metatheory → discipline_metatheory. The experiment tree is unchanged and remains the provenance record (copied, not moved). Receipt names otherwise frozen.
• Gate 4 — external consumer. LeanProofs/Witnessed/Examples.lean imports only the canonical surface, builds a Lift derivation, and applies no_free_lift / paid_lift_sound — proving the promoted API is usable from outside the cone.
• Gate 5 — footprint regression gate. scripts/check-witnessed-footprint.sh re-attests all 10 ratified receipts against their documented footprints (RATIFICATION-v1.3.md): 6 axiom-free, 2× [propext], 2× [propext, Quot.sound]. Fail-closed — non-zero on build failure, footprint drift, or sorryAx.
• Gate 6 — prose reconciled. README.md, WHAT-THIS-PROVES.md, and the ported file headers updated to the canonical-surface state; the retired-maximal-Admissibility Calculus fence kept visible throughout. Frontier roadmap published as docs/WITNESSED-FRONTIER-REGISTER.md (named, not started; includes the “What Would Make This 2.0” gate).

v1.3.0-rc1 — Witnessed Derivation Calculus (candidate, 2026-06-17)

A candidate experiment surface (experiments/no_free_lift_wiring/Successor/, EXPERIMENTAL-WIRING, NOT in defaultTargets). Public 1.0/1.2 surface untouched. The canonical-surface promotion later shipped in 1.4.0 (above). After the original composition_classification gate was retired (see the entry below), a successor was developed and earned a narrow technical name. Claims + exact theorem receipts: experiments/no_free_lift_wiring/RATIFICATION-v1.3.md.

Earned (compiled, axiom footprints ≤ [propext, Quot.sound], no sorry)

• Witnessed Derivation Calculus — the defined inductive judgment Lift with composition (derivation_extends_along_paid_path), genuine multi-context cut (cut_admissible_general), soundness (paid_lift_sound), provenance (no_free_lift), and non-manufacture (revoked_floor_derives_nothing) — all schematic — plus a canonical-form normalization theorem (bridge_path_normal_form) established for the freshness embedding model. The name is earned by exhibiting the full package in a canonical model, not by an abstract universal normalization theorem.
• Four-axis model-admission discipline WitnessedDiscipline (bridge_valid / semantic_nontrivial / bridge_selective / properly_live) — a filter BESIDE the calculus (Normalization never imports it). The earlier single Discriminating axis is retired by factorization: under BridgeValid it is exactly SemanticNontrivial (bridgeValid_discriminating_iff_semanticNontrivial); bridge_selective adds the genuine, B-dependent teeth it lacked. Inhabited by the canonical freshness embedding (embedding_is_witnessed).

Does not change / does not claim

• Public 1.0/1.2 surface — unchanged. Name is the narrow witnessed-derivation object; “Admissibility Calculus” is not revived.
• Refusal legibility / continuation-bearing refusal (an external agent_gov frontier) is future candidate — no Successor theorem proves it.
• agent_gov correspondences are external implemented-instance / convergent evidence, not a verified reduction, and are not part of the ratification basis.

v1.3.0-rc1 — composition gate prosecuted and retired (2026-06-17)

A status correction, not new public mathematics. The composition_classification promotion gate named in v1.2.0 was attempted and adversarially reviewed (non-Claude, source-grounded, over the quarry copy); the result is a retirement of that target, not progress toward it.

Findings (no public-surface change)

• Attempted and adversarially reviewed the proposed composition gate; semantic bridge validity does not support the intended exclusive classification (naive_exclusivity_fails).
• Retained as durable corrections: arbitrary-length paid-path transport (framed as transport, not a calculus) and the semantic-truth ⊬ derivational-reach separation.
• Corrected the bridge non-closure account (carry-then-weaken; the path is sound, the one-step relation is not closed).
• Demoted the reach-floor closure condition to ordinary graph reachability / ancestor coverage.
• Withheld the word calculus; no successor promotion criterion adopted.

Does not change

• The 1.0 public theorem surface and all its non-claims — unchanged.
• “Calculus of attestation boundaries” was already a destination claim, not a present one. It remains a destination only; the specific gate proposed to earn it is now retired rather than pending. Findings record: experiments/no_free_lift_wiring/COMPOSITION-CLASSIFICATION-TARGET.md.

v1.2.0 — No Free Lift candidate annexes (2026-06-16)

A semantic / governance release, not new public mathematics. It adds fenced candidate and experimental material — shipped with its naming boundaries already corrected — and records a version boundary: the No-Free-Lift work establishes a formal theory of attestation boundaries, not yet a calculus.

Adds

• Fenced UNRATIFIED-CANDIDATE annexes in LeanProofs/Admissibility/: NoFreeLift.lean (the paid-bridge-closure spine) and CarryLaws.lean (the two coordinate cost laws). Axiom-free, unwired (not imported by LeanProofs.lean), committed 94df70e.
• A fenced experiments/ tree (Custody-Class: EXPERIMENTAL-WIRING, its own Lake project, not imported by the canonical surface) containing no_free_lift_wiring/ — the spine wired to modeled freshness/authority embeddings — with its audit (WIRING-AUDIT.md) and a ratification template (RATIFICATION-PENDING.md) coupled to the code.
• COMPOSITION-CLASSIFICATION-TARGET.md — names the theorem (composition_classification) required to promote the work toward any future “calculus of attestation boundaries” claim.

Changes (experimental wiring de-placarded before release; no proof changed)

• Wired.Contraction → Wired.BudgetMonotonicity (proves the metric budget law, not the structural contraction rule).
• Wired.Composition → Wired.CoCompilation (proves co-compilation True, not a composition result).
• composition_builds → modules_cocompile.
• Removed a "calculus is legal for this object" overclaim from the aggregator docstring. Old names retained only as provenance notes.

Does not change

• The 1.0 public theorem surface (AdmissibilityKernels, the eight [1.0] modules) and all its non-claims — unchanged. This release adds material; it does not correct any public-surface “calculus” drift, because there was none.
• Ratification status: nothing promoted.
• No present-tense “calculus” claim; no substructural claim; no substantive composition theorem.

Status

• No Free Lift is canonical-tracked / candidate, not canonical-ratified.
• “Calculus of attestation boundaries” remains a destination claim, gated on composition_classification (theory → calculus → substructural → conditional model→world; see the target doc). The word is not earned yet.

This site is open source. Improve this page.