Skip to main content

70  Executable Specifications and Lean Proof Envelope

70.1 Chapter status

Field	Value
Chapter ID	executable-specifications-and-lean-proof-envelope
Part	Part IV - Evidence, Implementation, and the Living Book
Status	conceptual
Manuscript maturity	v0.3 manuscript draft
Last updated	2026-08-03
Primary source records	genesiscode, spinoza, scf, talos, viea, circle_calculus_core, circle_ai_contract_suite, rope_position_certifier, proof_carrying_circular_computation, cca_project, moecot_manifest_project, corbens_best_model_possible_project
Claim label	Design rationale
Evidence level	argument
Source queue	primary: genesiscode; supporting: spinoza, scf, talos, viea, circle_calculus_core, circle_ai_contract_suite, rope_position_certifier, proof_carrying_circular_computation, cca_project, moecot_manifest_project, corbens_best_model_possible_project
Source loading state	source notes: genesiscode, spinoza, scf, talos, viea, circle_calculus_core, circle_ai_contract_suite, rope_position_certifier, proof_carrying_circular_computation, cca_project, moecot_manifest_project, corbens_best_model_possible_project, precision_contract, ext_reluplex_2017; raw cache: genesiscode, spinoza, scf, talos, viea
Test state	Proof manifest sync, local Lean build, protocol fixtures, depth and adequacy audits, and the formal semantic-depth record pass locally. The proof-artifact audit independently recompiles the exact 28-declaration AsiStackProofs.ProofEnvelope surface, executes a ten-event authority-lease trace, checks eleven composition splits, rejects 33 route cases, exercises expiry and a thin-summary collision, and rejects 19 complete-transport mutations; no artifact truth, arbitrary theorem adequacy, implementation refinement, support movement, or deployed enforcement is established.

70.2 Drafting guardrail

Executable contracts, tests, and Lean proofs occupy different lanes. A theorem is not proven because the prose says so; a proof target is implemented only when the corresponding artifact exists and the verifier passes.

Part III ended by separating structural receipts from model-quality claims. Part IV begins by generalizing that discipline: every formal-looking statement needs a declared artifact lane. Some claims become Lean predicates, some become schema fixtures, some become process validators, and some remain research targets until the architecture can state an operational predicate without pretending that broad ASI behavior has been proven.

The proof envelope is a translation layer. It translates prose claims into proof targets, schema targets, validator targets, benchmark targets, or blocked research targets, then records the exact kind of artifact that exists.

70.3 Human Reading Path

Concrete lens. The green-build baseline calls the deployed adapter proven. The envelope limits the theorem to its encoded transition until conformance is bound.

Elegant substrates and structural receipts alone do not prove broad capability. The evidence envelope makes that warning operational before claims harden into confidence. Some claims should become schemas, some tests, some Lean predicates, and some should remain open research questions.

This is the architecture’s proof etiquette. Formal language earns authority only when the artifact exists, the verifier passes, and the claim boundary is narrow enough to understand. A proof envelope should clarify what is checked, what is not checked, and what would still fail outside the finite predicate. It should not decorate an argument with borrowed certainty.

The payoff is restraint: the strongest language is reserved for the smallest artifact that actually passed. Mechanization earns weight by staying small. That restraint lets formal methods strengthen the manuscript without making it brittle or theatrical, and it gives future proof work a precise target instead of a slogan.

Formal proof helps most when it narrows exactly what may be said. The proof boundary is as important as the proof itself for trust.

70.4 Problem

The book contains many claims that sound formal: authority boundaries, support-state transitions, capability replacement, context adequacy, job lifecycles, proof-carrying claims, and cyclic contracts. Some of these can become Lean proofs. Some should remain JSON Schemas or process contracts. Some are research questions.

GenesisCode supplies the small trusted-kernel and obligation discipline. Spinoza supplies proof-carrying claim and downgrade discipline. Circle Calculus supplies a strong warning: theorem ids and proof status must not be confused with model quality, runtime, memory, or deployment claims.

Formal methods are desirable only when their scope is honest. If the book treats every rigorous-sounding concept as a Lean target, it creates proof theater. If it treats every proof as too narrow to matter, it loses a powerful boundary tool. The proof envelope must decide which predicates can be mechanized, which artifacts validate shape, which tests validate behavior, and which claims must remain prose.

70.5 Why existing approaches are insufficient

Formal methods are ineffective when applied to vague philosophical claims instead of operational predicates and transitions. They are also misleading when tests, diagrams, generated JSON, or Python examples are described as proofs. A useful proof envelope says what is mechanized, what is executable but not formal, what is blocked, and what is intentionally out of scope.

The hard part is not enthusiasm for proof; it is choosing the right unit of proof. “The system is safe” is too broad. “An execution request without a required approval cannot enter the approved state” is narrow enough to test, model, or prove. “The architecture is aligned” is too broad. “A support-state transition cannot move above argument without the required evidence record” is narrow enough to encode. The proof envelope keeps this discipline visible so formal artifacts strengthen the book instead of decorating it.

External formal-methods baselines define multiple evidence lanes that must not be collapsed. PDDL (ext_pddl_1998) models planning domains and problems, proof-carrying code (ext_proof_carrying_code_1997) pairs executable artifacts with checkable evidence, TLA+ (ext_tla_plus_home_docs) models systems, Lean (ext_lean4_theorem_proving) supplies proof-assistant structure, Dafny (ext_dafny_2010) connects programs and specifications, Reluplex (ext_reluplex_2017) verifies neural-network properties, Black-Box Simplex (ext_black_box_simplex_2021) frames runtime assurance, Copilot (ext_copilot_runtime_monitor_2010) generates runtime monitors, and PRISM (ext_prism_model_checker_2002) model-checks probabilistic systems. The proof envelope records which lane a local artifact belongs to; it does not upgrade broad ASI claims.

This also protects readers from a subtle form of evidence inflation. A Lean module may prove a record invariant, while a schema validates fields, while a test exercises behavior, while a benchmark measures performance. Those artifacts can all be valuable, but they do not collapse into one kind of support. If the book cannot state which lane a claim belongs to, the claim is not ready for stronger evidence language.

Semantic proof drift is the proof-envelope risk. A finite predicate can be correct and still be the wrong predicate for the intended ASI Stack boundary. That gap belongs in a semantic adequacy review, not in the Lean build status.

70.6 Core Claim

[executable-specifications-and-lean-proof-envelope.core, label: Design rationale, support: argument] Executable Specifications and Lean Proof Envelope owns a proposition-, predicate-, abstraction-, artifact-, verifier-, consumer-, implementation-, version-, environment-, and time-specific Formal Artifact Authority Lease: a schema, executable model, Lean theorem, model-checking result, runtime monitor, behavior test, benchmark, or external theorem may authorize only the exact consumer statement whose operational semantics, abstraction map and losses, assumptions, dependency closure, verifier result, semantic adequacy, implementation binding, limitations, non-claims, expiry, and revocation path are recorded; artifact existence, field presence, a finite route, proof depth, a green build, a passing fixture, or an external theorem identity alone confers no deployed enforcement, empirical truth, system safety, source correctness, support promotion, transfer, or SOTA authority.

