# AMRAL × Lebesgue Universal Covering — Round 13
## Proof-State Scheduler and Autonomous Work Allocation

**Document ID:** AMRAL-LUC-FC-R13  
**Version:** v0.1  
**Date:** 2026-09-19  
**Research status:** Round 13 / Autonomous proof orchestration  
**Research mode:** Human-Directed + Semi-Autonomous AI Mathematical Research  
**Research initiation and methodology source:** Neo.K  
**AI collaborating researcher and primary executor:** Aletheia / ChatGPT, GPT-5.6 Sol  
**Prior documents:** AMRAL-LUC-FC-R00 v0.2; R01–R12 v0.1  

---

# 0. This round's summary verdict

Round 12 established:

$$
\boxed{
\text{persistent distributed proof checkpoint}.
}
$$

Round 13 goes on to answer:

> Once a checkpoint has a pending frontier, how should an AI / local worker autonomously pull work and return results without a race condition or a stale worker corrupting the canonical proof state?

This round establishes:

1. an immutable Job Contract;
2. an immutable Worker Proposal;
3. the Canonical Merger single-writer rule;
4. lease = performance-only;
5. stale-worker semantic rebase;
6. Certified Ancestor Contraction;
7. late-expansion obsolescence;
8. active-claim rejection reopening;
9. the atomic merge theorem;
10. deterministic active-claim selection;
11. an actual concurrent-race dry run.

This round's verdict:

$$
\boxed{
\text{AUTONOMOUS SCHEDULER / MERGER ABI: CLOSED}
}
$$

$$
\boxed{
\text{CONCURRENT RACE SAFETY: TESTED}
}
$$

$$
\boxed{
\text{GLOBAL }0.8350\text{ HEAVY COMPUTE: STILL DEFERRED}
}
$$

---

# 1. A worker may not change canonical state

The Round 12 checkpoint is the sole proof source of truth.

A worker is not permitted to directly modify:

- the frontier;
- active claims;
- theorem-ready status;
- pending seeds;
- stale state.

A worker may only produce a:

$$
\boxed{
\text{Proposal}.
}
$$

The Canonical Merger:

$$
\boxed{
\text{Proposal}
\to
\text{Validated State Transition}
}
$$

is the only legal write path.

---

# 2. Job Contract

The scheduler produces, for a worker:

$$
J
=
(
id,
type,
CP,
H_{\rm dep},
p,
scope,
caps,
lease
).
$$

where:

- $CP$: the base checkpoint id;
- $H_{\rm dep}$: the proof-critical dependency fingerprint;
- $p$: the seed path;
- caps: node/time/resource limits;
- lease: used to prevent duplicate computation.

---

# 3. Job type

Mainly:

## `CERTIFY_SEED`

Attempts full closure of:

$$
B(p).
$$

## `EXPAND_SEED`

If closure is too hard, returns the complete descendant frontier.

## `LIFT_SEED`

Performs a witness conditional lift on a base seed.

## `AUDIT_CLAIM`

Performs an A2/A3 audit on an existing active claim.

## `SEARCH_WITNESS`

Only performs candidate discovery; does not directly enter proof state.

---

# 4. A lease is not part of the proof

A lease consists of:

- worker id;
- issued time;
- expiry;
- retry count;

and is nothing more than performance state.

Therefore:

$$
\boxed{
\text{lease expired}
\not\Rightarrow
\text{certificate invalid}.
}
$$

A certificate that arrives late can still be accepted via semantic rebase.

---

# 5. Worker Proposal

A worker returns an immutable:

$$
P
=
(
proposal\_id,
type,
job\_id,
CP,
H_{\rm dep},
p,
payload
).
$$

Proposal type:

- `CERTIFY`
- `EXPAND`
- `AUDIT_PASS`
- `AUDIT_FAIL`
- `COUNTEREXAMPLE`
- `INCONCLUSIVE`

A proposal by itself does not change proof state.

---

# 6. Proposal acceptance: first gate

The Canonical Merger first checks:

1. payload hash;
2. dependency fingerprint;
3. seed identity;
4. artifact hashes;
5. proposal type schema.

If the theorem-critical dependency differs:

`STALE-PROPOSAL`

and it is not merged.

---

# 7. EXPAND acceptance rule

For:

$$
p\to\mathcal D_p,
$$

this is accepted directly only when:

$$
p
$$

is still the current pending terminal frontier seed.

And it is verified that:

$$
\boxed{
\mathcal D_p
\text{ prefix-free and complete below }p.
}
$$

Accept:

$$
\mathcal P'
=
(\mathcal P\setminus\{p\})
\cup
\mathcal D_p.
$$

---

# 8. EXPAND does not allow an arbitrary rebase

If a worker, from an old checkpoint, returns an expansion for:

$$
p
$$

but the current frontier has already:

- split more finely; or
- $p$ is already certified;

the merger does not let the old expansion forcibly overwrite the current partition.

State:

`OBSOLETE-EXPANSION`

Reason:

the proof has no need to risk losing newer evidence for the sake of an arbitrary repartition.

---

# 9. CERTIFY acceptance rule

If:

$$
p
$$

is still the current pending seed,

a valid A1 certificate can directly close:

$$
p.
$$

If:

$$
p
$$

has already been split,

it cannot simply be called "stale."

Because the certificate may in fact prove the entire ancestor box:

$$
B(p).
$$

This is what leads to this round's core new theorem.

---

# 10. Certified Ancestor Contraction Theorem

## Theorem 10.1

Let the current frontier be:

$$
\mathcal P
$$

and let the part of it below the ancestor:

$$
p
$$

be:

$$
\mathcal D_p
=
\{
q\in\mathcal P:
p\preceq q
\}.
$$

Assume:

1. $\mathcal D_p$ complete-covers $B(p)$;
2. there exists a current-dependency valid certificate:

   $$
   c_p
   $$

   that directly proves:

   $$
   \forall x\in B(p),
   \quad
   \Phi(x)\ge T.
   $$

Then:

$$
\boxed{
\mathcal P'
=
(
\mathcal P\setminus\mathcal D_p
)
\cup
\{p\}
}
$$

is still a complete frontier, and using:

$$
c_p
$$

as $p$'s active claim is sound.

### Proof

The original:

$$
\mathcal D_p
$$

merely covers, within the proof partition:

$$
B(p).
$$

The new certificate directly proves the entire:

$$
B(p).
$$

So the descendants' coverage obligations are all absorbed by the ancestor claim.

The other branches are unchanged.

Q.E.D.

---

# 11. Race resolution: EXPAND first, CERTIFY later

Worker A:

$$
p\to\{p0,p1\}.
$$

merges first.

Worker B later returns an ancestor:

$$
c_p.
$$

As long as:

- the dependency is current;
- the certificate is valid;

the merger can perform:

$$
\boxed{
\{p0,p1\}
\to
\{p\}
}
$$

So the race does not force the certificate to be discarded.

---

# 12. Race resolution: CERTIFY first, EXPAND later

If:

$$
p
$$

is closed by a verified claim first,

a late-arriving expansion:

$$
p\to\{p0,p1\}
$$

is unnecessary.

Marked:

$$
\boxed{
\texttt{OBSOLETE-COVERED-BY-CERTIFIED-ANCESTOR}.
}
$$

Proof state that has already been closed cannot be split open again.

---

# 13. Descendant evidence is not deleted

Ancestor contraction only changes:

$$
\text{active frontier}.
$$

For completed descendants, the:

- certificate;
- audits;
- metrics;

are all retained, append-only.

If the ancestor claim is later rejected, they can be reused.

---

# 14. Claim rejection after contraction

If the active ancestor claim:

$$
c_p
$$

is rejected by a valid audit:

1. $c_p\to\texttt{REJECTED}$;
2. $p$ becomes:

   `PENDING`;
3. global theorem-ready becomes false.

Soundness does not require immediately restoring the earlier descendants.

The scheduler may:

- re-expand $p$; or
- find previously completed descendant evidence from history to build a new proposal.

---

# 15. Multiple CERTIFY proposals

Two workers may simultaneously prove:

$$
p.
$$

If both are valid:

- both claims are retained;
- only one is selected as the active primary.

Deterministic selector:

$$
\boxed{
\min
\text{ canonical claim hash}.
}
$$

The other is auxiliary evidence.

Final coverage is still "one active owner per seed."

---

# 16. Duplicate compute is legal

A lease only reduces waste.

The proof protocol allows:

- two emitters for the same seed;
- two auditors for the same claim;
- multi-machine replay of the same shard.

Duplication does not create a correctness conflict.

What the merger handles is:

$$
\boxed{
\text{evidence identity}
}
$$

not:

$$
\boxed{
\text{worker ownership}.
}
$$

---

# 17. Stale worker semantic rebase

A worker's base checkpoint:

$$
CP_{\rm old}
$$

may lag behind the current:

$$
CP_{\rm new}.
$$

It is not rejected outright just because the checkpoint id differs.

### CERTIFY

As long as:

- the seed box identity is still semantically the same;
- the proof dependencies are current;
- the certificate covers the ancestor box;

a semantic rebase is possible.

### EXPAND

Accepted only when the parent seed is still the current pending terminal.

---

# 18. Audit proposal

An A2/A3 worker returns:

`AUDIT_PASS`

or:

`AUDIT_FAIL`.

Even the worker's own verdict is just a proposal.

For a FAIL artifact, the Canonical Merger performs at least:

- a counterexample schema check;
- a hash check;
- a failure replay / minimal independent check.

