Arena 5 — Autonomous mutation: unsupervised PR with zero-trust merge

• Parent: README.md
• Formal index: ../FORMAL_LEDGER.md
• Prerequisite: TOPO_COGNITIVE_EVENT_HORIZON.md ((\pi_{\mathrm{cool}}), (S_{\mathrm{cog}}), (\mathcal{V}))
• Layer C policy: ../lean/Lean/ForkRaceFoldTheorems/EntropyBridge/README.md

State: The stack runs under cooling; the operator is intentionally out of the review path. (X(t)) still worsens because of a live defect in a distributed data pipeline. An autonomous agent proposes a patch (non-deterministic search). Challenge: merge only what deterministic gates can certify; never confuse proposal entropy with proof.

This note is architecture and epistemic discipline—not a product warranty. It extends the same boundary rule: stochastic generation is Layer C-ish noise; anything merged into the sealed artifact must be a bitwise-checkable closure under a fixed verifier.

1. Asymmetric proof burden — search vs verification

1.1 Decoupling (non-negotiable)

The autonomous actor may emit arbitrary junk until something passes the closed verifier (V). Trust attaches to (V), not to the actor.

1.2 The mechanically checkable artifact (what CI “blindly” accepts)

A merge promotion (even without humans) should require a bundle that a pure function of repository state + logs can validate:

Minimum bundle (engineering floor):

1. Deterministic patch identity: commit SHA (or content-addressed tree) of the exact diff applied — no floating “latest.”
2. Verifier closure: sequential green outputs from a pinned CI graph:
   • lake build (or project-equivalent) on exact lockfile + toolchain pin.
   • Targeted test suite for touched packages (affected slice), full suite if blast radius crosses boundaries (policy table).
3. Proof delta (if formal surface touched): Lean/TLA+ regeneration of obligations for changed modules — CI fails if new sorry or weakened theorem statements without a versioned exception file (explicit human-signed path not available here → no exceptions during unsupervised mode).
4. Reproducible attestations: cryptographic hashes of inputs to the verifier (lockfile hash, CI config hash, container digest). Stored as signed metadata (e.g. Sigstore/OIDC to the merge bot identity) so the bundle is not repudiable after the fact.

The exact object the bot must attach: not “trust me” prose — a machine-readable verification.json (name illustrative) containing at least:

{
  "patch_content_id": "<git-tree-or-bundle-hash>",
  "toolchain_id": "<exact resolver pin>",
  "ci_config_id": "<hash of workflow + container>",
  "gates": [
    { "name": "lake_build", "exit": 0, "log_hash": "…" },
    { "name": "lean_affected", "exit": 0, "log_hash": "…" },
    { "name": "jest_affected", "exit": 0, "log_hash": "…" }
  ],
  "formal": { "sorry_count_delta": 0, "touched_modules": ["…"] }
}

Blind trust here means: the merge bot runs only verify(bundle) → Bool using public verifier code — same posture as Layer C named axioms: the axiom is not “the LLM is honest” but “this bundle hashes to a green closure under pinned (V).”

1.3 What is not sufficient

• Syntax-only or linter-only green — insufficient for routing semantics.
• “Looks good” embeddings or LLM self-critique — not gates.
• Merge to production without canary topology (section 2) — violates zero-trust.

2. Topological quarantine — edge structure under unsupervised merge

Problem: Deterministic CI can miss semantic faults (routing policy, DO routing keys, gradual partition) while syntax and unit tests pass.

2.1 Never promote directly to the global blast radius

Policy: Unsupervised pipeline promotes patches only to a quarantine revision that receives:

• Synthetic traffic and/or shadow execution (read-only, duplicated requests), or
• A canary slice of real traffic with strict upper bound on blast radius (percentage, tenant allowlist, geography).

2.2 Dynamic edge topology (illustrative mechanisms)

• Revision-tagged workers: Durable Objects / isolates keyed by (tenant, revision); production traffic stays on revision_stable until promotion criteria hold.
• Routing lattice: API gateway sends only canary cohort to revision_candidate; all others pinned to stable.
• Split-brain guard: control plane refuses global route table update until section 3 health holds on the canary subgraph.

“Topological quarantine” means: the deployed artifact for the patch lives in a low-measure subgraph (G_q \subset G) with measured ingress and no shared mutable state with the critical path until promoted (or copied state with explicit version vectors).