Reader claim. A theorem proves exactly its proposition under its assumptions; it does not automatically prove that the implementation, environment, or world matches the formal model.

Operational rule. Bind every formal artifact to operational semantics, abstraction map, losses, assumptions, dependencies, verifier, implementation version, consumer statement, expiry, and revocation. If the binding is absent or stale, downgrade to a formal-model result rather than a deployed-system claim.

70.6.1 Worked proof envelope: the theorem holds, the adapter differs

A Lean theorem shows that an allowed transition never exceeds an encoded authority ceiling. The proof compiles, and its finite record model is internally valid. The production adapter, however, maps one permission class to a broader operation than the formal abstraction. The theorem remains true; the implementation-binding claim fails. The proof envelope therefore permits the statement “the encoded transition preserves the encoded ceiling” and blocks “the deployed adapter enforces least authority.”

Repair requires an explicit abstraction map, a conformance test against the actual adapter version, and a new consumer binding. A green theorem build cannot supply those facts. The chapter’s finite target and rejection checks distinguish implemented Lean artifacts, non-Lean artifacts, external theorems, and unsupported promotion requests. They establish proof and claim custody, not source correctness, semantic adequacy, implementation conformance, empirical truth, enforcement, or safety.

The claim remains at argument support. The current generated proof manifest contains 330 implemented narrow formal obligations and 3 planned targets without claimed theorems; the activation audit separately preserves its historical 298-target baseline. Current proof-depth snapshot: 340 proof targets, 133 Lean modules, 3153 theorem declarations, 1978 derived/decomposed, 447 direct/projection, 728 unknown/mixed, and 2/2 safety-critical chapter classifications present. That coverage does not prove broad chapter claims, source interpretation, deployed enforcement, model quality, semantic adequacy, or benchmark performance.

The proof-depth classifier is intentionally blunt. derived/decomposed means a theorem body uses structural proof steps such as unfolding, case analysis, rewriting, branching, contradiction handling, or comparable decomposition. direct/projection means the proof mostly projects an already-assumed field, implication, or equality. Direct/projection theorems can still be valuable traceability hooks, but the rendered chapter must preserve projection-only traceability language when safety-critical modules contain them. The classifier is not a proof of semantic adequacy; it is a guard against letting green builds sound broader than the predicates they actually check.

70.6.2 Claim-source mapping status

Appendix C records exact passage-reviewed mappings for all twelve assigned sources. The mappings justify proof-envelope priorities as design rationale only: small operational predicates, typed records, evidence artifacts, support-state boundaries, route/authority/lifecycle checks, and explicit non-claims. They do not promote the claim beyond argument support.

Source	What it supports	Limit
genesiscode	Three-part paper, Rust handoff, and style-contract bundle for trust strata, Gλ/CoreForm semantics, authenticated control variants, capability effects, graded replay, heterogeneous obligation/evidence lanes, semantic patches, types, e-graphs, translation validation, conformance, and spec-first tests. The audit additionally exposes fresh-token minting as an authority-bearing effect and finite equivalence tests as weaker than full translation validation.	No parser, evaluator, seal security, runner, replay checker, patch engine, obligation policy, type/proof stack, optimizer checker, benchmark, integration, or security result exists locally. The dated Codex workflow advice is not a language invariant or current-product source.
spinoza	Proposer/verifier separation, explicit formal scope, proof/citation/procedure tiers, belief revision, dependency tracing, downgrade behavior, and verifier-bound claims.	No open-domain autoformalizer, proof verifier, belief-maintainer, tier engine, arbitrary theorem-validity result, or whole-system epistemic correctness proof exists here.
scf	Stable capability identity, exact content binding, trusted-validator/untrusted-proposer split, contract requirements, evidence graphs, caller-bound authority, lifecycle ordering, and migration solvency.	Does not prove production safety, global alignment, evaluator integrity, route quality, actual rollback, or the SCF companion executable fragment inside this repo.
talos	Typed jobs, contract locks, claim extraction, evidence binding, adversarial verification, artifact certification, proof bundles, replay, secret-blind execution, and audit logs.	No Talos runtime, job executor, security benchmark, replay proof bundle, imported log, or execution-security result is validated here.
viea	Command contracts, artifact graphs, support-state rules, workflow-to-tool compilation, evaluation ratchets, residuals, vertical-slice loops, evidence hierarchy, and downgrade policy.	Architecture proposal only; no VIEA deployment, runtime trace, workflow compiler, benchmark, field-feedback record, or execution-loop behavior is proven here.
circle_calculus_core	Proof-status discipline, theorem manifests, proof boundaries, sidecar separation, finite structural facts, receipt commands, and explicit non-claims.	A separate external Circle rope receipt slice is recorded in docs/circle_external_receipt_slice.md, but this row remains proof-boundary context, not broad local proof ownership, model-quality evidence, or deployment evidence.
circle_ai_contract_suite	Contract families, schema and receipt fields, require gates, replay/fingerprint surfaces, generated packs, downstream rejection records, readiness fields, and non-claims.	A separate external Circle rope receipt slice is recorded in docs/circle_external_receipt_slice.md, but no vendored contract pack, ASI Stack consumer gate, or proof-adequacy claim is validated here; no model-quality, context, performance, or deployment claim follows.
rope_position_certifier	Exact/discretized RoPE receipt boundaries, collision and margin fields, theorem ids, certifier commands, sidecar regeneration surfaces, and one-channel real-phase frontier language.	Does not prove arbitrary real-valued RoPE, full all-channel RoPE, longer usable context, speed, memory, training stability, model quality, or deployment readiness.
proof_carrying_circular_computation	Cyclic-address seed, elementary address-safety theorem scope, stride-coverage boundary, Lean/Python sidecar distinction, and proof-plus-benchmark backend program.	No Circle sidecar, external Lean build, CoilIR lowering, cyclic backend benchmark, hardware-kernel benchmark, or performance claim is reproduced here.

70.7 Mechanism

The proof envelope begins by refusing to formalize the book’s broad theses directly. Each candidate claim is lowered into a Proof Target Record, then routed to Lean, executable schema validation, process validation, research backlog, or blocked status according to the predicate that can actually be checked.

flowchart LR
  A["Chapter claim or invariant"] --> B["Proof Target Record"]
  B --> C["Triage kind and non-claims"]
  C --> D{"Operational predicate?"}
  D -- "Lean-suitable" --> E["Lean module + lake build"]
  D -- "record/process" --> F["Schema, fixture, or validator"]
  D -- "not operational yet" --> G["Research target, blocked target, or residual"]
  E --> H{"Verifier passed?"}
  F --> H
  H -- "yes" --> I["Narrow implemented proof/spec state"]
  H -- "no" --> G
  I --> J["Appendix E and proof manifest"]

What the proof envelope shows: The proof envelope starts by triaging whether a claim has an operational predicate at all. Lean modules, schemas, fixtures, validators, blocked targets, and residuals are separate lanes, and a passing artifact updates only the narrow proof/spec state it actually checks.

