SF-TR-2026-011Proof-Gated Execution

A Reduction-to-Practice Framework for Mathematical Invariants in Self-Describing Computing Systems

SF-TR-2026-011 · Technical Report · first published 2026-05-19 · revised 2026-08-31 (r2)

Introduction to the revised edition

Added 2026-08-31. The paper below is r1, published 2026-05-19, with r2 corrections marked in place. Nothing has been silently removed; §9 records every change and why.

What this is

Proof-Gated Function is a method, not a test harness and not a library. Its statement is one sentence: a value may propagate only if a predicate anchored outside its producer says it satisfies the mathematical contract its producer claims to satisfy. Everything else in this paper — the trait, the wrapper, the witness, the ledger — is one embodiment of that sentence in Rust, and the method survives the embodiment being replaced.

The distinction matters because the method generalises past the setting it was developed in. Nothing in it depends on Rust, on the WISP pipeline, on biometrics, or on this particular hash function. What it depends on is that the predicate be a property of the operation rather than a re-derivation of it — a cosine lies in [-1, 1] whatever computed it — and that the predicate be authored somewhere other than the thing it judges. Those two constraints are the method. The rest is engineering.

Why it was built

It was not built to test the pipeline. It was built to answer a harder question: is the core architecture doing what the architecture says it does?

That question cannot be answered by a passing test suite, because a test suite is written by the same hand as the code and encodes the same misunderstanding. It cannot be answered by review, because the surface signals — it compiles, the tests pass, the prose is fluent — all match whether or not the answer is yes. What it needs is a check anchored outside both the implementation and its author.

Running the WISP claim-1 pipeline under proof gating produced that check. Twelve witnesses came out of one end-to-end run: the temporal encoding stayed on the unit circle at every observation, the composite's identifier was the content address of its own bytes, the coherence between consecutive composites was a real cosine in range, and the decay factor was a real decay. Each of those is a load-bearing claim the architecture makes about itself, and each was mechanically witnessed rather than asserted.

That corpus is the first witness that the core architecture works as intended. Not that the code is correct — no runtime witness establishes that — but that the specific mathematical claims the architecture rests on held, on real input, in a form a third party can reproduce and check without trusting either the author or the code. Before this run, those claims were documented. After it, they were evidenced.

The method was the by-product. It was developed in the course of asking the question, and it turned out to be the more portable of the two results.

The pairing with the Cell Protocol

Proof-Gated Execution (SF-TR-2026-011, 2026-05-19) and the Bench Cell Protocol (SF-SPEC-2026-003, 2026-05-21) were built two days apart. That is not a coincidence of scheduling. They are the same idea at two scales, and they were developed together because either one alone is insufficient.

The shape is identical in both: the gate precedes the thing it authorises, and the authorising artifact is anchored outside what it authorises. A predicate written after seeing the output would be fitted to it; a hypothesis registered after seeing the result would be a story. Both protocols exist to make that ordering structural rather than a matter of discipline.

They are also complementary in what they catch. Proof gating catches a wrong implementation from the inside — it does not care who wrote the code or how confidently. The Cell Protocol catches a wrong interpretation from the outside — it does not care how good the numbers look if nobody else can reproduce them, and a single refutation blocks admission however many peers agreed.

Together they are an attempt to falsify our own work before anyone else has to. The Foundation's stated posture is that a shape becomes structure only through testing and refutation by people other than its author. These two protocols are that posture made mechanical: one asks the mathematics to refute the implementation, the other asks other people to refute the result. Both were written by the party they are pointed at, which is the only honest reason to write them.

What r2 changes

The reference implementation of SF-WISP-STD-001 was written between May and August 2026 and applied this method from the first line rather than retrofitting it. That exercise falsified several claims in r1. They are corrected in place and enumerated in §9.

The corrections fall into three groups, and the third is the interesting one:

1. Two signature identifiers in §3.3 were wrong — they named the right mathematics under the wrong registry entries, which is a provenance error rather than a technical one.
2. Three empirical figures in §3.4 and §5 do not measure what they are described as measuring. The defect is in the claim-test suite, not in the framework.
3. One structural defect makes the audit ledger's central promise unkeepable as r1 implemented it, and fixing it required a change to the method's statement, not just to the code. See §9.3. This is the correction worth reading.

None of the three was found by review. All three were found by an implementation that had to make a decision the paper left open — which is the same argument the paper makes about tests, applied to the paper.

Abstract

We describe a framework in which every function call in a computing system is gated by a runtime geometric proof — a small mathematical predicate that witnesses the function's output satisfies its declared mathematical invariant. The witness is the only authorization for the output to propagate downstream; failed proofs halt execution and themselves become entries in an append-only audit trail. The framework generalizes the cryptographic five-step verification pattern of m_aegis from a single chain to every mathematical primitive in the system.

We apply the framework to the WISP semantic-identity authentication pipeline disclosed by U.S. Patent Application 19/308,229 (Notice of Allowance 2026-04-27) and produce a complete reduction-to-practice corpus: 974 captured biometric observations processed through the patent's claim-1 pipeline, each mathematical step witnessed by a content-addressed JSONL record. Twenty independent claim-property tests pass, four proof-rejection tests pass, and twelve witnesses populate the audit ledger from one end-to-end run.

