RFC-2: The certification surface — from a ladder to a coordinate system

[maxinelevesque]

RFC-2: The certification surface — from a ladder to a coordinate system

Status	Draft for discussion — not routed, not content-pinned
Supersedes	RFC-1 §2 (the ladder), §9 (certificates), §11 (the trust base) — presentation only
Preserves	RFC-1 §3–§5, §10, §13 unchanged. No mechanism, engine, or admission rule changes.
Baseline	dollspace-gay/Thermite @ 84d276e7 (gates G1–G4 shipped)
Companion	The assurance-order metatheory (§4) — a separate document, per the RFC-1 pattern

Contents: §0 Problem · §1 Coordinates · §2 Rendering · §3 The lattice · §4 Aggregation is deferred · §5 Dual labels · §6 Removing Lx · §7 Increments · §8 Unchanged · §9 Open questions

---

0. The problem

RFC-1 graded every obligation on a five-rung scalar ladder and stated the rungs mean refutation quality ("rank means refutation quality", §2). That was true when written, and it stopped being true the moment two mechanisms shared a rung.

Today Level::L3 denotes both:

• a general Verus/Z3 result — proven for all inputs, refutation incomplete (Z3 may return unknown), trust base ~500 kLOC of solver; and
• a Lean forge result — proven for all inputs, refutation absent (a failed proof is a stuck goal; the covenant is empirical), trust base a small kernel plus a per-item axiom gate.

These differ on both axes RFC-1 cares about, and they differ in opposite directions. Verus refutes better; Lean is trusted less. A scalar cannot carry that, so the scalar silently stopped meaning what §2 said it meant.

This is not a defect introduced by any one change — it is what a lossy projection does under load, and the collision predates any recent work. RFC-1 even anticipated it: §12 lists configuration C4 ("grid ladder — refutation × trust as a product surface") and demotes it to metadata on legibility grounds:

The 2-D decomposition is true and lives in the trust: field and make audit;
the ladder keeps the product's legibility.

RFC-2 revisits that call with the metatheory that did not exist then: the S₂.0 classifier, checked reconstruction at QF_LIA/QF_BV/EPR, the covenant, per-run translation validation, and boundary-closure classification. The decomposition is no longer theoretical — every coordinate is already computed and stored. Only one of them is rendered.

RFC-2's claim: the decomposition won. Render it.

1. The four coordinates

Each already exists in the implementation. None is new work to compute.

1.1 Scope — what the claim quantifies over

value	meaning	source
all	holds for every input	Verus/Z3, Lean, cage routes
bounded(n)	holds for every input up to size n	Kani/CBMC
per-exec	checked at the call site, this execution	runtime contracts
none	nothing is claimed about the body	#[slag]

1.2 Refutation — what a false clause yields

This is RFC-1 §9's falsification_channel. It was specified and never shipped — manifest.rs carries trust but no falsification field.

value	meaning	witness
complete	mechanically complete in-fragment	real point · bit pattern · finite structure
incomplete	a countermodel when the solver finds one; unknown possible	Verus counterexample
empirical	no mechanical refutation; a seeded generator attacks the claim	covenant CovenantRefuted
trace(n)	a concrete trace within the bound	Kani trace
abort	detected in production, at the violating call	L1 abort
none	—	#[slag]

Refutation is a property of the fragment, not of the proof. It classifies the question, not the answer. A successful complete certificate and a successful empirical certificate establish the same proposition; they differ in what the system can tell you when the claim is false, or when the code changes. Lx obscured this by looking like a quality score on the artifact.

What decidability buys is precisely the model-finding direction:

¬φ satisfiable ⟺ the procedure exhibits a model of ¬φ.

That biconditional is why complete means something: a valid answer carries the information no countermodel exists, because the procedure would have found one. Outside a decidable fragment there is no such guarantee, and three situations collapse into one observable stuck goal — φ is false, φ is true but unproven, φ is true but unprovable here.

1.3 Trust — what discharging this clause asks you to believe

Already shipped as Certificate::trust (forge/src/manifest.rs:266). Trust is a set, not a scalar.

value	meaning
lean-checked	Lean re-checked the actual req → clause theorem; the solver is a proof producer and leaves the trusted base
lean-lemma	Lean proved a bridge lemma licensing the route (e.g. r_relax_sound); the solver remains trusted
solver	Z3/Verus soundness, per query
fiat	trusted by declaration

inspection is a modifier, not a value (resolving OQ-3): the Rust↔Lean renderers stay inspection-tier even after reconstruction — bv_kernel_checked_trust_profile carries a residual "renderer correspondence remains inspection-tier" item alongside its lean-checked claim.

Trust splits into residual and discharged. A naive union is wrong: it makes the relax route {solver, lean-lemma} a superset of plain cage {solver}, and therefore "worse," when the bridge lemma is not a liability but a discharged obligation. Ordering by residual risk under set inclusion gives the right answer for free:

position	residual
lean-checked	{inspection, rustc}
solver, solver + lean-lemma	{solver, inspection, rustc}

{inspection, rustc} ⊂ {solver, inspection, rustc}, so trust is a two-element chain and lean-checked strictly dominates — with no metatheory required. And the relax route comes out equal to the unreconstructed cage rather than worse, which matches RFC-1 §12's own characterization of ℝ-relaxation as a coverage win rather than an assurance-rank win.