Each target should record its tag, module, artifact lane, formal target, artifact path, verifier command, verifier result, support-state impact, consumer requirements, semantic adequacy state, limitations, and non-claims. A passed schema check can support record shape. A passed Lean build can support a mechanized invariant. Neither can support empirical performance unless an experiment exists.

The repository now mechanizes the envelope rule as a finite target-status predicate. In AsiStackProofs.ProofEnvelope, an implemented target must carry module-existence and build-passed flags, and a non-operational target is routed to planned or blocked rather than implemented. The module also models proof-artifact reviews: a non-Lean lane cannot claim to be a Lean proof, support-state promotion requires an accepted evidence transition plus semantic adequacy, limitations, non-claims, and consumer-requirement matching, and external-theorem references require artifact refs, resolved theorem IDs, and non-claim boundaries. The proof is a policy invariant over proof-target records; it is not a filesystem crawler, theorem-discovery tool, semantic adequacy judge, external theorem verifier, or coverage audit.

A layered formalization path protects proof claims from inflation. First the prose names an invariant. Then the outline assigns a stable lean:* tag. Then the proof manifest records the target. Then triage decides whether the target belongs in Lean, a schema, a process validator, a research backlog, or a blocked state. Only then does an implementation artifact matter. This path makes it harder for a future writing run to confuse a desirable theorem with an existing theorem, or an existing theorem with a broad system guarantee.

Every passed artifact should produce a proof/spec receipt. The receipt says what command ran, what artifact was checked, what predicate or schema it covers, what consumer may rely on it, and what claims it explicitly does not support.

The artifact lane is a first-class field because different lanes fail differently. A Lean lane can fail because the module does not build. A schema lane can pass while the represented event never happened. A process-validator lane can check wiring without checking semantics. A behavior-test lane can exercise a path without proving a theorem. A benchmark lane can measure performance while saying nothing about proof. The proof envelope is useful only if those lane differences survive into the fixture and into the prose that consumes it.

70.7.1 Verification of an abstraction is not verification of transfer

A reusable abstraction creates at least three separately checkable claims. The semantic claim says the abstraction denotes what its contract says. The artifact claim says lowering, compilation, linking, or emission preserved that contract in the bytes that ran. The transfer claim says making the verified artifact available changed future outcomes under a frozen task distribution, search procedure, verifier, and budget. A proof of the first does not discharge the second, and neither proves the third.

The receipt should therefore bind a verification level and an exact outcome. Tested, exhaustive-bounded, solver-validated, certificate-checked, proof-assistant-checked, and artifact-validated results carry different authority. Likewise, unknown and timeout cannot be collapsed into refuted, while a verified artifact can remain transfer-neutral or transfer-negative. If source and emitted artifact differ, the consumer needs a translation or artifact-validation obligation rather than a comment asserting that the proof survived compilation.

The finite counterexamples and protocols in From Compression to Forward Transfer motivate this separation but are not mechanized in the repository. Any Lean target derived from them must first be deduplicated against existing proof owners and remain scoped to the encoded finite model.

70.7.2 A tiny kernel still has authority-bearing roots

GenesisCode proposes a useful three-way trust split: a minimal evaluator, immutable primitives, and seal operations at the semantic root; capability, replay, and package verifiers in an operational trust layer; and optimizers, JITs, e-graph rewriters, compilers, and backends outside the TCB when checked per artifact. The important word is when. Calling a component non-TCB does not remove it from the causal path. It moves trust to a checker whose source, semantics, dependencies, build, command, assumptions, and consumer claim must be smaller and independently bound.

The proposal exposes a subtle specification contradiction. A fresh unforgeable seal() cannot be an ordinary pure deterministic primitive unless its name supply and initial state are explicit. Freshness requires mutable state, randomness, a deterministic state-passing schedule, or a host-issued token. Sealing and unsealing can remain a pure relation, but the system must treat token minting as an authority-bearing initialization or runtime effect. Its issuer, entropy or counter state, epoch, scope, exportability, persistence, revocation, and replay behavior belong in the formal artifact. A nominal SealId field proves neither unforgeability nor safe custody across memory, serialization, FFI, reflection, restart, or process boundaries.

Sealed control variants still supply a strong invariant: user data that looks like UNHANDLED, EFFECT, or ERROR must not become privileged protocol state by matching a string or ordinary structure. But authenticated protocol origin is not authorization. Anyone holding the relevant token can construct the variant, so token distribution is capability distribution. A formal target must separate control authenticity, caller identity, delegated authority, target permission, and the runtime decision that follows.

GenesisCode’s Obligation Engine also sharpens the envelope. An obligation declaration, verification procedure, evidence artifact, verifier result, registry policy decision, and consumer claim are different objects. A package can choose weak obligations; a hash can identify bytes without validating them; a test, coverage report, benchmark, SMT trace, proof object, signature, and translation certificate confer different authority. Independent policy must define mandatory obligations, scope, expiry, waiver, challenge, and invalidation across dependency, toolchain, policy, verifier, or artifact change.

Optimization illustrates why exact names matter. Comparing source and target on a finite test suite is an equivalence test, not complete translation validation. A proof-producing rewrite trace, independently checked per translation, or a scoped symbolic/refinement relation may justify stronger language. E-graph rules additionally bind side conditions, arithmetic, effects, resource semantics, and the extraction cost model. “The compiler is outside the TCB” is earned only by the exact relation the checker actually decides.

This chapter has a narrower owner than the book’s general evidence system. Claims and Evidence owns support transitions, and Proof Contract Transport owns the identity and integrity of transported theorems and receipts. Executable Specifications and Lean Proof Envelope owns whether a particular formal or executable artifact is semantically adequate for a particular consumer statement. Its unit of authority is the Formal Artifact Authority Lease, not a global claim that formal methods make the stack correct.

70.7.3 Eighteen-stage formal-artifact lifecycle

The lifecycle registers the exact proposition, quantifiers, scope, owner, consumer language, authority sought, versions, environment, and expiry; then decomposes the broad claim and preserves its unproved remainder. It routes the predicate to the correct artifact lane, defines the abstraction map and losses, states the trusted base and environmental assumptions, and specifies valid and invalid states plus safety, liveness, resource, recovery, and counterexample obligations. Stable theorem and target identities, dependencies, consumers, artifacts, commands, and expected authority are frozen before implementation.

The artifact is then built in a pinned environment with source, toolchain, command, output, digest, warnings, timeouts, failures, and nondeterminism preserved. Where the claim crosses layers, an independently implemented checker or observational relation tests refinement from specification to executable model to implementation. Vacuity, inconsistency, unreachable-state, assumption-restatement, missing-field, mutation, countermodel, adversarial-schedule, stale-artifact, and wrong-consumer controls run before a semantic adequacy review compares the result with the prose obligation, strongest counterclaim, reachable behavior, intended consumer, and excluded cases.