The contribution is methodological: bounded falsifiability per function as the corrective discipline for systems where confident-sounding code — LLM-authored or otherwise — can pass review without ever being mechanically checked against the invariants it claims to satisfy.

1Introduction

1.1 The audit gap

Software review traditionally relies on three signals: that the code compiles, that tests pass, and that a human reviewer reads it and finds nothing egregious. These signals work well when the code's author can explain to the reviewer what invariants the code preserves. They work poorly when the author cannot, or when the reviewer has no mechanical means to check the explanation.

LLM-authored code amplifies this gap. A modern language model can produce fluent Rust, fluent CSS, fluent SQL, and fluent justifications for any of them. The output compiles. The tests pass — when there are tests. The reviewer reads paragraphs of confident prose about what the code does. None of this is a check against what the code should do. The model is optimized to sound rigorous, and sounding rigorous is not the same as being rigorous.

The corrective is not less abstraction. Abstractions remain necessary; the problem is not their existence but their unboundedness — abstractions without a paired falsifier. An abstraction with no test that could falsify it is taste pretending to be structure. The discipline this paper proposes is bounded falsifiability per function: every load-bearing function carries a mathematical predicate that, when evaluated against the function's actual input and output, either passes or produces a structured violation. The predicate is the proof the function emits with its output; without the proof, the output is not authorized to propagate.

1.2 The geometric framing

We call these geometric proofs because the predicates are drawn from a formal mathematical signature registry: cosine similarity bounded in [-1, 1], exponential decay bounded in (0, 1], Pythagorean identity \sin^2\theta + \cos^2\theta = 1 on cyclical pairs, BLAKE3 of canonical bytes producing a deterministic 16-byte anchor, scalar quantization preserving direction above a configured cosine floor. Each predicate has a SIG identifier — a stable name in the registry — and explicit bounds. The predicate is computed deterministically from the function's input and output. Computation produces either a witness (predicate value within bounds) or a violation (out of bounds, non-finite, or otherwise undefined).

The framing is intentional. Geometric signals that the predicates are real mathematical statements with shape and range, not merely flags or booleans. Proof signals that the witness has evidentiary force — a third party with the same input and output reproduces the witness byte-for-byte and verifies the predicate independently. Gated execution signals the structural commitment: without the proof, nothing proceeds.

1.3 What this paper contributes

Three claims:

1. A trait-level framework for proof-as-witness-as-authorization, implemented in ~300 lines of Rust at wisp-proof/src/lib.rs. The trait GeometricProof declares the inputs, outputs, bounds, and predicate of one SIG. The wrapper proven(&proof, input, f) is the only execution path through which a function call produces output that downstream code is permitted to use.

1. Seven concrete proofs drawn from the math signatures of the WISP pipeline: cosine, decay, temporal-unit-circle, provenance anchor, quantization coherence, entropy spread, and drift bound. Each lifts a mathematical invariant from an inline test assertion into a formal GeometricProof implementation, with deterministic content-addressing of input, output, and predicate value.

1. A complete worked example applying the framework to a real patent application. The WISP pipeline (BDY001) is exercised end-to-end against 974 captured biometric observations; twelve witnesses are produced from one run and appended to a JSONL audit ledger; three failure modes (out-of-bound, non-finite, drift-archive) are independently demonstrated. The full deploy lives at /Users/arc/Git/WISP Deploy/, builds in under fifteen seconds, runs the full test suite in under twenty milliseconds, and produces deterministic results across hosts.

2The framework

2.1 SIG, predicate, bounds

A signature is a stable identifier for a mathematical primitive. The 250-SIG formal registry used by the surrounding system contains entries like:

• SIG-V03 — cosine similarity between two vectors.
• SIG-T06 — half-life exponential temporal decay V(t) = e^{-\lambda \Delta t}.
• SIG-T05 — multi-scale sinusoidal temporal embedding with three cyclical pairs at daily, weekly, yearly periods plus a monotonic epoch component.
• SIG-C01 — provenance anchor as the truncated BLAKE3 hash of canonical bytes.
• SIG-S13 — scalar i8 quantization with bounded directional loss.

Every SIG names an invariant. The invariant is not a soft preference; it is a mathematical statement about the function's contract. Cosine takes vectors and returns a scalar in [-1, 1] — that bound is structural to the operation, not a runtime assumption. Exponential decay with \lambda \geq 0 and \Delta t \geq 0 always lies in (0, 1]. These are properties the implementation either satisfies or fails to satisfy; there is no third option.

A geometric proof for a SIG specifies:

• The input type the function consumes.
• The output type the function produces.
• The lower and upper bounds of the predicate.
• A deterministic predicate function \pi(\text{input}, \text{output}) \rightarrow \mathbb{R} whose value must lie within the bounds.
• A canonicalization rule mapping input to a 16-byte BLAKE3 content hash.
• A canonicalization rule mapping output to a 16-byte BLAKE3 content hash.

The predicate is not the function's behavior; it is the witness of the function's behavior. For cosine, the predicate is the cosine value itself — if it sits in [-1, 1], the function executed correctly. For provenance anchor, the predicate is the number of byte positions where the claimed anchor diverges from the BLAKE3 of the input — if zero, the function executed correctly. For exponential decay, the predicate is the decay factor — if positive and ≤1, the function executed correctly.

