Archived at the v13 custody boundary. This is a chronological record of the paths and labels under which the v3-v7 campaigns originally landed. It is not a current source map. The released public substrate now lives under
LeanProofs/CustodyIndexed/, its finished fixtures underLeanProofs/CustodyIndexed/Evidence/, and live incubation in the sibling skunkworks. Exact pre-migration source remains in the v12 tag and Git history. SeeV13-RELEASE-LEDGER.md.
LeanProofs/Scratch/PathVerdict/{Core,Edges}.lean (new, extracted),
lakefile.toml (CI roots). NOT part of the v7.0.0 release surface — the
v7 tag point precedes this commit.
PathVerdict δ: authority IS the empty log; no clean|blocked
garbage states), core-kernel/domain-parameter split (ObstructionKind δ
— not a junk-drawer enum, not an unconstrained parameter), edge layer +
fold with the tether theorems (fold_authority_iff,
authority_append_iff, render_clean_iff_authority — renderers can
decorate, they cannot mint admissibility).Admissibility/PathVerdict/ target is the eventual
PROMOTED home — operator ceremony, not this landing). Header carries the
Tier-1 scope brutality (the does-NOT-prove list) and the C3 overlap note
(verdict algebra ≠ sequent walls ≠ jurisdiction screen: adjacent
doctrine, disjoint proof objects; any bridge is its own slice).LeanProofs/Scratch/JurisdictionScreen.lean (extended in place). Codex
first-pass GREEN. Answers the release-boundary question (“is multi-currency
a v7 blocker?”) by SPLITTING it into three faces and building what is
buildable, instead of deferring wholesale:
derived_evidence_covers_no_more, zero-axiom, codex: strongest — “closes
the derivational widening face for all chain lengths with no extra frame
assumptions”): whatever obligation a derived receipt can fund, its origin
could already fund — one line via the resident anti-currency law
(echain_funding). A portfolio cannot be widened by derivation; the
obligation-indexed sibling of stamps_are_inherited_not_minted. Plus
operational_power_is_declared (respecting ⇒ funding power ⊆ declared
scope).SingleScoped opt-in
frame property + coverage_costs_receipts, Mathlib-free pigeonhole with
local erase lemmas): covering k distinct obligations requires k distinct
receipts. Concretely on the combined frame (mFrame_single_scoped):
three_obligations_cost_three_receipts (lower bound) +
three_receipts_cover_three_obligations (exactness witness, codex-
suggested) — three obligations cost EXACTLY three receipts. Custody
assembly is not an attack inside this skeleton: evidence enters only by
assumption, so every held receipt was individually acquired.UniversalReceiptFree; a graded threshold screen deliberately
NOT built (arbitrary, FP-riddled); the genuinely open remainder is
ISSUER-LEVEL provenance-correlated accounting — needs a provenance model
this skeleton does not have; named for v7.x, not silently deferred.LeanProofs/Scratch/JurisdictionScreen.lean (new; ≤ [propext, Quot.sound],
most theorems zero-axiom incl. the capture), lakefile.toml (CI root), Zoo
(mechanism 6 registered; escaped-animal record CLOSED; two new rows). Codex
first-pass GREEN — emperor check passed explicitly (“screen-shaped…
screening, not enforcement”).
AdmissionJurisdiction and slice
2’s StageStepDiscipline proved the same structural failure under two
vocabularies before this screen was allowed to exist.JurisdictionFrame (per-vocabulary, LOCAL: demands
classifies conversions to obligations, scopedTo is opt-in — no default
fungibility) + JurisdictionRespecting. Derivational faces:
conversion_requires_jurisdiction_receipt and
unmatched_context_cannot_convert (codex: strongest — “lifts the
rule-local screen through derivations via rootedness”: nothing in
custody scoped to the demanded obligation ⇒ underivable at any depth).admission_jurisdiction_iff_jurisdiction_screen,
stage_step_discipline_iff_jurisdiction_screen; pass/fail corollaries
recovered one-line from resident theorems (clean systems pass;
parse-implies-authority, season-pass skip fail; self-promotion fails
this screen TOO — the base-only variant that evades mechanism 3 does not
evade this).relFrame +
relation_promotion_fails_jurisdiction_screen — the C3 audit’s
relation-promotion attack, which satisfied the discipline and evaded
every screen resident at audit time, fails the minted screen; the clean
relation system passes (non-vacuous, codex-confirmed). One day:
escaped (C3) → cornered (slice 1) → caught (slice 3).bridgeAsRung and rungAsBridge cross-use cages — both SATISFY the
discipline (load-bearing-negative family members 4 and 5), both fail the
screen; combined_universal_receipt_free (total-form only — codex:
“should not be read as solving broader multi-currency”; the
many-but-not-all currency face stays open and gated).UniversalReceipt/UniversalReceiptFree +
disjoint_scopes_forbid_universal_receipt — the god-currency signature
at the receipt layer, total form.LeanProofs/Scratch/ProfileStages.lean (new; ≤ [propext, Quot.sound],
several zero-axiom, no choice), lakefile.toml (CI root), Zoo (two registry
rows). Codex first-pass GREEN.
ascend n: profile n + rung n
→ profile n+1). profile_stage_noncollapse — the gap-spec §4
theorem: without the n→n+1 receipt, stage-(n+1) standing is underivable,
any depth, any context, every n.ascent_pays_every_rung (codex: strongest) — the strong wall via a
Rooted induction: any derivation of profile k either assumed it or
climbed from a held profile j with EVERY rung in [j, k) literally in
custody. No skipped rung, no bulk discount. (Profile-level analog of
BootKernel’s anti-skip wall — cited, not duplicated.)paid_rung_ascends, two_rungs_ascend_two (two stages
cost two receipts, concretely).selfPromote: standing cited as its own
promotion evidence) — caught by resident mechanism 3, two lines
(self_promotion_violates_discipline); base-only-variant caveat
recorded per codex (it would evade mechanism 3 and fall to the step
condition — why both catches exist).skip: one receipt promotes two stages) —
SATISFIES the discipline (skip_satisfies_discipline, the
load-bearing-negative family’s third member), teeth demo
skip_ascends_two_for_one, caught by LOCAL StageStepDiscipline
(skip_breaks_step_discipline).StageStepDiscipline
is the SECOND local evidence-jurisdiction condition (after slice 1’s
AdmissionJurisdiction; genus named by the C3 relation-promotion
audit). The local wall now provably repeats across v7 slices — this is
the repeat evidence the generic screen’s admission decision asked for
(V7-GAP-SPEC §4). Generic screen still gated on operator admission.LeanProofs/Scratch/ArtifactProfiles.lean (new; entirely zero-axiom),
lakefile.toml (CI root), LeanProofs/Scratch/Zoo.lean (registry row +
escaped-animal status update), docs/V7-GAP-SPEC.md (RATIFIED by operator
2026-07-02 with the §9 failure-class wording amendment + explicit
no-registry non-goal). v7 “Artifact Authority Profiles” OPENS per the
ratified gap spec §10: the refusal skeleton, NOT the profile schema.
profile_does_not_compose_for_free — both profiles’ local material
in custody, no bridge receipt: observer verdict derives, admission does
NOT. cross_profile_conversion_requires_bridge — with the bridge
receipt the crossing composes (two-cut chain); the only difference is the
paid receipt. admission_requires_jurisdiction_receipt — the general
wall (codex: strongest of the slice).no_master_profile (MasterFree at the profile index) + — per codex
YELLOW finding, the screen’s scope limit DEMONSTRATED rather than
footnoted: two_way_profiles_fail_master_screen — a fully PAID
two-way bridge pair fails the index-level screen while satisfying the
discipline (two_way_profiles_satisfy_discipline): the resident
benign-router false positive instantiated at the profile level. Failing
MasterFree is a smell, not a conviction.parseAuthority:
foreign receipt cited directly as admission evidence, no bridge; true
minimal pair; codex: “real laundering specimen, not a strawman”).
parse_authority_satisfies_discipline — the load-bearing negative:
the attack launders inside EvidenceNeverConcluded, the relation-
promotion shape again. Catch: AdmissionJurisdiction (LOCAL
evidence-jurisdiction condition, explicitly the local face of the
still-gated general screen; observer side explicitly out of scope per
codex) — clean satisfies, attack breaks at the named rule
(parse_authority_breaks_jurisdiction). The C3 escaped animal is
CORNERED (local face caged), not caught (generic screen still gated).LeanProofs/Scratch/FiniteSupportChecker.lean (new), lakefile.toml (CI
root). v6 initial scope COMPLETE (both admitted slices landed same day the
lane opened). Codex first-pass GREEN; its weakest-theorem note (trace
provenance not public) closed same-slice with resident machinery.
CheckResult
(ok positional-trace | refusal offender); Core.check (tagged context);
Core.checkCtx (PLAIN finite context — tags canonically via slice 1’s
bridge, caller supplies no positions, still receives positional
testimony); firstDeficient (the counts-only decider, Option J — no
derivation built).check_ok_sound / checkCtx_ok_sound): ok ⇒ the untraced
normalizer succeeds and delivers a linear Deriv over the GIVEN context,
trace labels = the read spine, trace position-distinct. Codex: “real
soundness, not just verdict agreement… no circularity — untraced
linearize is the independent anchor.”check_refusal_excess / checkCtx_refusal_excess
/ check_refusal_offender_demanded): a refusal names an offender whose
total demand genuinely exceeds supply, and the offender is genuinely
demanded. Never a mislabel.check_complete): sufficient counts on the finite
support ⇒ accept. Soundness + completeness close the checker into a
DECISION PROCEDURE for this skeleton, not a semi-decision.firstDeficient_decides_check,
with support_covers_iff_all_covers): the verdict is decided by finitely
many count comparisons over readsOf — the v5 decision theorem’s
infinite-label quantifier (∀ l : J) reduced to the finite read support,
discharging the boundary v5 slice 3 explicitly left unclaimed.checkCtx_trace_entries_from_context, codex-
suggested, closed with resident trace_mem_initial): every accepted
trace entry is an occurrence of the tagged context; every traced label
was genuinely in the given context.check’s
traversal offender and firstDeficient’s scan offender may DIFFER
(reads [a,b,a,a] vs supply [a,a]: traversal refuses b, scan flags a);
both are proved excess witnesses; offender identity across reporters
deliberately not claimed.LeanProofs/Scratch/TracedCoherence.lean (new), lakefile.toml (CI root).
v6 “Executable Custody Checking” CAMPAIGN OPENED (new surface,
operator-admitted 2026-07-02; gap spec ChatGPT-drafted, operator-ratified;
hard prohibitions recorded in .governor/loop.json). Codex first-pass GREEN.
linearizeT_ok_projects — traced success projects: untraced twin succeeds
on the label projection, residual = projection of traced residual, linear
Deriv delivered.linearizeT_forgery_projects — traced refusal projects with the same
offender (refusal identity, not mere refusal existence; codex: “the l
is fixed on both sides”).linearizeT_ok_iff_linearize_ok / linearizeT_forgery_iff_linearize_forgery
/ tracing_preserves_verdicts — the verdict iffs and the packaged
no-new-cases theorem (scope items 1a/1c).trace_refines_untraced_run — the refinement package (scope 1b); codex:
strongest of the slice.tagFrom/tagged (+ tagged_map_snd, tagged_unambiguous,
count-level, no choice) and untraced_runs_trace_canonically: every
untraced run on a plain context lifts to a traced run, same verdict, same
offender, position-distinct trace. Slice 2’s checker consumes this to
accept untagged input and return positional testimony.Core + remover-projection
lemmas; reverse coherence by total result-case exhaustion.LeanProofs/Scratch/OverlapAudits.lean (new; entirely zero-axiom),
lakefile.toml (CI root), LeanProofs/Scratch/Zoo.lean (registry row +
escaped-animal record). A C3 run instantiates a candidate primitive as a
System and checks its claimed wall against the resident kernel; output is
an AUDIT VERDICT (instance → deflate/cite; delta → name precisely, build
stays gated), never a kernel.
derived-relations-need-witnesses
candidate, tooltheory 2026-06-19). Two-sided verdict:
relation_requires_relation_receipt; the Zoo mechanism-5 genus) AND —
after codex caught the first draft flattening endpoint-evidence and
relation-evidence into one index — the resident index-closure machinery
(relation_wall_is_closure_instance via no_free_cross_cut_generic).
The replay pair endpoint_verdicts_do_not_yield_relation is the
candidate’s law verbatim: verdict(A) ∧ verdict(B) derivable, relation
NOT.promote_discipline), is no universal stamp, and
promote_breaks_closure names exactly where the would-be screen lives
(an evidence-jurisdiction condition of the closure genus). Screen
unminted — then recorded as forcing-consumer gated per the candidate’s
own fences (policy superseded 2026-07-14; consumers no longer gate
formalization);
un-owned delta = cannot_testify as an output verdict type. Recorded
in the Zoo as the first KNOWN ESCAPED ANIMAL.silence_as_denial_violates_discipline), codex:
“correct mechanism ID.” Wall replay silence_records_without_denying
(timeout recorded ∧ denial underivable). AuthenticatedDenial.lean stays
the protocol-face home; Zoo registry row added.iEndpointEvid/iRelEvid),
closure-instance + closure-violation theorems added, promotion family
mirrored (promoteSym — src/evid asymmetry is an encoding artifact),
meta-verdicts labeled as such in the header. Strongest:
relation_requires_relation_receipt / denial_requires_signed_witness;
weakest: promote_not_universal (narrow by design); proof-shape class:
finite constructor exhaustion + rooted-collapse underivability.LeanProofs/Scratch/CaveatSequent.lean (extended in place — file stays
entirely zero-axiom; first draft leaked propext through Nat.le_max_left,
fixed by bounding fresh caveats with foldr-add instead of foldr-max),
LeanProofs/Scratch/Zoo.lean (registry row; C1 inventory COMPLETE),
docs/ZOO-TEMPLATE.md (inventory statuses swept).
BlindDemand (∀ cs, funded — total blindness), CaveatBlindFree (the
screen), BurdenRespecting (discipline-grade: every funding instance
forces cs ⊆ A; catches partial blindness too — codex: “the real
discipline-grade condition”). Bridge burden_respecting_caveat_blind_free
via exists_fresh_caveat: burden space unbounded vs finite acceptance
lists — NO degenerate escape, unlike the currency screen’s one-obligation
system.blind_discipline): the blind specimen SATISFIES
EvidenceNeverConcluded — blindness launders inside the custody
discipline, so no wall replay could cage it; a new screen was necessary.
(Docstring precision on this fixed per codex YELLOW→addressed: the theorem
proves exactly the discipline predicate, not “all v4 walls”.)blindSystem, fenced FORBIDDEN, true minimal pair —
fund retained, blindGate the only addition): use [] funded at every
burden set. Caught twice (blind_system_not_caveat_blind_free,
blind_system_not_burden_respecting); teeth demo
blind_system_funds_unaccepting_use — the F3 sequent wall FAILS in the
blind system (same context, same use as caveat_minimal_pair, opposite
verdict).unburdened_evidence_is_universal_stamp,
cav_system_not_currency_free): the CURRENCY screen fires on the CLEAN
caveat system — ev [] honestly funds every use (no strings attached ≠
god-currency). Scope fact, codex-confirmed defensible: screens have home
vocabularies; porting one across vocabularies without re-derivation is
itself a laundering move.burden_respecting_caveat_blind_free (“the clean
diagonal reason”); weakest blind_discipline (prose, fixed); proof-shape
class: first-order constructor inversion + finite-list freshness
diagonalization, two countermodel witnesses (blindGate, ev []).LeanProofs/Scratch/Zoo.lean (extended in place). Entire slice zero-axiom
(all 20 new theorems #print axioms-clean); codex first-pass GREEN.
ExecutionCustody.ticketSpent_does_not_imply_didExecute),
commit-attempted-as-executed
(ExecutionCustody.commitAttempted_does_not_imply_didExecute),
checkpoint-as-discharge
(CheckpointSettlement.checkpoint_cannot_discharge_unknown_commit),
observation-as-safety
(CheckpointSettlement.checkpoint_cannot_upgrade_observation_to_safety).entail_iff_rooted); the wall replay
pair (record derivable ∧ outcome underivable — the ANNEX statement’s
X ∧ ¬Y as a derivability conjunction); FORBIDDEN specimen = clean + ONE
record-as-evidence rule, caught by discipline unsatisfiability (the
summary-as-authority mechanism, reused).execution_requires_substrate_receipt' (arbitrary Γ,
attempts derivable, execution still receipt-rooted); weakest
substrate_receipt_funds_execution (intentional non-vacuity witness);
proof-shape class: finite-rule skeleton replay via
EvidenceNeverConcluded + entail_iff_rooted.CaveatBlind screen design (next).LeanProofs/Scratch/OccurrenceTrace.lean (new), lakefile.toml (CI root).
List (Nat × J)); linearizeT (the traced twin
of linearize, deterministic by construction — a function, no choice)
pays each read with the first occurrence carrying the demanded label and
RECORDS the consumed (position, label) pair, in read order.linearizeT_ok_conserves): for every measure,
context = trace + residual; trace_determines_consumed_multiset reads it
at pair indicators — the trace IS the consumed multiset.trace_labels_are_reads):
trace.map snd = readsOf, in order. Labels explain what was read;
occurrence traces prove who paid.linearize_trace_occurrences_distinct):
unambiguous input positions ⇒ no position appears twice in the trace —
two distinct reads cannot be funded by the same original occurrence.linearize_trace_occurrences_from_initial_context, trace_mem_initial):
every traced payment is an occurrence of the initial context (count +
membership forms; one_le_count_iff_mem helper).same_label_distinct_occurrences_traced):
tagged [(0,res),(1,res)] normalizes with trace exactly [(0,res),(1,res)]
— equal labels, distinct recorded payments; a single tagged occurrence
still forges (free_contraction_still_forges_tagged).linearizeT_ok_conserves. Docstring
fixes applied. Everything ≤ [propext, Quot.sound].LeanProofs/Scratch/LinearNormalization.lean (extended in place).
counts_suffice_for_linearize): sufficient
per-label occurrence counts ⇒ linearize succeeds. First-match is
order-safe because consumption is by-label (a read of one label never
removes another’s occurrences) — no ordered-supply hypothesis needed;
codex confirmed no fairness hole.linearize_ok_iff_counts_suffice): success ⟺
every label’s demand ≤ supply. One iff — the completed decision boundary
(semantic; executable finite checker is v6 lane).forgery_offender_is_excess): on refusal, the
NAMED offender label’s demand genuinely exceeds supply — the offender is
a witness, not a symptom (validity, not uniqueness/minimality).
linearize_forges_iff_excess packages the refusal side as an iff.removeFirstC_isSome, removeFirstC_none_count_zero.LeanProofs/Scratch/LinearNormalization.lean (new), lakefile.toml (CI root).
Core) can STATE free contraction; linearize
(computable, partial) pays every read with a distinct first-match
occurrence, threads residuals, and returns ok (a linear Deriv) or
forgery offender.linearize_ok_conserves): on success, context = reads +
residual for EVERY measure — payment neither erased nor duplicated.
chainOf_linearize: the evidence spine survives (labels + order).excess_demand_forges): demand above occurrence
supply for any label FORCES refusal — accounting-tied (via the conservation
law), not constructor-shaped; the offending trees are statable (codex
confirmed).linear_pay_twice_normalizes /
linear_free_contraction_cannot_normalize — same tree shape, same read
labels; two occurrences fund, one occurrence forges.
occurrences_not_labels packages it. pay_twice_consumes_both: both
occurrences consumed on success.cartesian_statable_but_linearly_refused):
the free-contraction tree embeds into the Prop layer under Cartesian and is
refused by linearization.normalize_refuses_payment_erasure = excess_demand_forges; the
chain/occurrence bar split across chainOf_linearize +
linearize_ok_conserves); named remaining before v5.0.0:
sufficient-count COMPLETENESS (counts suffice ⇒ ok) and a positional
occurrence trace (exact offender identity). Classical.choice intrusion
caught and purged; everything ≤ [propext, Quot.sound].LeanProofs/Scratch/StructuralNormalization.lean (new), lakefile.toml (CI
root).
SDeriv = derivation
trees with explicit wk/ctr/exch detour nodes; normalize eliminates
every structural node by membership TRANSPORT pushed to the ax leaves
(termination free — structural recursion; normality by TYPE — output is
Core).chainOf_normalize): the custody spine is
preserved as LIST EQUALITY — one equation refuting erasure, reordering, and
synthesis. The round trip (normalize_read_rooted, zero-axiom):
normalized output re-enters the v4 read-rooted class; reflection
(Core.toEntail) puts every v4 wall in scope of normalized output.chainOf
preserves labels/order, not ax-occurrence identity. Slice 2 target
locked: the linear layer, occurrence-sensitive spine, policy-paid
weakening/contraction — where free contraction FAILING to normalize is the
theorem.LeanProofs/Scratch/DerivationData.lean (new), docs/POST-V4-CAMPAIGN.md
(F6/F7 recorded), lakefile.toml (CI root).
all_derivs_read_rooted over reified derivation trees (Deriv), with the
reflection pair (eentail_iff_nonempty_deriv), purity of evidence
sub-derivations, and chainOf — the evidence chain as data, named as THE
invariant v5 normalization must preserve. v5 scope locked: structural
nodes create the detours; normalization returns to ReadRooted preserving
chainOf.LeanProofs/Scratch/DecidableScreens.lean (new), lakefile.toml (CI root).
DecSystem: finite systems as boolean rule tables + complete enumerations.
Every v4 screen gets an executable Bool version with a PROVED soundness iff
against the Prop screen: fundableB/universalStampB/
evidenceCurrencyFreeB/crossBridgeB/substantiveB/
universalCrossroadsB/masterFreeB.MasterFree
by decide; the sink PASSES — sink_master_free_by_decision is a
MasterFree proof obtained by computation + iff, not hand case analysis;
the stamp system fails the currency screen likewise. The proof-native seed
of the v6 checker.Classical.choice crept in via by_cases on undecidable
Props and was purged (Bool-cases on the executable screens instead) —
everything within [propext, Quot.sound]. Kernel decide only; the native
decision procedure stays forbidden. Walls (derivability itself) are NOT
decided here — v6 work, stated.LeanProofs/Scratch/Zoo.lean (new), lakefile.toml (post-v4 files + zoo
added to the CI lib roots — the coverage rule, applied on schedule this time).
EvidenceNeverConcluded — it forfeits
every v4 wall visibly. Clean neighbor: logs exist, logs fund nothing
(clean_summary_discipline). Log emission does not prove authorization.hubSystem (A⇄H⇄B full
mediation) caught; TRUE minimal-pair contrast sinkSystem (drop only the
outbound rules — receiving from everyone is not mastery; mediating every
pair is) passes the screen.CaveatBlind screen design before its cage.LeanProofs/Scratch/CaveatSequent.lean (new; entirely zero-axiom; codex
first-pass GREEN — first of the campaign), docs/AG-AUDIT-CHECKLIST.md (F4),
docs/ZOO-TEMPLATE.md (F5).
step_shape) IS
burden-monotone. One law, two faces: Δt (funding narrows as budget decays)
and caveats (burdens grow as evidence derives).
admissible_steps_grow_caveats (one-shot, the F1/F2 pattern);
caveat_dropping_is_inexpressible (cleansing requires new evidence, never
derivation); derived_evidence_inherits_caveats (chains);
burdened_evidence_cannot_fund_unaccepting_use +
all_burdened_context_cannot_fund_unaccepting_use (audit-requested
context-general wall); positive + minimal pairs. Closes the parked 4th
refusal slice (burden preservation under derivation; boundary transfer
explicitly out of scope). Named unscreened attack: caveat-blind demand
(CaveatBlind screen = follow-up).stampSystem and
fluentSystem.LeanProofs/Scratch/FluencySequent.lean (new). Entire file zero-axiom.
reliance_roots_in_provenance): under ANY evidence
calculus over the clean system, a derivation of mayRely c either assumed
reliance outright or holds provenance c literally in context. Confidence,
recall, and claims cannot be the root. HighConfidence ⊬ MayRely as a
two-case normal form, at any depth.confidence_cannot_be_upgraded_to_provenance, via
the one-shot steps_into_provenance_come_from_provenance + chain version):
no evidence calculus can derive provenance from confidence — provenance
requires its own read, at every confidence level. Fluency ⊬ Provenance,
constructively.high_confidence_does_not_mint_may_rely,
recall_does_not_authorize_reliance) + the positive pair
(provenance_funds_reliance).fluentSystem, fenced FORBIDDEN): the clean system
plus claim-blind sway rules — nothing dropped (codex caught the first
draft narrowing the obligation space; fixed to a true one-family minimal
pair). Confidence becomes a UniversalStamp; the currency screen catches
the system. A system that lets fluency fund reliance has installed a
universal currency, and the screen names it.mayRely.LeanProofs/Scratch/DeltaTSequent.lean (new), docs/POST-V4-CAMPAIGN.md
(new — ratified F1–F7/C1–C3 ordering, deferred list, the binding guard).
Post-v4 work; v4.0.0 was tagged and released clean (CI green, DOI minted)
before any of this landed.
step_shape) IS freshness decay. Evidence carries a
remaining-validity budget; a tick spends one unit; demanding uses require
minimum remaining budget.refresh_is_inexpressible, zero-axiom): no
evidence calculus over the Δt system can contain a refresh step — the
discipline’s law makes it UNSTATABLE, not merely refused. Renewal requires
new evidence (a new read), never derivation from the old. Generalized per
audit to the full characterization admissible_steps_decay /
admissible_chains_decay (zero-axiom): ANY admissible step into evidence
comes from evidence with at least as much budget, for every calculus over
the system.stale_context_cannot_derive_demanding_use, zero-axiom):
stale-holding contexts cannot derive demanding uses at any depth — proved
through the read-rooted machinery (roots-in-read + chain decay +
membership). Cartesian policy; linear version named follow-up.delta_t_exploit_blocked): same origin — the aging
chain ev R →* ev (R−n) exhibited, not asserted — funds at hold time,
refused after elapsed time. Valid-then ⊬ valid-now, formally.CHANGELOG.md (4.0.0 entry), README.md (v4 current release),
WHAT-THIS-PROVES.md (v4 section), docs/V4-RELEASE-LEDGER.md (new),
CITATION.cff (title/version/abstract — the 1.0-era “not a sequent calculus”
non-claim explicitly re-scoped to the stable kernel surface, where it remains
true), lakefile.toml (version 4.0.0; new CustodyIndexedSequents lean_lib +
default target so the release object is CI-covered — the v3 lesson applied;
build coverage ≠ promotion, modules remain SCRATCH),
docs/ROADMAP-bounded-calculi.md (both releases recorded; v5 campaign named).
LeanProofs/Scratch/EvidenceCalculusSequent.lean (new; additive). Codex
verdict: GREEN — v4 EARNED.
EvidenceCalculus = a step relation with two laws —
step_shape (funding never widens along derivation: the rule relation is
the sole authority map; derivation navigates it, never extends it) and
step_targets_evidence (steps produce evidence only — fences the
derive-to-target bypass, a real hole found and closed at design time).
EEntail adds a derive rule to the policy-parameterized sequent;
derivation inputs are paid through the context policy.echain_funding (funding monotone
backward along chains); stamps_are_inherited_not_minted (universality
cannot be manufactured, only inherited — one line, the depth lives in the
laws); derivation_funds_only_what_origin_funded (every crossing consuming
derived evidence traces to a read origin whose original scope included that
crossing — existential inclusion, honestly scoped per audit);
eentail_iff_read_rooted (audit-requested capstone: derivability ≡
read-rooted normal form — every cut at any depth structurally carries its
read origin, chain, and funding; no derivation shape lacks its custody
chain).UniversalStamp (shape inspection — the rule relation at the
evidence position, not index topology); EvidenceCurrencyFree (universality
exists only degenerately). Detection pair: fenced FORBIDDEN stampSystem
caught (stamp_system_not_currency_free), diamond clean
(diamond_no_universal_stamp). Named false negative: multi-currency
evidence below the universal threshold (consumer policy question).EEntail requires the
evidence calculus to respect the index set (hstepclosed); over-wide rule
relations are honest authorization, not laundering.LeanProofs/Scratch/StructuralPolicySequent.lean (new; additive — the audited
skeleton is untouched and recovered as an instance)
ContextPolicy abstracts
the one operation both disciplines share — Reads c j c' (“obtain a
judgment, leaving a residual”) — with two laws; PEntail threads residuals
through both premises of every cut (Γ ⊢ j ⊣ Γ'). Cartesian instance:
reading is free. Linear instance: reading is ResourceSequent.Consumes.cartesian_contraction_free derives from
a single occurrence; linear_contraction_priced proves the SAME derivation
impossible under the linear policy; linear_pay_twice shows two occurrences
fund it. Contraction is a policy with theorems, not an assumption. Plus
linear_depletion (monotone) and linear_every_derivation_pays (strict,
audit-requested: nothing derives for free).pentail_iff_rooted),
provenance chains (pentail_provenance — each hop’s evidence obtained by a
licensed read at its thread state), closed-index wall. Zero-axiom core.pentail_cartesian_iff, zero-axiom, bidirectional
induction): the parameterized skeleton collapses to the audited Entail —
S4 and the diamond recover compositionally.LeanProofs/Scratch/CustodyIndexedSequent.lean (extended; operator ruling: no
interim DOI, plow through)
crossroads_mediates_every_pair
states the god-calculus signature; s4_master_free proves the S4 system
clean by finite case analysis (codex: non-vacuous). Honest caveats in-file
per audit: this is universal-hub screening, not anti-authority
enforcement — false negative = evidence-currency master (an evidence-only
token funding every bridge; EvidenceCurrencyFree screening named as
follow-up), false positive = benign router (index-level screening
over-approximates).diamond_unfunded_route_closed (reaching the target one way does
not open the other way; uses the discipline).index_connectivity_does_not_imply_derivability — A→B and B→C hold at the
index level, everything funded, composite still underivable because the
midpoint judgments differ (b1 produced, b2 consumed). Bridges connect
judgments, not indices; index analysis is a smell detector, not a
conversion license. Zero-axiom.LeanProofs/Scratch/CustodyIndexedSequent.lean (new; post-v3.0.0; does NOT tag
v4 — release classification is the operator’s)
System (J, Ix, ix, Rule) + generic Entail.
ONE discipline condition — EvidenceNeverConcluded (no rule concludes an
evidence judgment) — yields by induction, for every conforming system:
evidence enters only by assumption (generic no-default-transitivity: nothing
can synthesize evidence, composite or otherwise); entail_iff_rooted, the
normal-form theorem — derivability is EQUIVALENT to evidence-rooted
chaining, i.e. no derivation shape exists in which a cut’s evidence is not
in custody, at any depth (the “cut cannot erase bridge evidence” target in
characterization form); provenance chains as first-class enumerable lists;
the generic index-closure wall (needs no discipline at all); weakening
declared as the Cartesian polarity (linear contexts = resource lane, named).s4_entail_iff bidirectional,
rule-for-rule; the generic machinery replays the specimen’s provenance and
no-synthesis theorems. ENTIRE FILE ZERO-AXIOM (not even propext).MasterFree predicate is v4 design work); multi-role exclusion stated
(derived certificates / evidence-producing subcalculi — the validator shape
— are the other v4 frontier).LeanProofs/Scratch/BridgeCompositionSequent.lean (new; post-v3.0.0, opens the
Custody-Indexed Sequents campaign)
BoundaryArtifact.MayMint, exposure class). Five calculus
indices; deliberately no bridgeTB index for a composite to live in; no
rule concludes evidence of any kind.composition_cannot_erase_bridge_evidence
(every mint traces to its full custody chain; bounded-normal-form scope
stated per audit), mint_without_downstream_axioms_requires_all_three
(audit-requested forcing version: strip the assumed-outright escape hatches
and all three evidences are mandatory), no_free_transitivity,
first_bridge_alone_does_not_compose (deriving hop one accumulates zero
boundary authority), and the S1 temporal wall re-established under the
extended rule set (each new cut pays its preservation case).[propext]: TS cut consumes the temporal premise (S0 discipline);
SB cut discharges from boundary evidence alone — declared as the
non-transitivity content; codex ruled the pairing premise syntactically
load-bearing (deleting it collapses the provenance chain).sealed_boundary_evidence_unsatisfiable);
soundness never converts.lakefile.toml, WHAT-THIS-PROVES.md, README.md, CHANGELOG.md
BoundedCalculi/ — the LeanProofs lib owns only its root module, which
deliberately does not import the aggregate — so the v3 release surface was
invisible to lake build/CI (explains the earlier full-build-green-while-
scratch-broken anomaly). Added a BoundedCalculi lean_lib + default target;
bumped package version to 3.0.0. Build coverage, not promotion: the
LeanProofs.lean boundary is unchanged. Scratch/ stays uncovered by
design (compile-is-contact, checked per-file by the campaign loop).WHAT-THIS-PROVES.md (Relation to prior
work): Gentzen/cut, Girard/linear logic, ABLP access-control calculus,
Appel–Felten PCA, Necula PCC, Lamport/TLA, W3C PROV, Denning IFC,
SPKI/SDSI + macaroons, in-toto/SLSA — with the anti-flattening claim (the
distinct object is bounded lifecycle calculi with explicit non-collapse
walls; the welding is the novelty, not the ancestors) and a pointer to the
fuller two-sided map in the papers repo. README links it.LeanProofs/BoundedCalculi/{ExecutionCustody,BootKernel,CheckpointSettlement}.lean
(moved from Scratch, ANNEX release-surface headers),
LeanProofs/BoundedCalculi/MeasureAccounting.lean (new support module),
LeanProofs/BoundedCalculi.lean (aggregate: +4 imports, hardened compile-
marker language), LeanProofs/Scratch/{ExecutionSequent,ExecutionObligationSequent}.lean
(re-pointed at MeasureAccounting/new namespaces), README.md,
WHAT-THIS-PROVES.md, CHANGELOG.md (v3.0.0 entry), docs/V3-RELEASE-LEDGER.md
BoundedCalculi/ ANNEX release surface (not promoted-kernel authority),
with ugly non-authority headers + goblin wards (stage-separation ≠ actuator;
accumulation ≠ escalation; membership-compaction rejected, Split law chosen).MeasureAccounting so the release surface imports no scratch (ANNEX →
Witnessed/ANNEX only; Scratch → ANNEX).LeanProofs.lean untouched.docs/V3-RELEASE-LEDGER.md (new), docs/ROADMAP-bounded-calculi.md (§10 all
slices L0–L6 closed)
LeanProofs/Scratch/CheckpointSettlement.lean (new)
ResourceSequent.Split (first
draft’s membership-level rule let duplicates collapse — codex countermodel;
Split closes it). checkpoint_mints_nothing (zero-axiom) blocks the whole
upgrade family; settlement_preserves_live_multiplicity +
per-entry count conservation; unknown-commit and observation-to-safety
walls; minimal pair dropping_live_obligation_invalidates;
compaction_is_real. Dead-entry policy flagged open (receipts-vs-droppable
is consumer policy).LeanProofs/Scratch/BootKernel.lean (modified)
reaches_from_settled_freezes_baseline), ladder-entry inversions
(settled_entered_only_from_observed, execution_entered_only_from_minting,
zero-axiom), and the honesty fix — capabilities_accumulate states the
monotone capability nesting as a theorem instead of denying it; the
omnipotence theorem docstring demoted to schema (the hard walls are the
anti-skip theorem, the witness invariants, and the absent root/signature
vocabulary).settled_witness_covers_observed_baseline).Campaign-scoped change tracking (operator directive 2026-07-01: version/release
history stays in the root CHANGELOG.md; this file tracks the SCRATCH campaign
as it lands, commit grouping is not the unit of record). Everything below is
Custody-Class: SCRATCH unless stated; nothing here changes a promoted kernel,
an import boundary, or the public surface. Verification receipts land under
.governor/verify_receipts/ (gitignored; durability = receipt content hashes,
not git). Program counter: .governor/loop.json.
Invariant under audit throughout: no artifact may testify beyond the stage it actually survived.
LeanProofs/Scratch/BootKernel.lean (new)
settled_requires_settlement_witness, invariant under
composition); anti-skip wall cold_start_single_exit (zero-axiom);
full_boot_reachable specimen (zero-axiom); settlement freeze; no
root/signature vocabulary (structural absence).LeanProofs/Scratch/ExecutionObligationSequent.lean (new),
ExecutionSequent.lean (wsum machinery generalized to any element type)
obligation_accounting + receipt_accounting +
ticket_accounting_with_obligations (triple-entry conservation);
one_receipt_cannot_license_two_discharges; no_silent_discharge; exact
discharge_inversion (zero-axiom); refusal walls cannot_discharge_unowed
/ cannot_discharge_without_held_receipt; lifecycle + minimal-pair
specimens (zero-axiom).LeanProofs/Scratch/ExecutionSequent.lean (new)
Γ ; τ ⊢[Execution] committed(t, now) ⊣ τ_spent over
Witnessed.ResourceSequent’s Split/Consumes (reused, not re-derived).trajectory_accounting): initial measure =
spent + residual, for every measure w; corollaries commits_le_initial,
ticket_commits_le_initial_occurrences (general no-double-spend),
id_commits_le_initial_id_occurrences (anti-forgery accounting). Built as
the codex-audit-requested generalization of the singleton walls.one_ticket_cannot_commit_twice,
spent_context_cannot_commit_anything (consumption exhausts authority).stale_at_commit_cannot_commit +
fresh_at_attempt_does_not_survive_to_late_commit (same ticket, same
context, only the tick differs — freshness is evaluated at commit).unconsumed_ticket_survives_commit).sequent_commit_does_not_imply_execution; judgment vocabulary
structurally cannot state DidExecute.LeanProofs/Scratch/BridgeSequent.lean (new)
TemporallyValid,
ProjectionAuthorized, surface-side bridge evidence); two rules (ax,
bridgeCut); no master judgment; no rule mints tValid or bEvid.bridge_cut_derives + concrete_sequent_sound — the licensed
crossing, sound against real ProjectionAuthorized over real objects.
Soundness genuinely consumes the temporal premise (closes the C-audit
dead-weight finding at this layer).no_free_cross_cut — ZERO-AXIOM syntactic non-derivability for
all temporal-only contexts, all surface targets, all derivation depths
(relative to the declared rule set, stated explicitly per audit).pAuth_derivation_roots_in_assumptions (audit-requested) —
every surface authorization traces to actual context membership.LeanProofs/Scratch/ExecutionCustody.lean (modified)
CommitUnknown was decorative.commitUnknown_testifies_to_neither (zero-axiom): an unknown substrate
outcome testifies to NEITHER execution nor non-execution (crash-ambiguity
laundering blocker).DischargedObligation decoupling).LeanProofs/Scratch/TemporalToSurfaceBridgeWiring.lean (modified)
ProjectionAuthorized is temporal-blind). Operator chose in-vocabulary
strengthening.surface_authorized_does_not_imply_temporally_valid (reverse cut) and
temporal_surface_mutual_nonimplication (bidirectional independence
capstone; product-orthogonality scope stated precisely per second audit
round). Both [propext]..governor/ (new), docs/ROADMAP-bounded-calculi.md (§10 statuses + §11
as-built ledger), docs/worked-examples/temporal-surface-vocabulary-alignment.md
(relocated from the duplicate LeanProofs/docs/ roadmap, retitled as an
alignment log)
.governor/loop.json program counter stood up (nq precedent:
program counter + custody trail in git, runtime receipts gitignored).governor verify-run exit-code receipts +
#print axioms footprint checks + codex adversarial audits (codex =
auditor; bwrap sandbox blocks codex-as-builder in this environment).ObligationResidue already imports ResourceSequent; natural join).