A runtime claim additionally binds a named implementation, build, deployment, monitor or trace source, observation boundary, and independent effect. Only then may the system issue a least-authority receipt. Monitoring covers changes to the proposition, source, theorem, dependency, toolchain, specification, implementation, environment, policy, threat, rights, consumer, and evidence. Failure triggers refusal, residualization, quarantine, revocation, migration, rollback, supersession, refutation, or retirement. Decisive results require independent formalizations, tools, implementations, and evaluators before transfer; material change expires the lease while lineage, countermodels, negative results, semantic losses, unproved remainders, and residual owners remain visible.

70.7.4 Governed Transition Calculus

The chapter-specific contracts share a small transition kernel. A governed transition is represented as

[ T = (I_s, I_t, A, O, E, R, C, , ), ]

where (I_s) and (I_t) are the exact source and target identities; (A) is the authority under which the transition is considered; (O) is the set of obligations that must be discharged; (E) is the evidence actually available; (R) is the residual set that survives the decision; (C) names the downstream consumers; () gives expiry and revocation conditions; and () gives rollback, compensation, quarantine, supersession, or retirement when an exact return is impossible. This is the Governed Transition Calculus. It is a shared vocabulary and admission shape, not a new chapter, a universal theorem, or evidence that any runtime enforces the fields.

The calculus gives twelve recurring obligations a single home:

1. authority cannot escalate merely because a transition is useful;
2. evidence cannot promote without an accepted evidence transition;
3. context cannot become authority by being present;
4. a plan cannot be counted as an effect;
5. a receipt cannot replace independent observation;
6. unresolved residuals must be conserved across handoffs;
7. expiry and revocation must reach consumers and descendants;
8. a replacement cannot inherit the predecessor’s qualification;
9. rollback must close the declared effect surface or retain an explicit unresolved effect;
10. admitted work needs a bounded path to completion, refusal, quarantine, or retirement;
11. identity must survive composition across specification, implementation, observation, and evidence layers; and
12. the subject of a protected change cannot solely ratify its own authority, evaluator, or constitution.

Different chapters instantiate different subsets and stricter fields. System Boundaries owns authority; Claims and Evidence owns support movement; context, planning, runtime, replacement, readiness, and release owners keep their own semantics. The calculus prevents those owners from inventing incompatible handoff meanings. Its first honest implementation is a record and consumer crosswalk. Nonvacuous models, countermodels, implementation refinement, natural traces, and empirical observations belong to the later evidence phase.

70.7.5 P0–P6 semantic-depth overlay

The existing artifact classifier says what kind of artifact exists. It does not say how far that artifact reaches toward the intended system meaning. Every formal target should therefore receive a separate semantic-depth label:

Level	Earned meaning
P0	Schema, type, field, or record-shape property.
P1	Finite route, rejection, conservation, or preservation property over the modeled state.
P2	Reachability with an explicit witness, executed path, and nonvacuity check.
P3	Refinement to a named implementation or binding to a runtime monitor.
P4	Cross-component safety, noninterference, or adversarial composition under stated assumptions.
P5	Bounded liveness, recovery, revocation, or concurrency behavior.
P6	Empirically bound semantic property with a named independent observation contract.

Levels are obligations, not a score that a target acquires from neighboring work. A P0 theorem can remain useful and correct without being “upgraded.” A P2 witness does not confer P3 implementation binding. P6 does not mean a universal empirical truth; it means that the exact proposition is connected to a named observation under a frozen scope. Each target eventually needs its assumptions, consumer, witness or explicit unreachability, implementation binding, mutation coverage, semantic owner, maximum inference, and retain/rewrite/retire disposition. During the manuscript-completion phase this overlay organizes the proof estate; it does not claim that the current declarations have already earned those labels.

70.7.6 Semantic depth and implementation binding

Artifact class is not enough. Two Lean-backed claims can have very different semantic depth. A field-presence predicate establishes that a record contains a name. A finite route establishes the modeled output for one bounded state. A derived invariant composes such predicates under explicit assumptions. An executable-model bridge shows that a tracked program and formal vocabulary share a bounded trace. An implementation binding additionally identifies the deployed artifact and independently observed runtime effect. The five lanes are ordered by obligations, not by prestige, and none automatically promotes the next.

CCA contributes the need for an explicit abstraction map and by-construction properties around its typed calculus. MoECOT Manifest contributes pass/reproducer/legality artifacts while also demonstrating that extensive internal contract structure can coexist with weak external capability. Corben’s Best Model Possible contributes the decisive negative cases: named tribunal rows, shape-valid fixtures, playback, and source structure can all be green while semantic binding or current execution is absent. These projects form one local lineage; they are design and contradiction inputs, not three independent validations.

The semantic-depth record maps each prose term to a formal symbol, representation, and declared loss. It states clock, concurrency, event completeness, adversarial-log, identity, and environment assumptions; names what holds by construction; and lists runtime behavior excluded from the model. A consumer can therefore rely on “the finite route denies this modeled record” without silently converting it into “a deployed service denied the real effect.”

The strongest objection is that a hand-authored depth label can become another decorative checklist. That is correct unless the label binds artifacts, verifier commands, assumptions, and consumer language. The fixture therefore rejects a passing formal or executable lane without artifact and verifier identity, and it blocks runtime language while implementation binding is absent. This still does not prove that the abstraction map is correct; it makes that judgment and its losses inspectable.

70.7.7 Refinement types, dependent types, and proof-carrying data

Ordinary schemas establish shape. Refinement types add predicates to a base type—for example, a nonnegative latency below a declared deadline, or a grant whose scope is a subset of an authority ceiling. Dependent types allow one field or artifact type to depend on another value, such as a vector indexed by its declared dimension, a route receipt indexed by the exact contract version, or a rollback witness tied to the state surface it claims to restore. These tools move selected preconditions from prose into construction and checking.

The gain is real but bounded. A refinement checker proves the encoded predicate for the encoded value under the checker and logic assumptions. It does not prove that a field measures the intended property, that the bound is safe, or that serialization and runtime preserve the semantics. Dependent encodings can hide assumptions in indices, conversion functions, proof erasure, foreign calls, or trusted axioms.

Proof-carrying data treats evidence, not only code, as a typed artifact. A dataset row, observation, model output, authorization, transformation, or certificate can travel with a machine-checkable witness for provenance, schema, permitted derivation, range, freshness, or another finite property. Consumers verify that witness against a named policy and exact identity before using the payload. Familiar JSON shape alone is never the proof.

The envelope also states finite-encoding limits. Continuous dynamics, real numbers, distributions, neural computations, clocks, and open environments enter a proof assistant through finite representations and abstraction maps. Quantization, rounding, overflow, nondeterminism, concurrency, compiler lowering, kernels, and sensor interpretation can break a property that held in the mathematical model. Every transported proof therefore binds numeric format, tolerance, runtime, transformation chain, trusted base, and exact property preserved at each step.

flowchart LR
    D["Runtime or data artifact"] --> T["Base type / schema"]
    T --> R["Refinement predicate"]
    R --> P["Dependent identity and witness"]
    P --> C["Consumer verification"]
    C --> B{"Abstraction and runtime bound?"}
    B -->|yes, finite scope| U["Use under named contract"]
    B -->|missing| H["Hold as unbound formal evidence"]