Note the deliberate absence of the word kernel: it is claimed by the Lean kernel, the seccomp filter, the OS-kernel target, and the "kernel-grounded" descriptor. See the nomenclature issue.

The distinction this axis exists to preserve. Reconstruction is {lean-checked} — Z3 is gone entirely (engine.rs:130: "the SAT solver and LRAT converter are proof producers only: neither remains in the trusted base"). The relax route keeps Z3. Today the audit cannot tell them apart: KERNEL_CHECKED_TRUST_MARKER is the substring "kernel-checked", and r_relax_sound's description ends in that substring, so the marker fires for both. That is the same scalar-collapse pathology as the L3 blur, one layer down. (Filed separately per §7.)

1.4 Boundary — how far the claim closes

Already shipped (f78dd664, 2026-06-05, "end-to-end vs to-the-boundary classification"), typed as AssuranceScope.

value	meaning
e2e	the claim closes over the item's whole call graph
to_boundary	closes to declared #[boundary] contracts, which are assumed
to_platform(p)	closes to a named frozen platform registry p

Boundary is orthogonal to the ladder and always has been: a clause can be fully proven and to-the-boundary — its own contract verified, the whole-program guarantee still resting on a foreign body. Level and boundary answer different questions: how well is this proven versus how far does the proof reach.

2. The rendering

scope/refutation/trust@boundary

rendered	what it is
all/complete/lean-checked@e2e	caged and reconstructed — the strongest position available
all/complete/{solver,lean-lemma}@e2e	the nlsat relax route
all/complete/solver@e2e	caged, reconstruction not yet available for the fragment
all/incomplete/solver@e2e	general Verus/Z3
all/empirical/lean-checked@e2e	the Lean forge
all/incomplete/solver@to_platform(x86_64-pc-uefi-smp-v1)	a kernel core, stated honestly
bounded(8)/trace(8)/solver@e2e	Kani
per-exec/abort/fiat@e2e	runtime contracts
none/none/fiat@e2e	#[slag]

The two rows that render identically as L3 today — general Verus/Z3 and the Lean forge — are now visibly different objects.

3. The lattice

3.1 Coherent cells

The coordinate product is mostly empty, and the emptiness is structural. Refutation is functionally determined by scope everywhere except all:

scope	admissible refutation	why
none	none	nothing is claimed, so nothing to refute
per-exec	abort	a runtime check can only fail at the violating call
bounded(n)	trace(n)	which is "complete, relative to the bound"
all	complete · incomplete · empirical	the only free choice