2.2 The trait

In Rust the framework reduces to a single trait:

pub trait GeometricProof {
    type Input;
    type Output;

    fn sig(&self) -> SigId;
    fn bounds(&self) -> (f64, f64);
    fn predicate(&self, input: &Self::Input, output: &Self::Output) -> f64;
    fn hash_input(&self, input: &Self::Input) -> [u8; 16];
    fn hash_output(&self, output: &Self::Output) -> [u8; 16];

    fn prove(&self, input: &Self::Input, output: &Self::Output)
        -> Result<ProofWitness, ProofViolation>;
}

The trait's default prove implementation evaluates the predicate against the bounds and returns a ProofWitness on pass or a ProofViolation on fail. The witness carries: the SIG, the two content hashes, the predicate value, the bounds, and a wall-clock timestamp. The violation carries the same fields plus a textual reason. Both are serializable; both can be appended to an audit ledger; both are content-addressed via BLAKE3.

A concrete implementation — SIG-V03 cosine — is about thirty lines:

pub struct CosineSimilarityProof;

impl GeometricProof for CosineSimilarityProof {
    type Input  = (Vec<f32>, Vec<f32>);
    type Output = f32;

    fn sig(&self)    -> SigId    { SigId::new("SIG-V03") }
    fn bounds(&self) -> (f64,f64) { (-1.0 - 1e-6, 1.0 + 1e-6) }
    fn predicate(&self, _: &Self::Input, output: &f32) -> f64 { *output as f64 }
    fn hash_input(&self, input: &Self::Input)  -> [u8; 16] { blake3_first_16(&serialize(input))  }
    fn hash_output(&self, output: &Self::Output) -> [u8; 16] { blake3_first_16(&serialize(output)) }
}

The bounds permit a small numerical slack outside the strict mathematical range to absorb floating-point rounding. The predicate is the cosine itself. The hashes canonicalize the input pair and the output scalar so that two independent verifiers given the same vectors arrive at the same witness identity.

2.3 The execution wrapper

Proof-gated execution is a single function:

pub fn proven<P, F>(
    proof: &P,
    input: P::Input,
    f: F,
) -> Result<(P::Output, ProofWitness), ProofViolation>
where
    P: GeometricProof,
    F: FnOnce(&P::Input) -> P::Output,
{
    let output = f(&input);
    let witness = proof.prove(&input, &output)?;
    Ok((output, witness))
}

The function takes the proof, the input, and the function to execute. It runs the function, evaluates the proof, and returns either the (output, witness) pair or a ProofViolation. The witness is structurally the only authorization for the caller to use the output: at the type level, (P::Output, ProofWitness) is the only thing proven returns on the success path, and ProofViolation propagates as the error.

This is the structural form of proof as enablement of execution. Nothing prevents a programmer from calling the raw function directly — Rust's visibility system can be used to forbid that, by making the underlying implementation crate-private and exposing only the proven variant — but even in the permissive form, every call site that goes through proven participates in the audit trail. Migration is incremental: wrap the calls you care about, leave the rest unwrapped, expand coverage over time.

2.4 The audit ledger

Witnesses and violations are appendable to a JSONL audit ledger:

{
  "sig": "SIG-V03",
  "input_hash":  [b0..b15],
  "output_hash": [b0..b15],
  "predicate_value": 0.9999,
  "bound_low": -1.000001,
  "bound_high": 1.000001,
  "timestamp_ms": 1779179742075
}

Each line is one witness or violation. The file is append-only; replaying it reconstructs the corpus of "what ran, with what input hash, with what output hash, with what predicate value." Two independent verifiers, presented with the same source code and the same input data, produce identical ledgers byte-for-byte (modulo timestamps).

r2 — the promise does not survive its own parenthesis. "Modulo timestamps" is where it leaks. timestamp_ms is inside the witness, so it is inside the witness's content address, so two runs of identical inputs produce different witnesses and the ledger has no stable identity. A root that changes on every run cannot be cited as evidence of anything. The correction is a change to the method, not to the code: the clock is an argument, never a read. A flat JSONL file is also weaker than this section claims — it commits to the corpus but yields no way to disclose one witness without disclosing all of them. See §9.3. The audit corpus is the reduction-to-practice artifact: not "this code looks right" but "this code ran on this input, produced this output, and the output satisfied this invariant."

3Worked example — WISP

3.1 The pipeline

The WISP semantic-identity authentication pipeline disclosed by BDY001 (U.S. 19/308,229) is a ten-step method:

1. Receive multimodal user input (textual/voice/temporal/role).
2. Embed each modality into its corresponding vector (narrative, temporal, role).
3. Fuse the vectors into a composite semantic authentication object.
4. Store the composite in a persistent semantic memory graph.
5. On subsequent input, regenerate a composite.
6. Compute semantic coherence via vector similarity (cosine).
7. Apply exponential time-based decay to produce a trust coefficient.
8. Compare trust coefficient against an authentication threshold.
9. If passing, emit an authentication packet to an external system.
10. If failing, deny and exclude from persistent storage.

Each step has at least one mathematical primitive backing it. Each primitive has a SIG. Each SIG has, under this framework, a geometric proof.

3.2 The captured corpus