70.7.8 Compression as a verified program transformation

Quantization and compression transform one executable program into another. The refinement question is not whether their parameter arrays are close. It is whether the transformed package—including decoder, scales, codebooks, indices, residuals, kernels, routing, and fallback—preserves each named protected property under the contract.

Some obligations can be formal: integer range, saturation, rounding semantics, serialization, decoder determinism, shape, bounded numeric error, route priority, identity checks, or exact fallback. Others require competent empirical evidence: calibration, rare-behavior preservation, natural utility, distribution shift, and evaluator adequacy. The transformation record assigns each obligation to its actual evidence lane rather than claiming that a finite numeric bound proves behavior.

The strongest finite transfer has the shape of a margin argument. If a reference artifact satisfies property \(\varphi\) with decision margin \(m(x)\) and an independently checked implementation bound establishes \(\lVert M(x)-\widehat M(x)\rVert\leq\delta(x)<m(x)\) for every \(x\) in the declared region, then that property transfers on that region. The conclusion does not cover other properties, inputs, preprocessing, samplers, kernels, or agent environments. Small verifiers, routers, numerical kernels, constrained decoders, and safety monitors may admit this treatment even when a frontier generative model does not.

A translation-validation pattern is appropriate when verifying every compiler pass is impractical. For each produced artifact, independently check the exact reference/transformed pair against a bounded equivalence or refinement condition. pass, fail, and unknown are all valid results. An unknown protected property routes to more precision, the reference implementation, abstention, or escalation; it never becomes equivalence by default.

70.8 Interfaces

The Proof Target Record is the interface between prose, outline, Lean, schemas, validators, and Appendix E. It lets the book say exactly which finite predicate has an artifact behind it while keeping broader system behavior outside the proof claim.

Minimum fields:

• proof_id
• chapter_id
• lean_tag
• target_kind
• artifact_lane
• formal_target
• artifact_refs
• verifier_command
• verifier_result
• support_state_effect
• consumer_requirements
• semantic_adequacy_review
• limitations
• non_claims

The outline defines proof scope. proofs/proof_manifest.json records the generated target set. Lean modules implement selected invariants. JSON Schemas implement record contracts. Validation checks that manifests, schemas, and examples stay coherent.

The support-state effect remains deliberately narrow. A passed lake build can justify saying that a local finite-record predicate builds. It cannot justify saying the source interpretation is correct, the real system enforces the rule, the model behaves well, or the benchmark improved. A passed schema validator can justify saying that a fixture has the required shape. It cannot justify saying the represented event happened. This separation is what makes the proof envelope useful to a living book rather than theatrical.

Consumer requirements belong beside the proof artifact. A chapter, protocol, or release profile may consume a proof only if the proof lane, command, artifact path, version, semantic adequacy state, and non-claims match what that consumer needs. Otherwise the proof remains true but unusable for that purpose.

The semantic adequacy review is not a second proof. It is a record of whether the finite predicate actually matches the boundary it is being asked to support. Until that review exists, the safest support-state effect is narrow: the artifact passed its verifier, but the prose may not borrow more meaning than the predicate states.

Twelve ownership interfaces keep the lease from becoming a universal proof claim. Chapter owners define the proposition and unproved remainder; Claims/Evidence owns support transitions; Proof Transport owns identity and integrity; schemas own record shape; proof assistants and model checkers own derivations inside declared models; executable specifications own bounded traces and refinement candidates; Runtime/Serving/Security own actual enforcement; Benchmarks/Verification own empirical adequacy; Source/Artifact/ Supply Chain own provenance, rights, and toolchains; Resource Economics owns formal and governance cost; Readiness/Incident/Release owns canary, public wording, quarantine, and correction; and Living-Book/Change Governance owns stable tags, synchronized surfaces, lineage, expiry, and successor work.

70.9 Invariants

• No theorem is claimed proven without lake build.
• Proof tags remain stable.
• Broad claims are decomposed before formalization.
• Python tests and diagrams are not Lean proofs.
• Proof status does not imply model quality or deployment safety.
• A formal artifact requires a semantic adequacy note before it can strengthen prose beyond its finite predicate.
• Field presence, finite route, derived invariant, executable-model bridge, and implementation binding remain distinct lanes with distinct authorized statements.
• Every abstraction mapping names what semantics it loses, and every finite invariant exposes clock, concurrency, completeness, and adversarial-log assumptions where applicable.
• An unbound implementation cannot authorize a runtime claim.

The proof boundary also preserves artifact class. A schema pass, Python fixture, successful Quarto render, Lean theorem, benchmark result, and human review note are different kinds of evidence. They may support one another, but they cannot substitute for one another without an explicit transition record. That separation keeps formal work from becoming a confidence aesthetic and keeps ordinary tests from being described as proofs.

The full invariant set requires exact lease scope; visible unproved remainders; separate artifact lanes; complete abstraction maps and losses; explicit trusted bases and environmental assumptions; separation of safety, liveness, progress, recovery, resource, and empirical obligations; green-build restraint; distinct field-presence, projection, route, derived, bridge, binding, and observed-effect depths; exclusion of vacuous, inconsistent, unreachable, duplicated, orphaned, unused, and unconsumed declarations from authority; stable dependency and consumer links; exact external-theorem hypotheses and non-ownership; named implementation binding for runtime language; visible failures and disputes; least-authority composition; change-triggered expiry; descendant-complete revocation; independent-error separation; and ownership for every semantic loss, unproved remainder, disputed judgment, failed transfer, and retirement.

70.10 Certified neural properties are bounded formal artifacts

Neural-network verification belongs inside the proof envelope, but it requires a different abstraction map from a Lean proof about stack records. Reluplex demonstrated satisfiability checking for properties of bounded ReLU networks, including an aircraft collision-avoidance case [@ext_reluplex_2017]. Modern verifiers may use branch-and-bound, abstract interpretation, mixed-integer formulations, or specialized relaxations, yet the authority question remains the same: exactly which network, arithmetic semantics, input set, and output property were checked?

A neural certificate packet binds model and checkpoint digest, preprocessing, architecture and supported operators, numerical semantics, input region, perturbation norm or physical set, property, verifier and version, timeout policy, proof or counterexample artifact, independently checked result, implementation binding, and uncovered cases. “Unknown” and timeout are first-class outcomes. A certificate for one region may narrow an empirical threat residual; it cannot be generalized to other inputs, checkpoints, modalities, preprocessing code, or the surrounding agent.

Failure modes include unsound relaxations, floating-point mismatch, omitted preprocessing, a vacuous input region, post-certificate weight changes, unsupported operators replaced by optimistic approximations, and selecting only properties that the verifier can prove. The explicit nonclaim is that a certified property establishes neither natural-distribution robustness nor model intent, data quality, privacy, alignment, whole-system security, or deployment safety. It is a theorem about an encoded artifact under recorded assumptions.

70.11 Failure modes

