Interpolant Envelope

Status: active research probe; conjectural outside the checked finite core.

Promotion is not authorized. Neither accession to the Technical Spine as a paper family nor a stable Bulla API may be claimed from this work. The unmet accession gate is recorded in papers/research-status.yaml: end-to-end abstraction-to-code verification, foreign semantics, and open-world claims remain unresolved.

Publishing the record is a separate act and is authorized. paper.md is the gate report as a typeset frontier record, carrying that accession gate on its first page. This sentence previously read "public paper promotion ... not authorized", which was read as forbidding the record itself and left this directory contradicting the authority, where the entry is public: true with an external-review packet prepared.

#Implemented

#Language, semantics, and certificates

• FRSL-1 finite relational syntax and direct semantics.
• Exhaustive model enumeration with explicit bounds.
• Full definitions, partial RELY/REFUSE surfaces, and ESCALATE residuals.
• Same-shared-reduct/different-target countermodel certificates.
• CHOICE_REQUIRED for exact-minimal definitions that remain inequivalent over some reachable shared-signature structure outside the local theory.
• Result v0.2 causes, typed next actions, enrichment plans, and a choice quotient that collapses observational duplicates before governance.

#Packages, receipts, and verification

• Closed package metadata: protected signature pins, evidence requirements, authority, scope, expiry, verifier, cost, and proof references.
• Independent replay of gluing, protected-language use, definition, preserved refusals, canonical form, and package binding.
• Ordinary ActionReceipt recording through the open action type bulla.invent; ActionReceipt v0.2/v0.3 is unchanged.
• Compile-once/apply-many caching, strict evidence adapters, receipted package selection, exact reliance-policy binding, and replayed application receipts.
• Exact inclusion-minimal reliance-repair catalogs and fresh-reason vocabulary checks for bounded precedent compilation.
• A zero-Bulla-import standalone verifier.
• A version- and hash-pinned SMTInterpol 2.5 adapter with retained raw artifacts, separate RESOLUTE proof checking, and exhaustive post-verification; missing, unknown, timeout, and unsupported output remain INDETERMINATE.
• A provider-neutral LLM-candidate protocol with provenance and hard disclosure budgets; no model output is trusted without the same package verifier.

#Witnessing, benchmarks, and monitoring

• Signed experimental witness checkpoints, append-only checkpoint archives, extension checks, and a read-only transport.
• Sixty frozen benchmark instances across twelve seam families, a twenty percent holdout, and eight fail-closed adversarial controls.
• A bounded J-tuple precedent compiler, protected-consequence legislation detector, and reliance-cut explainer.
• A common-filtration e-process monitor using an arbitrary-dependence weighted arithmetic merger, exercised in full, opaque, regenerated, and sparse arms.
• A Lean 4.28 finite semantic spine with no sorry and a local axiom audit.
• A two-live-local-tool semantic-control-plane demo and frozen external-pilot intake/adjudication contracts.
• Logic passports, conservation manifests, exact observable separating-set plans, componentwise burden frontiers, and signed enrichment handshakes.

#Certified refinement

• Certified world-set refinement with typed PRESERVE, REFINE, REVISE, and ROUTE movements, epoch staleness, and ordinary transition receipts.
• An isolated refinement checker, a complete transition/transparency demo, and a frozen 240-case scaling study.

#Not implemented or not established

• A constructive Beth theorem for geometric sites.
• A verified compiler from FRSL-1 JSON bytes into the Lean semantics.
• Unbounded first-order interpolation or model extraction.
• A repository-bundled SMTInterpol jar or Java runtime. The lock file pins the official artifact; operators supply the matching binary out of band.
• LLM benchmark arms against the new frozen holdout.
• External-domain adjudication or production prevalence.
• Production checkpoint federation, plurality, stake, slashing, slot runtime, witness-pool operation, or revocation transport.
• A stable Bulla predicate wire format.

#Trust boundary

The exhaustive checker is the reference semantics. SMTInterpol and LLMs may propose candidates but cannot promote them. The Lean file proves the abstract finite obligations; Python tests currently mediate the abstraction-to-code boundary. This is stronger than unchecked synthesis and weaker than an end-to-end verified compiler.

See PREREGISTRATION.md for frozen gates and OWNERSHIP-MATRIX.md for novelty boundaries.

The benchmark uses family-specific vocabularies and three-state boundary domains, but remains a curated synthetic regression corpus. Its outcome mix is constructed and its expected statuses are known to the generator. Holdout success tests implementation stability; it does not estimate how often real disputes are safely compilable.

See FRSL-1-SPEC.md for the closed language, package, certificate, result, and receipt-binding formats. See INTERNAL-GATE-REPORT-2026-07-18.md for the current frozen evaluation and promotion decision; the July 17 report is historical.

The subsequent implementability sprint is specified in CERTIFIED-SEMANTIC-REFINEMENT-SPRINT.md. Its current disposition is recorded in CERTIFIED-REFINEMENT-GATE-REPORT-2026-07-18.md, with open attacks in CERTIFIED-REFINEMENT-HOSTILE-REVIEW.md.