The empirical input is 974 biometric observations captured by a prior m_logos deployment, stored as JSONL at data/logos-manifold.jsonl. Each observation contains a six-dimensional normalized geometry vector (post-Welford), an eight-dimensional Kronos temporal embedding, a wall-clock timestamp, a channel identifier when applicable, a modality tag (acoustic, kinetic, or system), and raw samples for the acoustic channel. The distribution is 890 acoustic, 84 kinetic, and a residual 5 system entries. The observations span several hours of authentic user activity, captured by the original Logos manifold deployment before the framework described here existed.

3.3 Seven proofs

Seven SIGs are implemented. Each is approximately thirty lines of Rust locked to a single mathematical invariant.

SIG-V03 · CosineSimilarityProof — (Vec<f32>, Vec<f32>) → f32. Bounds [-1, 1] plus numerical slack. Predicate is the cosine output itself. Hashes canonicalize the two vectors. Used by the coherence comparison between consecutive composites (claim 1.vi) and by role-vector alignment (claim 4).

SIG-T06 · ExponentialDecayProof — (f64, f64) → f64. Input is (\lambda, \Delta t). Bounds (0, 1]. Predicate is the decay factor. Used by the trust-coefficient computation (claim 1.vii).

SIG-T05 · TemporalUnitCircleProof — [f32; 8] → f64. Input is the 8-D Kronos embedding. Predicate is the worst-case deviation |\sin^2\theta + \cos^2\theta - 1| across the three cyclical pairs (daily, weekly, yearly). Bounds [0, 0.5] — real captures show some drift from the strict unit circle but stay well-bounded. Used to witness that every temporal vector remains on the unit circle within tolerance (claim 1.ii.ii).

SIG-C01 · ProvenanceAnchorProof — Vec<u8> → [u8; 16]. Input is the canonical bytes to be anchored. Output is the claimed 16-byte BLAKE3 anchor. Predicate is the count of byte positions where the claimed anchor disagrees with the recomputed BLAKE3 of the input. Bounds [0, 0] — any mismatch is a violation. Used to witness the composite's content-addressed identifier (claim 1.iii).

SIG-S13 · QuantizationCoherenceProof — (Vec<f32>, Vec<f32>) → f64. Input is the (original, reconstructed) pair. Output is the cosine between them. Bounds [0.9, 1] — the empirical floor for the captured geometry's 17-decade dynamic range under scalar i8 quantization. Used to witness that storage compression preserves direction (claims 1.iv, 6).

SIG-S19 · EntropySpreadProof — Vec<f32> → f64. Input is the population of pairwise cosines from a sample window. Predicate is the standard deviation. Bounds [0, 2]. Used to witness narrative coherence detection (claim 5).

r2 — wrong identifier. SIG-S19 in the registry is Welford Online Statistics, not an entropy spread. The mathematics described here is right; the name is not. See §9.1.

SIG-S29 · DriftBoundedProof — (Vec<f32>, Vec<f32>) → f64. Input is two geometry vectors. Output is the L2 distance. Bounds [0, \text{max\_drift}] — the configured archive threshold. Used to witness drift management; a violation indicates an archive candidate (claims 9, 19).

r2 — wrong identifier. SIG-S29 in the registry is Sliding-Window Event Rate. The operation described is an L2 distance, whose registry entry is SIG-V06 — L2 Distance. The ceiling is not part of the signature: a threshold is a deployment's policy, and binding one into a signature makes every deployment that tunes it non-conforming. See §9.1.

3.4 The proven pipeline

The claim-1 pipeline runs as follows. Italicized lines are the witnesses that materialize in the audit ledger; the eight-line block is run eight times, once per temporal observation in the window.

load 974 observations from logos-manifold.jsonl
take the first 8 events → multimodal input

for each event:
    proven(&TemporalUnitCircleProof, event.time.vector, worst_pair_deviation)
        → witness SIG-T05

fuse_geometry(events) → composite_geometry, mean_cosine, mean_L2

canonical_bytes = composite_geometry serialized
proven(&ProvenanceAnchorProof, canonical_bytes, |b| BLAKE3(b)[..16])
    → witness SIG-C01

q = quantize_f32_to_i8(composite_geometry)
recon = dequantize_i8_to_f32(q)
proven(&QuantizationCoherenceProof(0.9), (composite_geometry, recon), |o,r| cos(o,r))
    → witness SIG-S13

take the next 8 events
fuse → second_composite

proven(&CosineSimilarityProof, (composite_geometry, second_composite), compare_manifold)
    → witness SIG-V03

dt = |t2 - t1|;  λ = ln(2) / (7·86400)
proven(&ExponentialDecayProof, (λ, dt), |(l,d)| exp(-l·d))
    → witness SIG-T06

trust = coherence · decay
if trust ≥ threshold:
    packet_id = BLAKE3(composite_1 ‖ composite_2)[..32]
    emit authentication packet
else:
    deny + exclude

One run on the captured corpus produces:

• 8 SIG-T05 witnesses — temporal vectors on the unit circle (max deviation 5.96 \times 10^{-8} across all eight).
• 1 SIG-C01 witness — provenance anchor for the fused composite.
• 1 SIG-S13 witness — quantization preserves cosine at 0.9143.
• 1 SIG-V03 witness — coherence between consecutive composites at 0.9999.