• Formalization theater.
• Unstable proof target names.
• Claiming proof from prose.
• Treating external theorem ids as local proof ownership.
• Promoting a downstream claim from a structural receipt alone.
• Calling field presence a derived invariant or a finite route deployed enforcement.
• Omitting concurrency, missing-event, or adversarial-log assumptions from an otherwise valid finite theorem.
• Treating a passed executable bridge as implementation binding without a deployed artifact and independently observed effect.

Semantic mismatch, unmodeled semantics, and spillover move the target to downgrade, schema, process, or research status.

Proof laundering starts when a valid local predicate, external theorem id, generated receipt, or schema pass is used to promote a broader claim whose semantics were never formalized.

Orphaned formality is the opposite failure. A proof target exists, but the prose no longer explains what it means, the outline no longer routes to it, or the source claim it was supposed to bound has changed. In that case the theorem may still compile while no longer governing the manuscript. Proof artifacts should stay linked to claims, limitation prose, generated manifests, and audit records.

The matched failure set includes decorative theorem counts; trivial predicates carrying broad claims; schema, test, benchmark, or citation laundering; direct projections marketed as semantic derivations; finite routes marketed as deployment enforcement; executable fixtures marketed as implementation binding; abstraction maps that erase identity, concurrency, missing events, nondeterminism, failures, adversaries, resources, rights, or open-world behavior; safety/liveness/resource/empirical category errors; vacuous or inconsistent models; stale tags and consumers; duplicate, orphan, unused, or unconsumed proof bloat; unresolved external theorem hypotheses; censored failures and countermodels; wrong-scope consumer use; hidden proof and monitor cost; support movement without a transition; incomplete descendant revocation; and sunk-cost resistance to merging, replacement, refutation, or retirement.

70.12 Minimum Viable Implementation

The proof envelope begins with the existing generated proof manifest plus a proof target record. The repository fixture validates chapter, Lean tag, target kind, artifact lane, formal target, artifact refs, verifier command/result, support-state effect, consumer requirements, semantic adequacy state, limitations, and non-claims. The target itself remains unproved until the referenced artifact and semantic adequacy checks support it.

The current local verification gate includes cd lean && lake build; a passing build confirms the Lean modules in this repository, not every prose claim that references them. The proof-envelope module adds narrow record-level invariants for implemented status, non-operational routing, proof-lane authority, support-promotion boundaries, and external-theorem reference boundaries. Appendix E publishes the generated coverage summary from proofs/proof_triage.json: all 327 proof targets are covered by triage. The proof artifact traceability audit checks only that targets are wired through manifest records, triage records, Lean modules, root imports, chapter hooks, limitation prose, and Appendix E coverage. The proof-depth classifier records whether theorem bodies are direct/projection, derived/decomposed, or unknown/mixed so proof etiquette is visible in the manuscript. Semantic proof adequacy review is recorded separately from traceability and does not promote broad system claims.

A proof/spec receipt suite should make the envelope operational: one Lean predicate receipt, one schema-validation receipt, one process-validator receipt, one behavior-test receipt, one benchmark receipt, one external theorem reference rejected as local proof, and one semantic adequacy residual that prevents prose promotion.

The repository now also includes schemas/formal_semantic_depth_record.schema.json, one blocked three-project semantic-depth fixture, and ten expected-invalid mutations. The harness rejects erased abstraction loss, missing concurrency assumptions, duplicate lanes, field-presence/runtime laundering, finite-route/deployment laundering, a derived result whose route dependency failed, an artifactless executable bridge, missing runtime exclusions, a runtime claim from an unbound implementation, and fixture-based support promotion.

The exact current minimum is one proof-target schema and valid fixture; one generated 330-target proof manifest with all 330 targets implemented; a 130-module Lean workspace with 2,902 theorem declarations classified as 1,804 derived/decomposed, 435 direct/projection, and 663 unknown/mixed; proof-readiness, traceability, depth, and semantic-adequacy review surfaces; one blocked formal-semantic-depth record with ten rejecting mutations; and an exact 28-declaration ProofEnvelope surface. Five retained negative cases sit beside 23 lifecycle and transport results. The independent consumer executes a ten-event issue/change/review/reissue/revoke trace, checks eleven composition splits, rejects 33 route cases, exercises expiry and a thin-summary collision, and rejects mutations to all 19 complete-transport fields. The separate activation audit preserves its historical 298-target, 65-module, and 1,151-theorem baseline. This minimum provides no artifact or source truth, complete semantic formalization of the stack, deployed enforcement proof, general implementation refinement, independent formal reproduction, empirical result, chapter-core transition, or SOTA result.

70.13 Mature Research Target

The formal-methods endpoint is a claims control plane for the whole stack. It does not try to prove “ASI safety” or “alignment” as one grand theorem. It maintains a live registry of every formal-looking promise, routes each promise to the right artifact lane, and refuses to let a passed artifact support a broader claim than it actually checks.

A mature proof envelope makes every chapter, protocol, release, and runtime module consume proof only through a typed Proof Target Record. The record would name the exact predicate, source claim, artifact lane, verifier command, verifier result, semantic adequacy review, consumer requirements, support-state effect, limitations, and non-claims. A Lean predicate, JSON Schema, process validator, behavior test, benchmark, external theorem reference, and research backlog item would remain different objects with different authority.

A proof-envelope surface needs:

• A generated proof/spec registry fed by the outline, chapter hooks, Appendix E, schemas, Lean modules, validators, and release profiles.
• Semantic adequacy reviews that ask whether a finite predicate is the right predicate for the prose boundary before any support language strengthens.
• Consumer gates that block downstream use when artifact lane, command, version, non-claims, or adequacy state do not match the consuming chapter or runtime.
• Stale-proof and orphan-target detection when a theorem name changes, a schema evolves, a chapter claim moves, or a target remains implemented but no longer maps to the intended boundary.
• Receipts for proof, schema, process, behavior, benchmark, and external-reference lanes so future agents can see exactly which authority each artifact carries.
• Failure closure that routes proof laundering, formalization theater, external-theorem borrowing, stale tags, and claim-from-prose errors into downgrade, quarantine, or adequacy residuals.

With that envelope in place, the stack could depend on mechanized record-level claims without pretending that record-level proofs are deployed enforcement, empirical model quality, benchmark success, or source-truth validation. The proof envelope remains a target architecture until semantic adequacy reviews, artifact audits, runtime consumers, and accepted evidence transitions show where each formal predicate can and cannot carry prose.

70.13.1 Argument-exit and proof-rationalization campaign

The full attempt audits all 298 activation-baseline proof targets and all 1,151 activation-baseline theorem declarations. Every declaration receives a stable identity, proposition, assumptions, dependency and consumer graph, semantic-depth class, vacuity and reachability result, artifact and verifier record, current use, strongest counterclaim, required lane, terminal disposition, and preserved lineage. Direct projections, assumption restatements, duplicated lemmas, unused theorems, orphan targets, misleading names, and unconsumed traceability declarations are merged, replaced, or retired unless a named consumer genuinely needs them.