2.3 Semantic bombs beyond CI

Mitigations (stack in depth):

1. Differential probes: active checks that routing invariants hold (ping mesh, expected fan-out, quorum responses) — not just HTTP 200.
2. Property tests on routing DSL if one exists.
3. TLA+ / model-check of deployment transition (if you have a promoted spec).

3. Rollback invariant — (\lambda_2)-style collapse without humans

3.1 Observable surrogates on the quarantine subgraph

On (G_q(t)) (canary), maintain streaming estimates:

• Algebraic connectivity proxy (\widehat{\lambda}_2(t)) — sparse Laplacian sketch, Fiedler estimate, or cheaper surrogate: second-smallest eigenvalue of a sampled Laplacian, or conductance lower bound.
• β₁ slack (cycle rank) on the effective routing graph as seen by probes.
• Application SLOs: error budget burn, latency p99, repair backlog (X) if visible in metrics.

3.2 Pre-registered automatic trigger (mathematical form)

Choose thresholds ((\lambda_2^*, \tau, W)) before deploy (policy-as-code).

Example trigger (hysteresis-friendly):

[ \text{ROLLBACK}(t) \equiv \bigl(\widehat{\lambda}2(t) < \lambda_2^*\bigr) \ \text{for } \tau \text{ consecutive windows} \quad\lor\quad \int{t_0}^{t} \bigl(\lambda_2^* - \widehat{\lambda}2(s)\bigr)+, ds > W ]

(\lor) hard SLO breach (error rate, partition detector) or β₁ collapse below (\beta_{1,\min}) on monitored subgraph.

Rollback action: atomic traffic shift (G_q \mapsto \emptyset) for production; restore exact prior revision pointer (content-addressed); freeze autonomous merge until operator or stronger gate.

No human observation required — only telemetry feeds and pre-registered predicates. This is the same epistemic stance as automated circuit breakers.

3.3 Invariant statement (control-theoretic)

Let (S) be deployed revision, (S^*) stable. Define safe set (\mathcal{U}) in metric space of ((\widehat{\lambda}_2, \text{SLO}, X, \ldots)).

Rollback invariant: If the controller enters unsupervised promote from (S^*) to (S), there exists a measurable stopping time (T) such that on ({T < \infty}), traffic is reverted to (S^*) and (\mathcal{V}) (from TOPO_COGNITIVE_EVENT_HORIZON.md) is restored restricted to what automation can observe — not full human judgment.

4. Lean / formal ledger posture

• Unsupervised mode: no new sorry; no weakening of signatures without out-of-band approval — CI enforces.
• Autonomous PR: valuable as search; merge is a theorem only about (V(\text{bundle}) = \text{true}) — same EntropyBridge discipline: the machine does not “prove psychology”; it proves closure under the checker.

5. Honest limits

• Verification is only as strong as (V). Unknown unknowns in routing semantics remain — quarantine + rollback reduce blast radius; they do not eliminate it.
• Adversarial patches that pass tests but attack monitoring itself require independent observability (multi-party metrics, external probes).
• Human-out-of-loop is an operational mode, not an ethical default — document when it is enabled.

Standing closure

The autonomous enclosure is complete when four commitments hold at once: Layer C names what logic cannot derive; fluid + spectral dynamics bound structural death and operator coupling; (\pi_{\mathrm{cool}}) protects human capacity; proof-carrying merge makes the author of a patch epistemically irrelevant—only (verify(bundle) \in {\top,\bot}) under a pinned verifier (V) may promote code. (G_q) contains the mismatch between proved constraints and routing reality; the integral rollback on ((\lambda_2^* - \widehat{\lambda}2)+) turns sustained harm into an automatic sever without consensus.

Humility: Sealed means every gate is explicit—not that all failure modes are impossible. What lies outside (V) (unknown specs, gamed telemetry, adversarial observability) can still bite; the stack bounds and contains—it does not claim omniscience.

Implementation appendix (repository artifacts)

Sigstore/OIDC signing is not implemented in the reference verifier; extend signatures when binding merge-bot identity.

See also

• THREE_ARENAS_SYNTHESIS.md
• TOPO_COGNITIVE_EVENT_HORIZON.md
• RANDOMNESS.md
• EntropyBridge README