r2 — two of these figures do not measure what they say. 0.9143 compares a vector against its own clipped sign pattern rather than against a dequantized reconstruction. The 1.0000 reported as mean_cosine elsewhere in the suite is the acoustic fusion weight, which can only take the values 0.0, 0.5 or 1.0 — the result of binding a five-tuple positionally under the wrong names. See §9.2.

• 1 SIG-T06 witness — decay factor 1.0000 over a 40-second window.
• 1 authentication packet ID: f3447d87ba5e5df07a9eb0994e46551dabe72e86c80bd1358c05192fa4131744.

The packet ID is deterministic. Re-running the test on a different host produces the same hex string. The witnesses' hashes are deterministic; their timestamps are not, but the structure is.

The audit ledger after one run is twelve lines, each a valid JSON witness. The total runtime, including the cargo test overhead, is under twenty milliseconds.

4Failure modes

A framework that always passes is no framework. Three failure modes demonstrate that the proofs actually reject when their invariant is violated.

4.1 Out-of-bound output

A simulated buggy or adversarial cosine function returns 1.5. The proof rejects:

sig:    SIG-V03
value:  1.5
bounds: [-1.000001, 1.000001]
reason: predicate value 1.5 outside SIG bounds [-1.000001, 1.000001]

The wrapper returns Err(ProofViolation); the output never leaves the function call. Downstream code never sees the value 1.5.

4.2 Non-finite output

A function returns f32::NAN. The proof rejects:

sig:    SIG-V03
reason: predicate value is not finite

The framework treats NaN, +\infty, and -\infty as immediate violations regardless of bounds. This catches numerical pathologies — division by zero in cosine when one vector has zero magnitude, e.g. — before they propagate.

4.3 Drift threshold exceeded → archive candidate

Two geometries are tested against a DriftBoundedProof with max_drift = 2.0. A nearby pair (drift 0.11) passes; a far pair (drift 244.54) is rejected:

sig:        SIG-S29
value:      244.54
bound_high: 2.0

The rejection is the patent's claim-9 archive signal: a composite whose drift exceeds the maintenance threshold is an archive candidate rather than a continued participant in the active manifold. The framework treats "archive" not as a separate code path but as the natural meaning of a proof violation: the output is real, it satisfies the function's purely computational contract, but it does not satisfy the invariant declared for downstream propagation. The audit ledger records the violation; the runtime declines to forward the output.

5Empirical results

The full deploy at /Users/arc/Git/WISP Deploy/ contains:

• 12 dependency crates, ~13,845 lines of Rust.
• 1 captured-telemetry fixture, 974 observations, 562 KB.
• 1 new framework crate (wisp-proof), ~600 LOC.
• 2 test files (bdy001_patent.rs, bdy001_proven.rs), collectively 24 tests.

Test results:

Build: 14 seconds clean, 0.13 seconds incremental. Test runtime: 13 ms.

r2 — twenty passing tests is not twenty witnessed claims. Nine of the twenty operate on hardcoded constant vectors and never read the captured telemetry; most of the remainder assert only that a value is finite, that a count is non-negative, or that a sort sorted. Those assertions have no falsifying input. The framework in §2 is sound and is unaffected; the claim-test suite is not evidence for it. See §9.2.

Deterministic outputs:

• Auth packet ID: f3447d87ba5e5df0... — identical across hosts, identical across builds, identical between the sovOS source tree and the WISP Deploy.
• Quantization coherence on captured geometry: 0.9143 — identical across runs (input-determined, no stochastic component).
• Worst-case temporal unit-circle deviation: 5.96 \times 10^{-8} — identical across runs.
• Coherence between consecutive composites: 0.9999.

Audit ledger after one claim-1 run:

12 witnesses total
  SIG-C01: 1   (provenance anchor)
  SIG-S13: 1   (quantization coherence)
  SIG-T05: 8   (temporal unit circle, one per observation in the window)
  SIG-T06: 1   (exponential decay)
  SIG-V03: 1   (coherence between composites)

Each witness is a content-addressed JSON record averaging ~250 bytes. Storage cost per witness is trivial; storage cost for a full audit corpus covering ten years of system operation at 1000 witnesses per second is under 100 GB.

6Discussion

6.1 Relationship to proof-carrying code

The framework is in the tradition of proof-carrying code (Necula, 1997), where compiled programs ship with a proof that they satisfy a safety policy, and the receiver verifies the proof before executing. Our setting differs in three ways.

First, the proofs are runtime witnesses, not static safety properties. We do not prove that the function will produce a value in the bound for all inputs; we prove that this function call, on this input, did produce a value in the bound. The audit ledger is the corpus of such demonstrations, accumulated over time, rather than a single static artifact attached to the binary.

Second, the proofs cover mathematical invariants, not safety policies. "Cosine returned a value in [-1, 1]" is not a property of memory safety or information flow; it is a property of the mathematical contract the function is presumed to satisfy. The framework is agnostic to whether the function was written by a human, a model, or generated mechanically — the invariant exists regardless of authorship and the witness exists regardless of authorship.

Third, the audit corpus is itself a research artifact. Replaying the ledger reproduces every mathematical step the pipeline took, with content hashes that any third party can verify. For patent reduction-to-practice arguments, for regulatory audits, for adversarial review of supposedly "compromised" runs, the ledger is the evidence that the system did what the documentation claims.