Load-bearing predicates must use the right model: richer transition systems, temporal or concurrency semantics, noninterference, resource conservation, recovery and liveness, probabilistic reasoning, or refinement where the prose requires them. Behavior, capability, quality, and cost obligations move to executable and empirical lanes instead of being forced into Lean. The campaign tests vacuity, inconsistency, unreachable states, countermodels, mutations, adversarial schedules, stale dependencies, wrong consumers, and revocation; then binds real implementations and monitors where runtime authority is sought.

Decisive claims require independent formalizations or tools when useful, independent implementation and evaluation, complete proof and governance cost, and transfer across environments, consumers, attacks, and time. Results may be narrow, null, refuted, retired, or blocked_after_full_attempt. Until every load-bearing atom and declaration receives its required full attempt and terminal disposition, the chapter core remains argument; theorem counts and green builds are explicitly non-terminal.

70.14 Codex test plan

Test	Purpose	Status
Proof target record fixture validation	Check that proof target records expose artifact lane, verifier command/result, consumer requirements, semantic adequacy state, limitations, support-state effect, and non-claims.	implemented; passing via python3 scripts/validate_protocol_examples.py
Proof manifest sync test	Check that outline proof tags and proofs/proof_manifest.json agree.	implemented by validation; validated locally
Lake build smoke test	Check that local Lean modules build.	validated locally
Implemented-target missing artifact/build negative case	Reject implemented proof-target status when the target lacks a module/artifact reference or passing verifier/build record.	implemented in AsiStackProofs.ProofEnvelope; passing via cd lean && lake build; no filesystem discovery or proof-adequacy claim
Non-Lean artifact proof-laundering negative case	Reject schema, process, behavior, benchmark, external-theorem, or backlog artifacts that are presented as Lean proof claims.	implemented in AsiStackProofs.ProofEnvelope; passing via cd lean && lake build; no artifact semantic-adequacy claim
Support-promotion boundary negative case	Reject support-state promotion from a proof artifact without accepted evidence transition, semantic adequacy, limitations, non-claims, and consumer-requirement match.	implemented in AsiStackProofs.ProofEnvelope; passing via cd lean && lake build; no Appendix C or chapter-core promotion
External theorem reference boundary negative case	Reject external-theorem references that lack artifact refs, resolved theorem IDs, or non-claim boundaries.	implemented in AsiStackProofs.ProofEnvelope; passing via cd lean && lake build; no external theorem ownership or transfer claim
Implemented-target envelope negative case	Reject an implemented proof-target record whose module-existence or build-passed field is false, while repository validators independently inspect current modules and imports.	implemented in AsiStackProofs.ProofEnvelope plus proof-artifact audit; no filesystem semantics inside Lean
Non-operational target routing negative case	Exclude implemented status when the finite record is assumed non-operational and routed only to planned or blocked, while repository validators independently enforce current classification.	implemented in AsiStackProofs.ProofEnvelope plus proof-manifest and proof-artifact validation
Proof target coverage summary	Classify proof targets by status, triage class, and recommended route.	implemented in generated Appendix E; checked by python3 scripts/validate_proof_readiness.py
Proof artifact traceability and lease-lifecycle audit	Verify target traceability, recompile the exact 28-declaration module, reconstruct one ten-event issue/change/re-review/reissue/revoke trace, check eleven composition splits, reject 33 route cases, exercise expiry and a lossy-summary collision, and mutate all 19 complete-transport fields.	implemented in docs/proof_artifact_audit.md; checked by python3 scripts/validate_proof_artifact_audit.py; finite authored-record semantics only
Proof-depth surface synchronization	Check that the chapter, reader chapter, outline, and roadmap expose the current proof-depth classification counts and direct/projection versus derived/decomposed distinction.	implemented by python3 scripts/validate_proof_depth_surface.py; this synchronizes proof-depth surface language and does not prove semantic adequacy
Semantic proof adequacy audit	Review whether each finite-record predicate is the right formalization of its intended chapter boundary.	implemented in docs/proof_adequacy_review.md; checked by python3 scripts/validate_proof_adequacy_review.py; classification and no-promotion audit only
Historical-project semantic-depth fixture	Distinguish field presence, finite route, derived invariant, executable-model bridge, and implementation binding while preserving abstraction losses, assumptions, runtime exclusions, and no-promotion boundaries.	implemented by python3 scripts/validate_formal_semantic_depth.py: one blocked record and ten expected-invalid mutations; no arbitrary adequacy or deployed-enforcement result

70.14.1 Formalization hooks

Tag	Module	Target	Status
lean:proofs.envelope.operational_invariant	AsiStackProofs.ProofEnvelope	An exact formal-artifact authority lease preserves target, proposition, verifier, consumer, implementation, environment, expiry, support, and effect custody over arbitrary runs; artifact versions increase only on explicit change; a ten-event witness invalidates, re-verifies, rebinds, reissues, and revokes.	implemented
lean:proofs.envelope.failure_blocks_promotion	AsiStackProofs.ProofEnvelope	Lease issuance rejects mismatched identity, missing artifact, adequacy, consumer, limitation, or non-claim boundaries, expiry, support promotion, or external-effect authority; rejected events are noninterfering, revoked states absorb suffixes, thin summaries cannot recover boundary-sensitive issue decisions, and complete transport preserves steps.	implemented

These Lean hooks are implemented as authored finite-record predicates for proof-target status discipline and a reachable formal-artifact authority lease. They do not inspect the repository filesystem directly, discover missing proof opportunities, validate external theorem IDs, judge semantic adequacy, or promote any broad book claim beyond its recorded support state.

The formal audit counts 28 declarations in ProofEnvelope.lean: five retained negative cases and 23 lifecycle and transport results. The lifecycle preserves target, proposition, verifier, consumer, implementation, environment, expiry, support, effect, version, and receipt custody over arbitrary successful runs. It includes reachable issuance, explicit artifact-version invalidation, re-verification, re-binding, reissuance, expiry, and reason-bound revocation; exact rejected-event noninterference; absorbing revocation; one summary collision proving that a thin view cannot recover boundary-sensitive issue decisions; and complete transport that round-trips, is injective, and preserves steps. The independent Python consumer recompiles the module, reconstructs the ten-event trace and all eleven prefix/suffix splits, checks 33 rejected routes, and rejects mutations to each of the 19 transported fields. None of those authored fields establishes artifact or source truth, filesystem discovery, semantic adequacy, implementation refinement, runtime enforcement, external theorem applicability, system safety, capability, cost, reproduction, transfer, or support-state movement.

70.15 Source crosswalk