Only a valid FAIL updates the claim to:

`REJECTED`.

---

# 19. Counterexample dominance

Any valid counterexample:

$$
x\in B(p)
$$

that makes the claimed inequality fail

is sufficient by itself to reject:

$$
c_p.
$$

No vote from other auditors is required.

Once again:

$$
\boxed{
\text{evidence dominance}
\ne
\text{majority vote}.
}
$$

---

# 20. Atomic Merge Theorem

## Theorem 20.1

Assume that, before the transition, the checkpoint has:

- a prefix-free frontier;
- a complete frontier;
- every theorem-ready seed carrying a valid active claim.

If each step uses only the following primitives:

1. pending seed -> verified claim;
2. pending seed -> complete descendant frontier;
3. complete descendant frontier -> verified ancestor claim;
4. active claim reject -> pending seed;
5. append audit / auxiliary claim;
6. dependency-stale filtering;

then after any finite sequence of accepted transitions:

1. the frontier is still prefix-free;
2. the frontier is still complete;
3. if:

   `theorem_ready=true`

   then every frontier seed carries a current, valid active claim.

### Proof

By induction on the length of the transition sequence.

Each primitive preserves the invariant, respectively, via:

- direct closure;
- Round 11 frontier replacement;
- Certified Ancestor Contraction;
- reopening without claiming theorem-ready;

Q.E.D.

---

# 21. Canonical merger is single writer

Even with 100 workers running in parallel,

the canonical state transition is still serialized as:

$$
CP_0
\to
CP_1
\to
CP_2
\to\cdots
$$

Worker proposals can be parallel.

The merger commit must be atomic.

This is the proof-state equivalent of a single-writer / multi-producer pattern.

---

# 22. Merge journal

Every accepted/rejected proposal records:

```text
proposal_id
base_checkpoint_id
current_checkpoint_id_at_merge
decision
reason
result_checkpoint_id
```

This is the orchestration audit trail.

It does not enter the mathematical premises, but it matters for race debugging.

---

# 23. Scheduler job source

The scheduler always draws jobs from the:

$$
\boxed{
\text{current canonical checkpoint}
}
$$

Priority sources:

1. pending frontier;
2. un-audited active claims;
3. hard unresolved witness cells;
4. stale claims needing revalidation.

---

# 24. Job priority

Round 09 supplies:

- uncertainty $\tau$;
- margin $m$;
- predicted depth;
- historical nodes.

For parallel finish time, the recommendation is:

$$
\boxed{
\text{TAIL-FIRST}
}
$$

giving dispatch priority to the seeds predicted to be hardest.

Because easy seeds usually do not determine the global makespan tail.

This is a heuristic; it does not affect the proof.

---

# 25. Job caps

A worker job may specify:

```text
node_cap
wall_cap
memory_cap
max_depth
```

If a cap is hit:

- it must not fake a leaf;
- it returns an EXPAND descendant frontier;
- or INCONCLUSIVE.

---

# 26. Autonomous local worker loop

```text
pull current job

if job = CERTIFY:
    run proof search
    if closed:
        emit CERTIFY
    elif node cap:
        emit EXPAND
    else:
        emit INCONCLUSIVE

if job = AUDIT:
    independently replay
    emit AUDIT_PASS / FAIL

never mutate checkpoint
```

---

# 27. Canonical merger loop

```text
read latest checkpoint
validate proposal
compare dependency fingerprint
reconstruct seed relation to current frontier

case CERTIFY:
    current pending -> close
    descendants current -> ancestor contraction
    already covered -> auxiliary/obsolete

case EXPAND:
    current pending terminal -> replace
    otherwise -> obsolete

case AUDIT_FAIL:
    if valid -> reject claim, reopen coverage obligation

append merge journal
emit new checkpoint
```

---

# 28. Reference concurrent-race dry run

Round 13 uses Round 12's:

`checkpoint_v4_rejected_B`

as its starting point.

In that checkpoint:

$$
\boxed{
01
}
$$

is the sole pending seed.

---

# 29. Scheduler dispatches two parallel jobs

Deliberately simulating a duplicate/race:

## Job A

`EXPAND_SEED(01)`

proposal:

$$
01
\to
\{010,011\}.
$$

## Job B

`CERTIFY_SEED(01)`

using the real reference evidence of Round 12's V5 corrected shard-B claim.

Both jobs come from the same old checkpoint.

---

# 30. Merge A first

Accept the expansion first:

$$
\{00,01,10,11\}
\to
\{00,010,011,10,11\}.
$$

At this point:

$$
010,\ 011
$$

are pending.

Global:

`theorem_ready=false`

PASS.

---

# 31. Late certificate semantic rebase

Job B comes back late.

Although:

$$
01
$$

is no longer a terminal seed,

nonetheless:

$$
\{010,011\}
$$

complete-covers:

$$
B(01).
$$

and the certificate is current and proves the entire:

$$
B(01).
$$

The Canonical Merger performs:

$$
\boxed{
\{010,011\}
\to
\{01\}.
}
$$

and appends the corrected verified claim.

Global:

$$
\boxed{
\texttt{theorem\_ready=true}.
}
$$

PASS.

---

# 32. Late expansion after closure

Another:

`EXPAND(01)`

is submitted.

At this point:

$$
01
$$

already has a current active verified claim.

The merger:

$$
\boxed{
\texttt{OBSOLETE-COVERED-BY-CERTIFICATE}.
}
$$

The frontier is unchanged.

PASS.

---

# 33. Reference result

The machine dry run confirms:

| Step | Frontier | Ready |
|---|---|---:|
| start | `{00,01,10,11}` | false |
| expand | `{00,010,011,10,11}` | false |
| late certify + contraction | `{00,01,10,11}` | true |
| late expand | unchanged | true |

So the most important async race has actually been run through.

---

# 34. Why this matters for global $0.8350$

In a real heavy run:

- some local worker may still be proving a large seed;
- the scheduler has already timed out and split the same seed to someone else;
- the old worker comes back hours later with a complete certificate.

Without ancestor contraction:

the old work is wasted.

With ancestor contraction:

if the proof is still current, the entire descendant workload can be eliminated outright.

So:

$$
\boxed{
\text{late strong evidence can dominate newer finer partition}.
}
$$

---

# 35. Proof-state monotonicity is not frontier monotonicity

Frontier depth does not necessarily only increase.

It can go:

$$
p
\to
\{p0,p1\}
\to
p.
$$

What is truly monotone is the:

$$
\boxed{
\text{append-only evidence history}.
}
$$

The active partition may refine or contract.

---

# 36. Worker result trust categories

Proposed:

## `PROOF-CANDIDATE`

The worker believes it is provable.

Still requires A1 canonical replay.

## `SEARCH-CANDIDATE`

Only a numerical result.

Cannot close the seed.

## `COUNTEREXAMPLE-CANDIDATE`

If the canonical check is valid, it can reject a claim.

## `EXPANSION-CANDIDATE`

Only changes the work partition; makes no claim of proof.

---

# 37. Global scheduler authority split

## Scheduler

May decide:

- what gets computed first;
- which worker it goes to;
- node cap;
- duplicate work.

## Worker

May produce a proposal.

## Verifier

May produce audit evidence.

## Canonical Merger

The only one that may:

$$
\boxed{
\text{change canonical proof state}.
}
$$

This is this round's most important governance boundary.

---

# 38. COMPUTE-DEFERRED

## C13-1

Feed the real global:

$$
T=0.835
$$

checkpoint into the scheduler.

## C13-2

Build a local worker adapter:

```text
checkpoint job JSON
-> local Python
-> proposal JSON
```

## C13-3

Build a lagged AI audit adapter.

## C13-4

Automatically produce a new checkpoint + State Crystal on every merge.

## C13-5

Test multi-worker races:

- duplicate certify;
- expand/expand;
- certify/audit fail;
- stale dependency mid-run.

---

# 39. Round 14's assigned topic

## AMRAL-LUC-FC-R14
### Semantic Rebase, Claim Dominance, and Proof-State Garbage Collection

The next round can address:

1. how an old worker proposal performs semantic rebase;
2. certificate ancestor / descendant dominance;
3. when auxiliary evidence can be archived;
4. when stale artifacts can be moved out of the hot checkpoint while keeping history;
5. proof-state compaction;
6. keeping checkpoint size from growing unboundedly with millions of shards of history.

This will move the distributed proof-state further, from "correct" to also "maintainable over the long term."

---

# 40. Reproducibility checklist

## Worker/merger authority split

`FORMALIZED`

## Lease non-semantic rule

`FORMALIZED`

## Ancestor contraction

`PROVED`

## Late expansion obsolescence

`FORMALIZED`

## Atomic merge invariants

`PROVED`

## Reference async race

`PASS`

## Global autonomous workers

`COMPUTE-DEFERRED`

---

# 41. Shortest handoff conclusion

Round 13 completes:

$$
\boxed{
\text{Checkpoint}
\to
\text{Jobs}
\to
\text{Worker Proposals}
\to
\text{Canonical Merge}
}
$$

The most important new closure:

$$
\boxed{
\text{Certified Ancestor Contraction}.
}
$$

So a worker's late-arriving strong certificate is not wasted just because the scheduler has already split the seed more finely.

The distributed proof now has:

- parallel producers;
- a single canonical writer;
- stale-worker rebase;
- race-safe frontier refinement / contraction;
- append-only evidence;
- fail-closed audit.

It can therefore safely connect more autonomous AI / local runtimes, without any worker itself gaining the power to "declare a proof established."