6.2 Connection to the Reasonability Protocol

The framework instantiates one dimension of what an earlier internal working note called the Reasonability Protocol — the discipline that LLM-authored systems must remain reason-able, meaning able to be reasoned about mechanically by something other than another LLM. The Protocol's schema proposes five dimensions: mathematical invariants, empirical benchmarks, boundary symbols, phase status, and reproducibility.

This paper covers the first dimension. Per-function math invariants become per-call witnesses; the ledger becomes the audit corpus; failed invariants become structured violations rather than panics. The remaining four dimensions of the Protocol — bench envelopes, IP-boundary symbol guards, phase-gate status verification, environment-frozen replay — are straightforward extensions of the same trait-plus-ledger pattern applied to non-mathematical predicates.

6.3 Why this works as a defense against LLM-authored opacity

A language model writing code is fluent by construction. It can produce the function, the test, the documentation, and the explanation — and all four can be wrong in mutually consistent ways. A reviewer reading the package cannot easily detect this; the surface signals all match.

The geometric proof framework breaks the fluency loop by introducing a predicate the model did not author. The cosine bound [-1, 1] is not a claim about the code; it is a fact of the mathematics the code purports to implement. No amount of fluent generation makes 1.5 lie inside [-1, 1]. If the function returns 1.5, the proof rejects, and the violation is recorded with the SIG, the value, the bounds, and a human-readable reason.

The defense is not that the model cannot lie. The defense is that the predicate is anchored outside the model's output. The mathematics did not come from the model; the SIGs predate the implementation; the bounds are properties of the operations themselves. A model that emits a buggy cosine function still cannot make 1.5 fall within [-1, 1] — that inequality is decided by arithmetic, not by review.

6.4 Scaling to the full registry

Seven SIGs is small. The surrounding system's formal registry has 250 SIGs across temporal, cryptographic, geometric, signal, governance, identity, silicon, repository, project-scribe, manifold, and other families.

r2 — the registry now carries 280 entries. The extrapolation below scales accordingly and the conclusion is unchanged. Extending the framework to cover all of them is mechanical: each SIG's mathematical statement already exists in the corresponding implementation crate (kronos-math, sage-functions, canon-functions, etc.); the work is lifting each statement into a GeometricProof implementation, declaring its bounds, and writing the input/output hashing rules.

Extrapolating from the seven-proof prototype, full coverage of the registry is approximately 7,500 LOC of Rust — three to four weeks of focused work for one engineer, less in parallel. The architecture does not need to change; only the table needs to be filled. Each SIG covered is one more dimension of mathematical claim the system can mechanically witness rather than assert. The audit corpus grows monotonically; older witnesses remain valid; the framework does not invalidate prior runs.

6.5 Open questions

Three open directions deserve note.

Type-level proof carrying. The current proven wrapper is a runtime check; a programmer can call the unwitnessed function directly and bypass the audit. A type-level extension would introduce Proven<T> such that downstream consumers can only accept values that have been through proven — the type system itself becomes the enforcement. This is implementable in Rust today but requires careful threading through every call site; the prototype here is the runtime form.

Formal verification integration. The runtime predicates assert "this call passed"; they do not assert "all calls will pass." A formal verification pass (e.g., via Creusot or Kani) over the implementation crates would provide the static complement. The two forms compose naturally: the static proof guarantees the function meets its contract for all inputs; the runtime witness records that it did so for this specific input. The audit ledger remains the empirical corpus regardless of static verification status.

Composition under failure. When a proof rejects, downstream processing halts. In a pipeline of n stages, the system must decide whether a single rejection terminates the entire pipeline, or whether some stages tolerate violations from upstream. The framework leaves this to the caller — proven returns Result, and the caller decides what to do with the violation. A future direction is articulating a composition algebra over violations: which violations are recoverable, which propagate, which trigger archival, which require human escalation. The patent's four-state authorization model (Approve / Deny / Escalate / Delay) is a candidate basis for this algebra.

7Related work

The framework borrows from several traditions:

• Proof-carrying code (Necula 1997, Lee & Necula 2000) — programs ship with proofs the receiver verifies. Our witnesses are dynamic rather than static; our predicates are mathematical rather than safety properties.
• Property-based testing (QuickCheck, Hypothesis) — predicates evaluated against generated inputs. Our predicates are evaluated against actual runtime inputs, and the predicate becomes the authorization rather than merely the test signal.
• Cryptographic execution boundaries (m_aegis-style five-step verification chains) — proof-of-work, verifiable delay function, hash chain consumption, cosine threshold, Merkle crystallization gating execution. We generalize this pattern from cryptographic to mathematical invariants and from one chain to many independent SIGs.
• Information flow control (Sabelfeld & Myers 2003) — typed systems that prevent secrets from flowing into observable channels. Our framework is information-flow-adjacent in that the proof authorizes the output to flow; without the proof, the output does not.
• Append-only audit ledgers (Bitcoin, Certificate Transparency) — hash-linked sequential records that any participant can verify independently. Our audit ledger is structurally similar but at the per-function-call granularity, not per-transaction.

The novel contribution is the integration: applying the audit-ledger pattern to per-function mathematical witnesses, on real captured input, inside an actual filed-patent's claim pipeline, with structured rejection of violations.

8Conclusion