Source ID	Title	Layer	Planned use	Readiness
genesiscode	GenesisCode	executable_specification	Tiny pure calculus + obligations + provenance for auditable AI-symbiotic programming.	source note available; local raw cache available
spinoza	Proof of Belief / The Spinoza Architecture	reasoning_epistemology	Neurosymbolic belief, transparent axiomatic AI belief systems, verification, belief revision.	source note available; local raw cache available
scf	Stable Capability Fields	governance_recursive_self_improvement	Stable boundaries, replacement, bounded authority, recoverable evolution.	source note available; local raw cache available
talos	Talos Protocol	labor_execution_os	AI labor OS. Deterministic cognitive manufacturing, typed jobs, control planes, auditability, tool isolation.	source note available; local raw cache available
viea	Verified Intent-to-Execution Architecture	whole_stack_execution_spine	Intent -> command contracts -> artifacts -> routing -> runtime targets -> verification -> deployment -> feedback.	source note available; local raw cache available
circle_calculus_core	Circle Calculus	proof_carrying_mathematical_substrate	Proof-carrying finite cyclic mathematics project with Lean proofs and theorem manifests.	source note available
circle_ai_contract_suite	Circle Calculus AI Contract Suite	proof_carrying_ai_contracts	Theorem-linked AI contract families with explicit non-claims.	source note available
rope_position_certifier	Proof-Carrying RoPE Position Distinguishability	proof_carrying_position_contract	Exact/discretized RoPE position receipt boundaries and non-claims.	source note available
proof_carrying_circular_computation	Proof-Carrying Circular Computation	proof_carrying_compute_substrate	Certified cyclic address/rewrite track with benchmark boundary.	source note available
cca_project	Constructive Cognitive Architecture	local historical-project lineage	Abstraction maps, typed calculus boundaries, by-construction properties, and the difference between contract structure and broader semantics.	source note available
moecot_manifest_project	MoECOT Manifest compiler-era project	local historical-project lineage	Pass/reproducer/legality artifacts, internal-contract breadth, and the boundary between executable models and external behavior.	source note available
corbens_best_model_possible_project	Corben’s Best Model Possible	local historical-project lineage	Negative cases for vacuous checks, playback/live-replay confusion, absent current builds, and missing implementation binding.	source note available

70.15.1 Manifest source assignment reconciliation

These rows keep Executable Specifications and Lean Proof Envelope’s manifest assignments visible at their recorded review boundary. Passage review does not establish local reproduction, performance, safety, deployment, or support-state movement.

Source	Intake role	Boundary
precision_contract	Metadata-first comparator: The Precision Contract: A Functional Rate–Distortion Theory for Behavior-Preserving Neural Computation. Corben-authored July 2026 theoretical and systems paper replacing universal per-weight precision questions with a contract-relative functional rate-distortion problem over complete executable descriptions. It proposes representation canonicalization, protected-behavior contracts, precision fields, progressive base/residual encoding, dynamic routing, full physical and assurance-cost accounting, a Functional Precision Compiler, and scoped precision certificates. Existing chapters are upgraded first; no universal bit bound, implemented compiler, preserved-behavior result, efficiency result, certificate validity, support promotion, SOTA, AGI, or ASI claim is inferred.	No passage-level source claim, local implementation, reproduction, safety, performance, deployment, support-state, or ASI result is established by this reconciliation row.
ext_reluplex_2017	Passage-reviewed comparator: Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks. Supplies a concrete neural-network verification case in which a solver checks a stated property over a bounded ReLU network region.	The theorem concerns only the encoded network, property, arithmetic semantics, and region; it does not prove model intent, data quality, whole-system safety, or deployed implementation binding. No local implementation, reproduction, performance, safety, deployment, support-state, or ASI result is established by this reconciliation row.
forward_transfer_program_synthesis	Passage-reviewed comparator: From Compression to Forward Transfer: Evaluating Reusable Knowledge in Program Synthesis. Separates a verified semantic abstraction from verified lowering, emitted-artifact validity, and measured forward transfer, and supplies exact outcome and verification-level vocabularies for each boundary.	No Lean theorem, solver run, certificate check, compiler validation, emitted-artifact validation, or transfer experiment was executed for this source. No local implementation, reproduction, performance, safety, deployment, support-state, or ASI result is established by this reconciliation row.

70.16 Summary

The proof envelope makes formality useful by staying small, operational, and bounded. Lean proves only what Lean checks. Schemas validate shape. Tests validate behavior. Benchmarks validate measured claims. The living book must keep those lanes separate.

The same separation applies to performance pressure. A benchmark result can raise confidence only when its run record, baseline, residuals, regression floor, and anti-Goodhart checks are explicit.

The proof envelope should let a reader tell exactly what was proved, what was merely validated, what was tested, what was benchmarked, and what remains prose. If those lanes blur, the proof envelope has become decoration. The immediate value is local: small invariants about authority ceilings, field replacement, evidence transitions, budget records, context mounts, and proof receipts can be checked without pretending that the entire architecture has been formalized. The longer-term value is cultural. Agents improving the book or the stack should learn that mechanized claims need artifacts, commands, and failure records. Formality is useful when it reduces ambiguity and overclaiming; it is harmful when it becomes ornamental confidence.

70.17 Evidence reconciliation (2026-07-16)

The invariant protocol, field meanings, and inference limits are stated once in Living Book Methodology. This packet contains only the chapter-specific projection; its authoritative per-atom rows are the executable-specifications-and-lean-proof-envelope slice of experiments/claim_family_terminal_coverage/results/result.json.

The core remains blocked after full attempt at argument support. The strongest family attempt was Full-state update and unlearning causal campaign. Its exact boundary is: Broad unlearning claim is narrowed with no support promotion; behavioral removal is not influence, privacy, legal, storage, backup, or descendant erasure. Across 73 atoms, the terminal ledger records 73 blocked_after_full_attempt.

Chapter-specific field	Value
Family / atom denominator	CF-07 / 73 atoms
Terminal dispositions	73 blocked_after_full_attempt
Core	executable-specifications-and-lean-proof-envelope.core: blocked_after_full_attempt at argument
Core attempted / missing lanes	causal, empirical, executable, formal, source-synthesis / normative, transfer
Attempted local lanes	causal, empirical, executable, formal, source-synthesis
Missing or unproved lanes	normative, transfer
Strongest family bundle	Full-state update and unlearning causal campaign (end_to_end): One adequate five-seed, seven-arm terminal campaign preserving two prior instrument failures and separate behavioral, influence, privacy, lineage, storage, backup, and descendant axes.
Negative controls	deletion retrain comparator; approximate mitigation arms; 15 rejecting mutations; failure-lineage preservation.
Accepted transitions	v1_0_pilot.proof_envelope.no_change
Maximum inference	Broad unlearning claim is narrowed with no support promotion; behavioral removal is not influence, privacy, legal, storage, backup, or descendant erasure.
Reproduction / next burden	Replay scripts/validate_p4_m7_update_unlearning_v3.py and scripts/validate_claim_family_terminal_program.py; fill the named atom-specific lanes under a new prospective protocol.

70.18 Handoff

Executable specifications and Lean predicates define which narrow claims can be checked, but evidence pressure also needs a path for measured capability without Goodhart collapse. Benchmark Ratchets and Anti-Goodhart Evidence takes that role. It turns benchmark runs into records with baselines, residuals, regressions, saturation states, contamination boundaries, and promotion decisions so measured pressure cannot outrun preserved failures.