Further constraints: fiat ⟹ scope ∈ {none, per-exec} (claiming all inputs by declaration just is #[slag]); incomplete ⟹ solver ∈ residual (if Lean re-checked it, the route was decidable, hence complete); empirical ⟹ lean-checked (empirical refutation is the covenant, a forge construct).

Incoherent a priori — a certificate landing in one of these is a schema violation and a real bug detector:

all/*/fiat          none/{≠none}/*        bounded(n)/complete/*
per-exec/{complete,incomplete,empirical}/*
all/incomplete/lean-checked                all/empirical/solver

Eight coherent cells, five of them in all:

none/none/fiat                        (slag)
per-exec/abort/fiat                   (runtime)
bounded(n)/trace(n)/solver            (Kani)
all/complete/lean-checked             (reconstructed cage)
all/complete/{solver, lean-lemma}     (relax route)
all/complete/solver                   (cage, unreconstructed)
all/incomplete/solver                 (general Verus)
all/empirical/lean-checked            (the forge)

3.2 Seven order-elements

The relax route and the unreconstructed cage have identical residual, refutation, and scope — they are order-equivalent, different routes to one position. So eight cells collapse to seven distinct elements.

                 A                 all / complete   / lean-checked
                / \
               /   \
              B     \              all / complete   / solver   [≡ relax route]
              |      \
              C       D            all / incomplete / solver
               \     /             all / empirical  / lean-checked
                \   /
                  K                bounded(n) / trace(n) / solver
                  |
                  R                per-exec / abort / fiat
                  |
                  S                none / none / fiat

This is a bounded lattice. Top A, bottom S, and both non-trivial pairs have meets and joins:

pair	join	meet
B ∨ D	A	K
C ∨ D	A	K

The meets are worth reading: the greatest common assurance of the forge and any solver route is Kani. That is the honest answer to "what can I claim about a module mixing forge and cage clauses without appealing to either's distinctive strength."

3.3 The obstruction is exactly N₅

The sublattice {K, C, B, D, A} is the pentagon:

        A
       / \
      B   \          K < C < B < A     (chain of length 3)
      |    D         K < D < A         (chain of length 2)
      C   /          D ∥ C,  D ∥ B
       \ /
        K

N₅ is the forbidden sublattice for modularity, so the assurance order is non-modular, hence non-distributive. That is the formal statement of a fact the implementation kept rediscovering: the axes genuinely interact, and no amount of per-axis reasoning recovers the whole structure.

Two consequences the documents should carry:

Any total order must invent a comparison. A linear extension always exists, so RFC-1's scalar ladder was not wrong to be totally ordered — it was wrong to be silent about which relation it added. The fiat is B ∥ D and C ∥ D being forcibly ordered. The L3 blur is C ∥ D being forcibly identified, which is strictly worse: an invented equality rather than an invented inequality.

The pentagon names the companion's subject. {Kani, general-Verus, cage-solver, forge, reconstructed-cage}. The companion document's job is to characterize that one obstruction — prove the cell inventory complete, prove N₅ is the only non-modular sublattice, and decide whether the forge ∥ solver edge stays incomparable or earns a principled orientation.

3.4 Comparison and floors

• Certificates compare by product order. Incomparable pairs are reported incomparable, never silently ordered.
• Acceptance gates compare against a declared set of floor tuples, accepted on dominance over any member. For a single floor this is identical to per-axis minimums, so the set form costs nothing until needed — and it is already needed: the strict artifact path requires @e2e while a platform-image path requires @to_platform(p). Two acceptable positions, not one floor.
• The floor set is declared in-repo, versioned under RFC-3's contract, not computed per command. Scattered acceptance constants are how a build path comes to invent its own criterion privately.
• make audit reports the Pareto frontier plus the weakest link per axis, and the residual-trust statement stays the last thing it prints.

4. Aggregation is deferred

Composing clause tuples into item tuples, and item tuples into artifact tuples, is not per-axis minimum, and RFC-2 deliberately does not specify it. Three known failures of the naive rule:

1. Refutation is fibered over scope. complete means complete relative to the scope claimed. bounded(8)/trace(8) and all/complete both say "complete" and mean different strengths; comparing across fibers without normalizing is a category error.
2. Boundary acts on refutation. A clause completely refutable @to_boundary is completely refutable modulo the assumption — a counterexample to the whole-program property can live inside the foreign body, where no channel observes it. Boundary acts on the other axes rather than beside them.
3. Trust is not flat (§1.3): residual composes, discharged does not.

This follows RFC-1's own precedent. §3 shipped the admission test while deferring its characterization:

the precise admitted arithmetic–quantifier mix is the stage-2 metatheory
deliverable (§12)

Same move: ship the surface, name the deferred characterization, make it a numbered deliverable rather than an unstated gap. Until the companion lands, forge reports per-clause tuples and the weakest link on each axis separately, and computes no single composite claim. The existing aggregation sites keep computing exactly what they compute today.

The companion must also prove its operator agrees with what forge check computes — the same discipline as classifier_correct. Metatheory that merely coexists with the implementation is how drift starts.

5. Dual labels and the collapse policy

Every claim is validity relative to a frame, and the fragment plus decision procedure are what fix the frame. Different audiences need different amounts of that frame.

So a certificate carries two labels, both stored, neither derived at read time:

• engineer label — what changes a decision: "proven for all inputs; a false clause gives you a concrete failing input."
• formal label — the tuple plus frame: fragment, procedure, axioms, residual.

Presentation is progressive disclosure: the engineer label on the front page, the frame behind --explain, the lattice position in the audit.

The rule that makes this safe:

Collapsing two formal positions into one engineer label is permitted, and is
governed by an explicit, versioned collapse policy. Collapsing them
silently is a schema violation.

This is the piece that prevents the L3 blur recurring. The blur was never wrong because two mechanisms shared a label — it was wrong because nothing declared the collapse, on what grounds, for which audience. A declared collapse is a reviewable design decision. An undeclared one is drift that looks like a decision.

6. Removing Lx

Lx is removed, not retained — deleted from the certificate schema, audit output, skill, and README during the 2.0.0-beta line. The tuple becomes the sole certification surface.

A lossy projection kept "for skimming" is a projection someone will eventually gate on, guaranteeing a second source of truth and slow drift back to the collision this RFC exists to fix.

The migration table is a translation aid for readers of historical certificates, not a live projection:

historical Lx	tuple
L4	all/complete/*
L3	all/incomplete/* or all/empirical/* — ambiguous; the collision class
L2	bounded(n)/*
L1	per-exec/*
L0	none/*

The L3 row is the point: historical L3 certificates cannot be mechanically migrated, because the number never carried enough information to tell the two cases apart. That is the clearest argument for the change, and why removal is cheaper now than later.

Migration cost, measured. The checked-in oracle corpus is 12 .cert.json files (10 at L3, 2 at L0), hand-authored and compared as subsets. Subset comparison means R2-1…R2-5 do not break them at all — only removing Lx does, and that is 12 files to re-cut by hand. There are no external consumers to migrate: version 0.0.1, two tags, no releases.

Per RFC-3, removing Lx breaks both the certificate schema and the assurance semantics — permitted within the beta line, and the reason 2.0.0-beta is where it lands.

7. Increments

#	increment	surface	risk
R2-1	Ship falsification_channel per RFC-1 §9	manifest.rs, cert schema v3	low — additive
R2-2	trust as a set; split lean-checked/lean-lemma; order by residual inclusion	manifest.rs, engine.rs	low — already the semantics
R2-3	Surface boundary in the per-clause record	manifest.rs	low — exists at item level
R2-4	Coherence validation: reject certificates in incoherent cells (§3.1)	manifest.rs	low — additive, and a bug detector
R2-5	Render the tuple; dual labels + declared collapse policy (§5)	manifest.rs, audit.rs	medium
R2-6	Product-order comparison, declared floor set, Pareto frontier	audit.rs, new policy file	medium
R2-7	Retire the level-as-verdict idiom	10 call sites	low — arguably a bug fix
R2-8	Classification certificate — emit the fragment verdict pre-discharge	manifest.rs, check.rs	medium
R2-9	Remove Lx from schema, audit, skill, README	everywhere	high — breaking; requires R2-1…R2-8

No engine, admission-rule, or solver path is touched by any increment.

R2-7, sized

Level is mentioned 288 times across forge/src and thermite-*/src, but only 23 are real comparisons, in five shapes:

shape	count	what it actually is
verdict proxy	10	cert.level == Level::L3 && cert.reject.is_none() — asking did it prove, not where does it sit. Should read CertVerdict::Proved.
floor	4	< Level::L3 in the build/image path — the only true floors
aggregation	6	min-over-clauses; unchanged pending §4
downgrade clamp	1	check.rs:2158
bounded check	1	kani.rs:370

Correction to an earlier assumption: G2Checks.g2_flip_permitted does not read a level. It is declared && checks.all_green() over four booleans (axiom_probe, doc_drift, differential, two_phase_tv). Removing Lx does not touch it.

The verdict-proxy shape is the same scalar-overload pathology one level further down — it is why L3 kept accreting meanings — and fixing it is arguably a bug fix independent of this RFC.

R2-8, the classification certificate

The S₂.0 classifier returns Admitted | Rejected(reason) | Unknown and drives routing, but nothing about the fragment is persisted: thermite_spec::classifier::classify is referenced once outside its own crate (cli.rs:2001), and manifest.rs has no admission field. The frozen RejectReason vocabulary dies at the CLI boundary.

Map that onto §3 and the structure is exact:

classification determines the refutation coordinate (which fiber) ·
discharge determines the trust coordinate (position within it)

Two phases, two coordinates — and only the second is recorded. Consequences:

• The best achievable rung for a clause is statically computable and cheap, yet cannot be answered without running the whole pipeline.
• "Escalate UP, never degrade down" is not independently auditable. You cannot verify a clause reached the forge because the cage genuinely could not hold it, versus because a cage attempt timed out. RFC-1 §2 requires the classifier "name why — a routing reason from a frozen vocabulary, never a bare refusal." That vocabulary exists and is discarded.
• Pre-discharge code has no artifact describing what it logically is.

Today's certificate is a post-mortem. R2-8 adds the prognosis, which is the more fundamental of the two: it determines the coordinate the post-mortem later fills in.

Out of scope, filed separately

Per the presentation-only boundary: the KERNEL_CHECKED_TRUST_MARKER substring conflation; the dual closure classifier (verified_closure vs the legacy one); to_platform_boundary as a raw string outside AssuranceScope. Each is a defect against the axes RFC-2 defines, not a change to them.

8. What RFC-2 does not change

RFC-1 §3 (cage admission), §4 (numeric routing, @bv and the three locks), §5 (the forge, the covenant, the meaning audit), §10 (anti-Goodhart), and §13 (limits) stand unmodified. The seven verdicts stay closed. Covenant-before-burn stays structural. This RFC is about how the system reports what it already does.

9. Open questions

• OQ-1 — Does refutation need a reconstructed value distinct from complete? Current view: no — trust carries it, and a reconstructed and a solver-trusted cage clause refute identically.
• OQ-2 — Should the covenant's falsify budget appear in the refutation coordinate (empirical(50000))? Argues for; costs schema churn.
• OQ-3 — Is inspection a trust value or a modifier? Resolved: a modifier (§1.3).
• OQ-4 — Does the partial order break g2_flip_permitted? Resolved: no — it reads four booleans, not a level (§7). The floor question is settled at §3.4: a declared set of floor tuples, dominance over any member.
• OQ-5 — How do historical L3 certificates migrate? Resolved: they do not need to. 12 hand-authored oracles compared as subsets; re-cutting them is a chore, not a design question (§6).
• OQ-6 — Does the boundary modality preserve the lattice, or does it fail to distribute over the pentagon? Expectation: it does not distribute, which would make it a second obstruction. Companion question.
• OQ-7 — Who owns the collapse policy (§5), and what is the review bar for changing it? A collapse policy nobody reviews is an undeclared collapse with extra steps.

[maxinelevesque]

Companion: RFC-3 (versioning) is #120. The two are coupled — removing Lx (R2-9) breaks both the certificate schema and the assurance semantics, which RFC-3 §4 permits inside the 2.0.0-beta line and which is the reason that line exists.

One prerequisite worth flagging from drafting RFC-3: Certificate carries no schema version field (forge/src/manifest.rs:489; CHECK_SCHEMA_VERSION is a private cache-key const in cache.rs:126, not a certificate field). So a consumer holding a certificate cannot tell which schema produced it. That is RFC-3 R3-1, it is one additive field, and it should land before any increment here that changes the schema.

[maxinelevesque]

The trust axis, worked through — and a revision to §3

Following up on §1.3 and §3 with the metatheory this needed. The short version: the non-modularity in §3.4 is not fundamental, it is caused by two empty cells that are artifacts of what is currently implemented, and filling them repairs the algebra. That changes the case for extending reconstruction from "better trust" to "structural repair."

1. The order is a fibration, and the interesting fibre is not a lattice

Refutation is functionally determined by scope everywhere except all (§3.1), so the position space is a dependent sum over the scope chain rather than a product. Three fibres are singletons. All structure lives in the all fibre.

And that fibre is not a lattice on its own. Take {B, D} — cage-solver and forge. Lower bounds within the fibre: C ≤ B but C ∥ D, and nothing else is below both. There is no meet in the fibre. The seven-element lattice only closes because K, from the bounded fibre, supplies the missing meet.

So the meet of two all-inputs positions escapes its own fibre and lands in a weaker scope. That is §4's composition problem stated structurally, and it is a better statement: the issue is not that composition is hard, it is that the fibre is not closed under meet.

2. The non-modularity comes from two holes

Lay the all fibre out as refutation (3-chain) against trust (2-chain):

	lean-checked	solver
complete	A	B
incomplete	hole — K2 forbids	C
empirical	D	hole — K3 forbids

Six cells, four occupied. If the grid were full the fibre would be 3-chain × 2-chain — a product of chains, hence distributive, closed under meet and join, and N₅ would not exist. The pentagon arises entirely because D reaches the top in one step while C needs two, and that asymmetry is the shape of the missing cells.

Which leads to the observation that reframed this for me:

§4.2's counterexample is precisely one of the holes.

C ⊓ₐ D = (all, empirical, solver) — the position §4.2 proves "incoherent" — is the bottom-right cell. The per-axis operator was computing the correct product meet all along. K3 was telling it the answer did not exist.

3. Neither hole is necessary

(empirical, solver) is arguably already occupied and mislabelled. Any Verus clause outside the admitted fragment is proved-or-shrug: MBQI fails to build a finite model, Z3 returns unknown, or the model names uninterpreted-function values that do not map back to a concrete Rust input. Those clauses certify today with refutation implicitly incomplete, which overstates what you get. incomplete is conflating "the procedure sometimes produces a witness" with "the procedure structurally cannot produce one for this shape."

The mechanism that fills it properly: extend the covenant to out-of-cage Verus clauses. RFC-1 §5 attached inhabit/falsify to the forge because that is where stuck goals were expected — but a non-admitted Verus clause has the same failure mode. The generator already exists (thermite-tv's SplitMix64, already shared by three consumers) and so does the covenant engine. It also suggests generalising the ordering rule: covenant-before-burn becomes covenant-before-discharge, since a falsifier hit means you never needed to solve.

(incomplete, lean-checked) is reconstruction extended past the decidable fragment. Nothing about kernel-checking requires decidability — Lean will check a proof of anything. K2 is a fact about how reconstruction was built, not about logic.

4. What is actually forbidden

Scoping this by what theorems prohibit rather than by difficulty estimates:

theorem	forbids	does not forbid
Matiyasevich	a decision procedure for nonlinear integer arithmetic	checking any particular proof that exists
Gödel / Church	a complete procedure for provability	kernel-checking a given term
Goldfarb	decidable HO unification outside the pattern fragment	checking a term whose implicits are resolved

All three constrain finding proofs, not checking them. Kernel type-checking is decidable everywhere; RFC-1 already names its only real limit as KernelBudget — "decidable but non-elementary in cost" — which is a resource verdict, not a wall.

So: nothing forbids reconstructing any proof that exists. What is forbidden is a complete procedure that always finds one. Reconstruction is a checking problem, and search is untrusted by construction — which is exactly the architecture Reconstruct.lean already uses for QF_BV, where the SAT solver is a proof producer and the kernel evaluates the LRAT check.

5. Consequences, including one correction to my own scoping

Instantiation replay is the cheapest remaining extension, not the hardest. A general Verus VC is discharged by quantifier instantiation. Record the instantiations, apply them, and the residual goal is quantifier-free — which drops straight into a path that already works. Crucially the instantiations need no trust: if the residual checks, the proof is valid however they were chosen. Same proof-producer architecture as the SAT solver in the BV path; MBQI rather than CDCL changes nothing about the trust story.

The relax route can reach lean-checked, which I had written off. I had assumed nlsat reconstruction meant replaying a CAD trace, which is impractical. That is the wrong certificate format. For a universally quantified polynomial claim over ℝ — exactly what the relax route handles — the natural certificate is Positivstellensatz / sum-of-squares, and checking one is polynomial identity verification, which is ring-level in Lean. Degree bounds are astronomical in the worst case, but that is complexity, not impossibility, and certificates for real program obligations are typically low-degree.

Since r_relax_sound — the ℝ→ℤ bridge — is already kernel-proven, only the real-side result is solver-trusted. An SOS certificate moves the whole route B → A.

6. What this means for the RFC

Filling both holes makes the all fibre the full 3 × 2 product: distributive, closed under meet and join, N₅ gone, and composition never escapes the region — §4.2 dissolves. You need both, since B ∧ D needs the bottom-right cell and C ∨ D needs the top-left one.

So the conjecture in the companion (that composites inhabit a larger region than atoms) is right but understated. The composite region is the product completion of the atomic region, and the atomic region is that product minus two contingently-empty cells.

Two edits I would make to RFC-2 on the strength of this:

• §3.4 should say the obstruction is contingent and name what removes it, rather than presenting non-modularity as a property of the domain.
• The boundary modality should be demoted. □_b is order-preserving, idempotent and deflationary — an interior operator, i.e. a comonad on the lattice. Interior operators canonically preserve meets and fail to preserve joins. So the conjecture that it does not distribute over join is probably true but is not a second obstruction; it is the expected behaviour of a modality, and I was treating normal structure as pathology.

None of this changes the presentation proposal. It does change the argument for R2-2 and for reconstruction generally: extending reconstruction is not only a trust improvement per clause, it is what makes the assurance order well-behaved enough to compose at all.

[maxinelevesque]

Companion: the metatheory of the assurance order

The deliverable RFC-2 §4 promises, following the pattern RFC-1 used for the stage-2 metatheory sketch. It formalises what the earlier comment on this issue argued informally, and adds the proofs, the labelling discipline, and two obligations that comment did not state.

Everything below is labelled established, conjectured, or open, and nothing advances a label without a proof or a counterexample.

---

RFC-2 companion: the metatheory of the assurance order

Status	Metatheory sketch — companion to RFC-2 §3–§4
Deliverable	The coherent region, the order on it, the obstruction to composition, and the proof that the operator and forge check coincide
Discipline	Same as the Lean spine: every claim labelled established, conjectured, or open. No claim advances a label without a proof or a counterexample.
Baseline	dollspace-gay/Thermite @ 84d276e7

---

0. What is established, conjectured, and open

The honesty declaration, first, because the rest is easier to read against it.

Established (proved below, from definitions RFC-2 §1 already fixes):

• E1 — Refutation is functionally determined by scope outside all, so the position space is a fibration over the scope chain rather than a product (§2.1).
• E2 — The atomic coherent region has exactly eight cells, seven order-elements (§2.3).
• E3 — Ordered by residual inclusion, trust is a two-element chain (§3.1).
• E4 — The seven elements form a bounded lattice (§3.3).
• E5 — It contains N₅ as a sublattice, hence is non-modular and non-distributive (§3.4).
• E6 — The all fibre is not closed under meet. B ∧ D and C ∧ D have no lower bound inside the fibre; the lattice closes only because K, from the bounded fibre, supplies one. The meet of two all-inputs positions escapes to a weaker scope (§4.2). This is the central result.
• E7 — Per-axis composition leaves the coherent region, and the lattice meet stays inside it but under-claims scope. The two candidate operators fail in opposite directions (§4.3).
• E8 — The non-modularity is contingent, not intrinsic. The all fibre is a 3×2 refutation-by-trust grid with exactly two cells empty, forbidden by K2 and K3. Filling both makes the fibre a product of chains — distributive, and closed under meet and join (§4.5).

Conjectured (argued, not proved):

• C1 — The composite region is the product completion of the atomic region, and K1–K3 are constraints on routes, not on claims (§4.4).
• C2 — The boundary modality does not preserve joins (§5). Note this is expected structure, not an obstruction: □_b is an interior operator, and interior operators canonically preserve meets and fail joins.

Open (no position taken):

• O1 — Whether the eight-cell inventory is complete with respect to the implementation — i.e. whether forge check can emit a position outside it (§2.4).
• O2 — The composite region's characterization (§4.4).
• O3 — Whether the forge ∥ solver edge should be oriented at all (§7 argues it should not be, globally).

1. Objects

A position is a quadruple

p = (s, r, τ, b)

with s ∈ Scope, r ∈ Refutation, τ ⊆ Residual, b ∈ Boundary, drawn from RFC-2 §1. Trust is represented by its residual — the set of things you must believe that the route did not discharge:

position	residual τ
lean-checked	{inspection, rustc}
solver, solver + lean-lemma	{solver, inspection, rustc}
fiat	{fiat, rustc}

A discharged obligation — a kernel-proved bridge lemma — is absent from the residual rather than present in a union. This is the representational choice that makes §3.1 come out right.

Boundary is carried separately throughout §§2–4 and treated in §5.

2. Coherence

2.1 Scope determines refutation outside all — established

scope	admissible refutation	argument
none	none	nothing is claimed, so there is no false clause to witness
per-exec	abort	a runtime check observes only the execution it runs in
bounded(n)	trace(n)	the procedure is complete relative to the bound, and its witness is a trace within it
all	complete · incomplete · empirical	free

Consequence. Refutation is not an independent coordinate. It is a fibration over scope, and the only fibre with internal structure is all. Every question in this document lives in that fibre.

2.2 The remaining constraints

• K1 fiat ∈ τ ⟹ s ∈ {none, per-exec}. Claiming all inputs by declaration is exactly #[slag], which is s = none.
• K2 r = incomplete ⟹ solver ∈ τ. If Lean re-checked the theorem the route was decidable, hence complete.
• K3 r = empirical ⟹ solver ∉ τ. Empirical refutation is the covenant, a forge construct, and the forge's discharge is kernel-checked.

2.3 Eight cells, seven elements — established

S  none      / none      / {fiat, rustc}                 slag
R  per-exec  / abort     / {fiat, rustc}                 runtime
K  bounded(n)/ trace(n)  / {solver, inspection, rustc}   Kani
A  all       / complete  / {inspection, rustc}           reconstructed cage
B  all       / complete  / {solver, inspection, rustc}   cage, unreconstructed
B′ all       / complete  / {solver, inspection, rustc}   relax route
C  all       / incomplete/ {solver, inspection, rustc}   general Verus
D  all       / empirical / {inspection, rustc}           the forge

B and B′ have identical coordinates and are therefore the same element, reached by different routes. Eight cells, seven elements.

This is where ℝ-relaxation's status falls out rather than being asserted: it is a coverage result, not an assurance-rank result, exactly as RFC-1 §12 described it. The bridge lemma buys admission to B, not promotion above it.

2.4 The completeness obligation — open (O1)

§2.3 enumerates what the rules permit. It does not establish that forge check cannot emit something else. That is a soundness statement about the implementation:

Obligation. For every program P and clause c, the position forge check
assigns to c lies in the eight-cell region.

Discharging it is mechanical and is the natural first increment: RFC-2's R2-4 already proposes rejecting certificates in incoherent cells, which converts this obligation into a runtime assertion and makes any counterexample self-reporting.

3. The order

3.1 Trust is a two-element chain — established

Order residuals by inclusion, smaller being better. Then

{inspection, rustc} ⊂ {solver, inspection, rustc}

so lean-checked < solver strictly, and solver ≡ solver + lean-lemma since the lemma is discharged and therefore absent from both residuals. No further structure is needed, and none is available: the residual sets in play form a chain, not an antichain. ∎

3.2 The order on positions

Componentwise: scope by the chain all > bounded(n) > per-exec > none; refutation within a fibre by complete > incomplete > empirical; trust by §3.1. Across fibres, scope decides — which is well-defined precisely because of E1.

3.3 It is a bounded lattice — established

                 A
                / \
               B   \
               |    D
               C   /
                \ /
                 K
                 |
                 R
                 |
                 S

Only two pairs are incomparable, {B, D} and {C, D}, and each has a unique least upper and greatest lower bound:

pair	join	meet
B ∨ D	A	K
C ∨ D	A	K

Proof. Upper bounds of {B, D}: A alone, since B ≰ D and the only element above D other than A is none. Lower bounds: {K, R, S}, whose greatest is K. Identically for {C, D}. Every other pair is comparable, so its meet and join are its endpoints. A is the maximum and S the minimum, so the lattice is bounded. ∎

The meets are worth reading rather than skipping: the greatest common assurance of the forge and any solver route is Kani.

3.4 The obstruction is N₅ — established

Take {K, C, B, D, A} with the embedding 0 ↦ K, a ↦ C, b ↦ B, 1 ↦ A, c ↦ D. Then K < C < B < A, K < D < A, and D is incomparable to both C and B. That is N₅.

It is a genuine sublattice: C ∨ D = B ∨ D = A and C ∧ D = B ∧ D = K, all inside the set, and the remaining pairs are comparable. ∎

N₅ is the forbidden sublattice for modularity, so the assurance order is non-modular; and since distributivity implies modularity, non-distributive.

What that buys. Non-distributivity is the formal content of "the axes interact." It is not a stylistic observation — it says no presentation of these positions as independent per-axis scores can recover the order, and therefore that per-axis reasoning about composition must fail somewhere. §4 finds where.

4. Composition

4.1 The naive operator

For clauses composing into an item, the obvious rule is per-axis:

(s₁,r₁,τ₁) ⊓ₐ (s₂,r₂,τ₂)  =  (min s, min r, τ₁ ∪ τ₂)

Scope and refutation take the weaker; residual risk unions, since you must believe everything either clause needed.

4.2 The all fibre is not closed under meet — established (E6)

Take {B, D} — cage-solver and the forge. Lower bounds within the fibre: C ≤ B, but C ∥ D, and no other all position lies below both. There is no meet in the fibre. Identically for {C, D}.

The seven-element structure is a lattice only because K — from the bounded fibre — supplies the missing bound. So:

The meet of two all-inputs positions escapes its own fibre and lands in a
weaker scope. ∎

That is the composition problem stated structurally, and it is a better statement than "the natural rule produces something incoherent": the issue is not the arithmetic, it is that the region composition has to close over is the wrong shape.

4.3 Both candidate operators fail, in opposite directions — established (E7)

Per-axis ⊓ₐ on C and D:

C ⊓ₐ D  =  (all, min(incomplete, empirical), {solver,insp,rustc} ∪ {insp,rustc})
        =  (all, empirical, {solver, inspection, rustc})

which violates K3 (r = empirical ⟹ solver ∉ τ) and is not one of the eight cells. It leaves the region.

Lattice meet C ∧ D = K is coherent, but K has scope bounded(n) while both clauses hold for all inputs — so the item does too. It leaves the truth, on the one axis where the truth is not in doubt. Coarsening does not rescue it: the greatest coherent position below C ⊓ₐ D is again K, since C and D each beat it on one coordinate and so neither lies below.

4.4 The resolution — conjectured (C1)

The paradox dissolves if K3 is read correctly. K3 was derived from how single routes work: empirical refutation comes from the covenant, whose discharge is kernel-checked. That is a fact about routes, not about claims.

A composite can have worst-case-empirical refutation and require solver trust, because different clauses contribute different coordinates. Nothing incoherent is asserted; the position simply cannot be produced by any one mechanism.

Conjecture C1. K1–K3 constrain routes. The composite region is the
product completion of the atomic region, and (all, empirical, {solver,…})
is a legitimate member of it.

If C1 holds, E6 stops being an obstruction and becomes a type distinction: atoms and composites inhabit different regions, and conflating them is what made composition look impossible.

Until then, RFC-2's conservative reporting is right and now has a reason rather than a shrug: an item's assurance is the antichain of its clause positions plus the weakest link per axis, with no single composite computed. Sound under either resolution, and strictly more informative than any point.

4.5 The obstruction is contingent — established (E8)

Lay the all fibre out as refutation (3-chain) against trust (2-chain):

	lean-checked	solver
complete	A	B
incomplete	empty — K2	C
empirical	D	empty — K3

Four of six cells occupied. If the grid were full the fibre would be 3-chain × 2-chain — a product of chains, hence distributive, closed under meet and join, and N₅ would not exist. The pentagon is the shape of the two holes: D reaches the top in one step where C needs two.

And note where §4.3's counterexample landed: (all, empirical, solver) is the bottom-right hole. The per-axis operator was computing the correct product meet all along; K3 was reporting that the answer did not exist.

Neither hole is a theorem.

• (empirical, solver) is arguably already occupied and mislabelled: a Verus clause outside the admitted fragment is proved-or-shrug, and incomplete conflates "sometimes produces a witness" with "structurally cannot for this shape." Filling it properly means extending the covenant to out-of-cage Verus clauses — and generalizing covenant-before-burn to covenant-before-discharge, since a falsifier hit means the solver was never needed.
• (incomplete, lean-checked) is reconstruction past the decidable fragment. Nothing about kernel-checking requires decidability; K2 is a fact about how reconstruction was built.

Both are needed: B ∧ D wants the bottom-right cell, C ∨ D the top-left. Fill both and composition never escapes.

This reframes reconstruction from a per-clause trust improvement into a structural repair of the assurance order.

5. The boundary modality is a comonad — conjectured (C2)

Boundary was carried separately above because it does not behave like a coordinate.

A clause at complete @ to_boundary is completely refutable modulo the assumption: a counterexample to the whole-program property may live inside the foreign body, where no channel observes it. So boundary acts on refutation rather than beside it — write □_b p for position p closed only to boundary set b.

□_b is order-preserving, idempotent (closing to a boundary twice is closing once), and deflationary (□_b p ≤ p). That makes it an interior operator — a comonad on the lattice.

Conjecture C2. □_b preserves meets and does not preserve joins.

The intuition for the join failure is that a boundary crossing reachable from p ∨ q need not be reachable from either alone, since the join can introduce a call path neither clause had.

This is expected structure, not a second obstruction. Interior operators canonically preserve meets and fail joins; a modality that distributed over both would be the surprise. An earlier draft of this document treated the join failure as a second defect independent of N₅, which was a misreading of ordinary modal behaviour as pathology.

The practical consequence is narrower than that framing suggested: the composite region of §4.4 must be characterized per-boundary, because joins do not commute with closure. That is a scoping requirement on O2, not an additional obstruction.

6. The agreement obligation

None of the above is worth anything if it merely coexists with the implementation. The discipline is the one classifier_correct already establishes for the S₂.0 classifier:

Obligation. The position this metatheory assigns to a clause equals the
position forge check computes for it, for every program in the conformance
corpus, and the classifier and the proven fragment coincide.

Concretely, three checkable statements:

1. Inventory soundness (O1) — every emitted position is in the region.
2. Order agreement — the comparison make audit performs is the order of §3.
3. Composition agreement — whatever forge reports for an item is what the operator of §4.4 yields, once that operator exists.

Statement 1 is available immediately via RFC-2 R2-4. Statement 2 follows R2-6. Statement 3 is gated on O2.

7. Should the forge ∥ solver edge be oriented? — open (O3), with a recommendation

RFC-1 oriented it by fiat: "A good trade, probably — and 'probably' is why L3 ranks below the rung whose refutations are mechanically complete."

Recommendation: leave it incomparable, permanently.

Orienting it requires answering "which do you fear more — solver unsoundness, or an unfalsifiable false claim?" That is not a logical question. It is a threat model, and it differs by deployment: a kernel shipping into an adversarial environment and a library proving a data-structure invariant have different answers, and both are right.

RFC-2 §3.4 already supplies the mechanism that makes a global answer unnecessary: acceptance gates compare against a declared set of floor tuples. A deployment that considers the forge acceptable declares D in its floor set; one that does not, does not. The edge stays unoriented in the metatheory and gets oriented locally, in a reviewable artifact, by whoever carries the risk.

This is the one place where the honest answer to a metatheory question is a policy mechanism rather than a theorem, and it is worth saying so plainly instead of manufacturing an order.

8. Summary

Position space	a fibration over the scope chain, not a product — established
Coherent atomic positions	8 cells, 7 elements — established
The order	bounded lattice, unique top A, bottom S — established
Obstruction	N₅; non-modular, non-distributive — established
The all fibre	not closed under meet; meets escape to a weaker scope — established, and the central result
Both candidate operators	per-axis leaves the region, lattice meet leaves the truth — established
The obstruction's status	contingent — two empty grid cells, neither a theorem — established
Proposed resolution	the composite region is the product completion — conjectured
Boundary modality	an interior operator; join-failure is expected, not an obstruction — conjectured
forge ∥ solver	leave unoriented; declare floor sets per deployment

Two things here are worth more than the rest.

E6 converts "we have not specified aggregation" from an admission into a result: the natural rule is provably wrong, and the reason is structural. RFC-2 defers composition because composition is genuinely hard, not because the drafting ran out of time.

E8 says the difficulty is not permanent. The pentagon exists because two cells of a 3×2 grid are empty, and neither is empty by theorem — one is arguably already occupied and mislabelled, the other is reconstruction past the decidable fragment. Fill both and the fibre becomes a product of chains, closed under meet and join, with composition never escaping.

That is the argument this document most wants read: extending reconstruction is not only a per-clause trust improvement — it is what makes the assurance order well-behaved enough to compose at all.