A system whose every mathematical step is witnessed by an externally-anchored predicate is a system whose claims about itself can be checked mechanically rather than read prosaically. The framework described here makes that property tractable in two ingredients: a trait that declares what the predicate is, and a wrapper that gates execution on the predicate passing.

The worked example demonstrates the property holds in a real instance: 974 captured biometric observations, twenty patent-claim tests passing, four proof-rejection tests passing, twelve witnesses generated, one audit-ledger artifact. The implementation cost is modest — under 600 lines of new Rust for the framework, ~150 lines per SIG implementation — and the runtime cost is negligible. The discipline is composable with existing testing, with existing verification, with existing audit practices.

Where this matters most is in systems whose internals are increasingly authored by entities that can produce confident output without necessarily producing correct output. Bounded falsifiability per function is the corrective. The proof is the only authorization. Without the proof, the output does not propagate. This is not a guarantee that the system is correct; it is a guarantee that incorrect outputs leave a mechanical trace, named by SIG, dated, hashed, and appended to a corpus that can be replayed by any party with the same source.

The system can still lie. The mathematics cannot.

9Revision record

Added in r2, 2026-08-31.

Between May and August 2026 the reference implementation of SF-WISP-STD-001 was written, applying this method from the first line rather than retrofitting it onto finished code. That exercise falsified several claims in r1. This section records every one, because a paper arguing that mechanical checks should outrank confident prose has no standing to correct itself quietly.

None of these was found by review. All were found by an implementation forced to decide something the paper left open — which is the argument of §1.1, turned on the paper that makes it.

9.1 Wrong signature identifiers

Two of the seven proofs in §3.3 named the right mathematics under the wrong registry entries. The authoritative registry is the 280-entry mathematical_formulas.md.

This is a provenance error rather than a technical one, and it is the more consequential kind. A signature identifier is a claim about which body of filed matter a piece of work reads on, and a wrong one points at the wrong family. The mathematics in both proofs was and remains correct.

SIG-I10 — Identity Signal Drift Detection — is the entry that looks like the natural anchor for a drift bound and is not usable here: it belongs to the passive-observation family, alongside observe(wisp), observe(warrant), observe(auth_state) and observe(health). That family is under separate review and is out of scope for this method. The correct reading is that a drift measurement is an L2 distance (SIG-V06) and the ceiling is a deployment's policy — thresholds do not belong inside signatures, because binding one there makes every deployment that tunes it non-conforming.

The reference implementation prevents recurrence structurally: a test scans every source file for SIG- citations and fails on any that is not declared in a bindings table. It caught the SIG-S29 binding within seconds of that binding being written. What the test does not check is that a declared title matches the registry's, because the registry lives outside the workspace; that check remains manual and was performed on 2026-08-31.

9.2 Figures that do not measure what they are described as measuring

Three empirical results in §3.4 and §5 are not evidence for what they are cited as evidencing. The defect is in the claim-test suite, not in the framework of §2.

mean_cosine = 1.0000. wisp-test/tests/bdy001_patent.rs:174 binds the five-tuple returned by fuse_geometry positionally, under names that do not match the return order. The quantity reported as mean_cosine is in fact the acoustic fusion weight, which can only ever take the values 0.0, 0.5 or 1.0 — so a reported 1.0000 carries no information about coherence at all. This is the failure mode that makes tuple returns dangerous, and the correction in the reference implementation is structural: return values are bound by name, never by position, so this class of error cannot be written.

Quantization fidelity 0.9143. The figure compares a vector against its own clipped sign pattern rather than against a dequantized reconstruction. It measures something real, but not the property SIG-S13 is cited for.

"Twenty independent claim-property tests pass." Nine of the twenty operate on hardcoded constant vectors and never read the captured telemetry. Most of the remainder assert only that a value is finite, that a count is non-negative, or that a sorted collection is sorted — assertions with no falsifying input, which therefore establish nothing. A conformance test should be able to state what input would have made it fail; these cannot.

One further point of accuracy: r1 refers throughout to the narrative vector as an embedding. There is no embedding model in that workspace. The narrative vector is six DSP scalars. That does not affect the framework — a predicate does not care how its input was produced — but it does affect §3.2's description of the corpus, and the abstract's "974 captured biometric observations processed through the patent's claim-1 pipeline" is better read as 974 captured DSP observations.

9.3 The structural defect — and the change to the method it forced

This is the correction worth reading, because it changed the method's statement rather than its implementation.

ProofWitness.timestamp_ms in r1 is populated by SystemTime::now(). The timestamp is a field of the witness, so it is inside the witness's content address, so two runs over identical inputs produce different witnesses and a different ledger. §2.4 anticipates this and waves at it — "identical ledgers byte-for-byte (modulo timestamps)" — but the parenthesis is the whole problem. If the ledger has no stable identity, no ledger root may be cited as evidence of anything, and the audit corpus that §1.3 offers as the paper's third contribution cannot do the work it is offered for.

The fix is not a code change. It is a constraint that belongs in the method's statement:

The clock is an argument, never a read. Every timestamp entering a witness is supplied by the caller. No component of a proof-gated computation reads a system clock, allocates randomness, or consults ambient state.

Two further constraints followed from applying that one honestly:

Predicates must be integer. r1's predicates are f64. f64::ln, f64::sin and f64::exp are not required by IEEE 754 to be correctly rounded, so two machines running the same binary can produce different predicate values and therefore different witnesses. A witness that reads differently on two machines is not evidence. The reference implementation moved every predicate to Q16.16 fixed point and supplied integer equivalents — square root, binary and natural logarithm, negative powers of two — for each transcendental the governance path needs.

"Undefined" is a state, not a value. r1 needs an is_finite check because a float predicate can silently become NaN. Integers have no NaN, so the undefined case has to be said out loud: the predicate returns an option, and None — a cosine of a zero-magnitude vector, a logarithm of zero — is a violation rather than a number a caller could compare against a bound. This is strictly better than the r1 form, because it makes the undefined case unrepresentable as a score rather than merely detectable after the fact.

The ledger needed a different structure. §2.4's append-only JSONL commits to the corpus and nothing more. It offers no way to disclose one witness without disclosing every witness, which is exactly what a party publishing evidence for a single measurement needs. Hashing all entries into one digest does not help: that is a set commitment, not a Merkle tree, and it yields no sibling path. The reference implementation replaced the flat file with an ordered binary Merkle tree with real inclusion proofs — leaves and internal nodes domain-separated against second-preimage substitution, lone nodes promoted rather than duplicated, and siblings combined by position rather than sorted so that the order of a run is committed rather than discarded.

9.4 What r1 got right, and what the implementation confirmed

The framework of §2 survives unchanged in shape. The trait, the wrapper, the witness-as-authorization property, and the failure taxonomy of §4 are all reproduced in the reference implementation with no structural revision.

The load-bearing rule of §2.1 — that a predicate is a property of the operation rather than a re-derivation of it — proved to be the most valuable sentence in the paper, and its importance grew rather than shrank. In a system with replaceable comparison, normalization and composition components, the numbers reaching a governance gate were computed by code the gate has never seen. Re-deriving a value and comparing establishes only that two implementations agree, which is worth very little when one of them is the component under suspicion. A property is checkable without trusting the producer. That is the difference between a check and a second opinion.

§6.3's argument also held up under a stronger test than r1 could run. A comparison component reporting a cosine of 3.0 sails past any threshold comparison; the invariant catches it, the authorization is withdrawn, and the refusal is recorded. In the reference implementation a violated invariant forces the most restrictive decision state irrespective of what the policy concluded, and the operator is told that the denial came from a broken invariant rather than a low score — because those two call for completely different responses, and reporting both as "denied" loses the distinction that matters.

§6.5's first open question — type-level proof carrying — remains open and remains the right next step. The runtime wrapper is still bypassable by calling the underlying function directly.

9.5 Summary of changes in r2

No text from r1 has been deleted. Every correction is a marked addition, so that a reader comparing the two revisions can see what was claimed, what was wrong with it, and what replaced it.

Artifacts

All artifacts are at /Users/arc/Git/WISP Deploy/:

• wisp-proof/src/lib.rs — the GeometricProof trait, ProofWitness, ProofViolation, SigId, and the proven() wrapper.
• wisp-proof/src/audit.rs — the AuditLedger JSONL appender.
• wisp-proof/src/sigs/ — the seven concrete proofs (cosine.rs, decay.rs, temporal.rs, provenance.rs, quantization.rs, entropy.rs, drift.rs).
• wisp-test/tests/bdy001_patent.rs — twenty tests, one per BDY001 claim, on real captured telemetry.
• wisp-test/tests/bdy001_proven.rs — the proof-gated pipeline

+ three failure-mode tests.

• data/logos-manifold.jsonl — the 974-observation captured fixture.
• data/proof-audit.jsonl — the audit ledger produced by one proven-pipeline run.

Build: cargo build --workspace. Test: cargo test -p wisp-test. Witnesses appear in data/proof-audit.jsonl after running bdy001_proven.

r2 — the current reference implementation. The method as corrected by §9 is implemented in the SF-WISP-STD-001 reference workspace, where wisp-proof carries the trait, the wrapper, the Merkle-rooted ledger and the cell protocol, and wisp-proof::governance applies proof gating to a full governance evaluation. The proofs there are integer-valued, the clock is an argument at every level, and the ledger root of a run is reproducible across runs and hosts. That workspace, not the r1 artifact above, is the one to read for a working example.

References

Necula, G. C. (1997). Proof-Carrying Code. Proceedings of POPL'97.

Lee, P., & Necula, G. C. (2000). Research on Proof-Carrying Code for Untrusted-Code Security. IEEE Computer.

Sabelfeld, A., & Myers, A. C. (2003). Language-Based Information-Flow Security. IEEE Journal on Selected Areas in Communications, 21(1).

Claessen, K., & Hughes, J. (2000). QuickCheck: A Lightweight Tool for Random Testing of Haskell Programs. Proceedings of ICFP'00.

U.S. Patent Application 19/308,229 (2025-08-23, NoA 2026-04-27). System and Method for Semantic Identity Authentication Using Multimodal Vector Embeddings and Temporal Coherence Analysis.

This paper is the methodology companion to the WISP Deploy artifact. It describes the open framework. The proprietary application surface — the remaining 243 SIGs, the broader system substrate, the four-state authorization model, the bipartite cryptographic warrant anatomy, the N-strand topological memory manifold — is filed but not disclosed here.