# AMRAL × Lebesgue Universal Covering — Round 14
## Semantic Rebase, Claim Dominance, and Proof-State Compaction

**Document code:** AMRAL-LUC-FC-R14  
**Version:** v0.1  
**Date:** 2026-09-19  
**Research status:** Round 14 / Long-running proof-state maintenance  
**Research mode:** Human-Directed + Semi-Autonomous AI Mathematical Research  
**Research initiation and methodology source:** Neo.K  
**AI collaborating researchers and primary executors:** Aletheia / ChatGPT, GPT-5.6 Sol  
**Prerequisite documents:** AMRAL-LUC-FC-R00 v0.2; R01–R13 v0.1  

---

# 0. This Round's Summary Verdict

Round 12–13 established:

$$
\text{checkpoint}
\to
\text{worker proposals}
\to
\text{canonical merge}.
$$

Once this genuinely runs long-term, new problems appear:

1. If a proof dependency's hash changes, must all old claims be recomputed?
2. When two claims can both prove the same region, which one should stay in hot state?
3. After rejected / stale / obsolete / superseded history accumulates into the millions of records, does the checkpoint balloon without bound?
4. If history is moved out of hot state, does that break theorem soundness?
5. If old evidence is needed again later, how can it be safely rehydrated?

Round 14 completes:

$$
\boxed{
\text{Semantic Compatibility}
}
$$

$$
\boxed{
\text{Claim Dominance}
}
$$

$$
\boxed{
\text{Minimal Active Proof Core}
}
$$

$$
\boxed{
\text{Hot / Cold Proof-State Compaction}.
}
$$

This round's main results:

- exact dependency-hash equality is demoted to a safe fast path, rather than being the only legal path;
- margin credit can migrate across target / scalar error budget via semantic rebase;
- unused witness-catalog extension does not make old claims stale;
- claim capacity is defined;
- claim dominance is defined;
- active proof reachability is defined;
- hot-core compaction is proved not to change current theorem-readiness;
- the cold archive is bound with content hash + Merkle root;
- the Round 13 reference checkpoint is actually compacted into a hot core plus cold archive;
- the semantic-rebase success/failure boundary is machine-tested;
- archive rehydration is machine-tested.

This round's verdict:

$$
\boxed{
\text{SEMANTIC REBASE LAYER: CLOSED}
}
$$

$$
\boxed{
\text{HOT/COLD PROOF COMPACTION: CLOSED}
}
$$

$$
\boxed{
\text{DESTRUCTIVE EVIDENCE DELETION: NOT AUTHORIZED}
}
$$

---

# 1. Round 12's Conservative Rule Is Still Correct

Round 12:

$$
H_{\rm dep}^{c}
=
H_{\rm dep}^{\rm current}
$$

is required before a claim is directly accepted.

This is:

$$
\boxed{
\text{a sound exact-identity fast path}.
}
$$

Round 14 does not negate it.

The problem is only:

> a hash mismatch does not mean the claim is necessarily mathematically incompatible.

So it adds:

$$
\boxed{
\text{a semantic implication path}.
}
$$

---

# 2. Semantic compatibility relation

For a claim:

$$
c
$$

and a current proof obligation:

$$
O,
$$

write:

$$
\boxed{
c\succeq_{\rm sem}O
}
$$

if the proposition already proved by the claim can logically imply the current obligation.

This must be decided by an explicit rule.

It cannot be decided by the model "feeling like" it is close enough.

---

# 3. Target monotonicity

If a claim proves:

$$
\Phi(x)\ge T_c
$$

over its full domain,

then for any:

$$
T'\le T_c
$$

it automatically holds that:

$$
\Phi(x)\ge T'.
$$

So lowering the target is:

$$
\boxed{
\text{naturally semantic-compatible}.
}
$$

But raising the target requires slack.

---

# 4. Scalar error-budget margin credit

Write the reference leaf's original one-sided quantity as:

$$
L.
$$

The old verifier accepts:

$$
L-e_c
\ge
T_c.
$$

Let the worst verified slack be:

$$
s_c
=
\min_{\rm leaves}
[
L-e_c-T_c
].
$$

Therefore:

$$
L
\ge
T_c+e_c+s_c
$$

for all leaves.

Under a new policy:

$$
e',
\qquad
T'.
$$

as long as:

$$
T'+e'
\le
T_c+e_c+s_c,
$$

the old raw witnesses still suffice to prove the new obligation.

---

# 5. Claim Capacity

Define:

$$
\boxed{
\operatorname{Cap}_{e'}(c)
=
T_c+s_c+e_c-e'.
}
$$

Then:

$$
\boxed{
T'
\le
\operatorname{Cap}_{e'}(c)
}
$$

is a sufficient condition for scalar-error semantic migration.

---

# 6. Margin credit ledger

Future production claims are recommended to always store:

```text
proved_threshold
verified_error_budget
worst_verified_slack
raw_lower_witness_policy
```

not just:

```text
PASS
```

because:

$$
\boxed{
\text{slack is a usable asset for future semantic rebase}.
}
$$

---

# 7. Reference capacity example

Round 11 local reference:

old:

$$
T_c=0.835,
$$

$$
e_c=10^{-8}.
$$

The worst slacks of three active shards:

## A

$$
s_A
=
3.8698779558643537\times10^{-7}.
$$

## B

$$
s_B
=
9.574949350055206\times10^{-7}.
$$

## C

$$
s_C
=
3.545377508240577\times10^{-7}.
$$

If the new error budget is:

$$
e'=2\times10^{-8},
$$

the capacities are:

$$
\operatorname{Cap}(A)
\approx
0.8350003769877956,
$$

$$
\operatorname{Cap}(B)
\approx
0.8350009474949350,
$$

$$
\operatorname{Cap}(C)
\approx
0.8350003445377508.
$$

So the aggregate capacity of this same local-reference proof under this stricter error policy is:

$$
\boxed{
T_{\rm cap}^{\rm ref}
\approx
0.8350003445377508.
}
$$

Again:

$$
\boxed{
\text{this is only Round 10/11 local reference scope,
not the global Lebesgue lower bound}.
}
$$

---

# 8. Target + arithmetic simultaneous migration

Round 14's actual test:

migrating from:

$$
T=0.835,
\qquad
e=10^{-8}
$$

to:

$$
\boxed{
T'=0.8350001,
\qquad
e'=2\times10^{-8}.
}
$$

All three active claims still have positive margin credit.

So:

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

within reference scope.

---

# 9. Migration boundary test

Pushing further to:

$$
T''=0.8350004
$$

with:

$$
e'=2\times10^{-8}.
$$

at this point at least A / C's capacity is insufficient.

So:

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

This proves the semantic validator is not:

> "dependency mismatch always passes."

but is genuinely bounded by the margin.

---

# 10. Witness catalog extension

A claim only depends on the witnesses actually used by its certificate.

If:

$$
W_c
=
\{B_7\}
$$

and the current catalog is:

$$
W'
=
\{B_7,B_9,\text{Fourier dictionary}\},
$$

then:

$$
\boxed{
W_c\subseteq W'
}
$$

so the catalog extension does not affect the old claim.

Therefore:

> adding new search candidates should not make an already-proved shard stale.

---

# 11. Witness mutation

If:

$$
B_7
$$

's geometric semantics / normalization changes,

then a claim that used:

$$
B_7
$$

cannot be reused merely by the catalog-superset rule.

What is needed is:

- exact geometric identity;
- or an explicit migration theorem;
- or revalidation.

---

# 12. Local dependency closure

A production claim should not bind the entire giant global dependency bundle.

It should store:

$$
\boxed{
D(c)
=
\text{the dependencies the claim actually uses}.
}
$$

for example:

- geometry modules used;
- witness ids used;
- arithmetic mode used;
- proof modes used;
- verifier semantics used.

A completely unrelated module added globally:

$$
\notin D(c)
$$

should not stale the claim.

---

# 13. Domain semantic rebase

If a claim proves an ancestor:

$$
B(p)
$$

while the current obligation is a descendant:

$$
B(q),
$$

where:

$$
p\preceq q,
$$

then:

$$
B(q)\subseteq B(p).
$$

So the ancestor claim:

$$
\boxed{
\text{dominates the descendant obligation}.
}
$$

This is the dependency-level generalization of Round 13's Certified Ancestor Contraction.

---

# 14. Descendant evidence is not an ancestor claim

In reverse:

$$
q\succeq p
$$

then a single:

$$
B(q)
$$

claim cannot prove:

$$
B(p).
$$

A complete descendant claim set is needed:

$$
\mathcal C_p
$$

covering:

$$
B(p).
$$

So:

$$
\boxed{
\text{single-claim dominance}
}
$$

and:

$$
\boxed{
\text{claim-set coverage}
}
$$

must be kept separate.

---

# 15. Claim Dominance

Define the current policy:

$$
\Pi.
$$

Claim:

$$
c_1
$$

dominates:

$$
c_2,
$$

written:

$$
c_1\succeq_\Pi c_2,
$$

if:

1. $c_1$'s domain covers $c_2$'s current-needed domain;
2. $c_1$'s semantic capacity is at least not lower than $c_2$'s;
3. $c_1$'s local dependency set is current-compatible;
4. $c_1$ has the required A1 evidence.

then:

$$
\boxed{
c_2
\text{ does not need to remain in the hot active proof core}.
}
$$

but the cold evidence cannot be deleted.

---

# 16. Same-seed dominance

For the same seed:

$$
p,
$$

two claims:

$$
c_1,c_2.
$$

if:

$$
\operatorname{Cap}(c_1)
\ge
\operatorname{Cap}(c_2)
$$

and:

$$
D(c_1)
\subseteq D(c_2)
$$

in the compatibility sense,

then the active primary should preferentially be:

$$
c_1.
$$

If the capacities are equal, use the canonical certificate hash as a tie-break.

---

# 17. Rejected claim never dominates

Even if a rejected claim:

- has a higher threshold;
- has larger slack;

it still cannot serve as an active dominance source.

It must first have a current valid audit state.

---

# 18. Active Evidence Graph

Define the complete proof history graph:

$$
G=(V,E).
$$

Nodes include:

- checkpoints;
- claims;
- audits;
- certificates;
- policies;
- witnesses;
- proposals;
- corrections.

The current theorem actually only depends on one reachable subgraph among them:

$$
\boxed{
G_{\rm live}.
}
$$

---

# 19. Minimal Active Proof Core

Round 14 defines the hot core as retaining at least:

1. scope;
2. root identity;
3. current target / semantic policy;
4. current frontier;
5. current primary active claims;
6. for each primary claim:
   - certificate hash;
   - proved threshold;
   - error budget;
   - worst slack;
   - local dependencies;
   - A1 evidence summary;
7. pending seeds;
8. cold archive root.

This is enough to answer:

> is the current scope theorem-ready?

---

# 20. Cold Evidence Archive

Moved out of hot state:

- rejected claims;
- superseded claims;
- stale claims;
- obsolete proposals;
- old orchestration journal;
- old checkpoints;
- auxiliary duplicate verified claims;
- old scheduler metrics.

They remain:

$$
\boxed{
\text{immutable content-addressed evidence}.
}
$$

---

# 21. The definition of Garbage Collection

This round:

$$
\boxed{
\text{GC}
=
\text{hot-state eviction}.
}
$$

not:

$$
\boxed{
\text{physical deletion}.
}
$$

so users can still:

- query correction ancestry;
- rehydrate old descendants;
- audit historical failures.

---

# 22. Hot-Core Compaction Theorem

## Theorem 22.1

Let the full state:

$$
S
$$

and the compact state:

$$
H
$$

have the same:

1. current scope/root;
2. current semantic policy;
3. current frontier;
4. current active coverage claims;
5. theorem-critical A1 evidence.

Then the current:

$$
\texttt{theorem\_ready}(S)
$$

and:

$$
\texttt{theorem\_ready}(H)
$$

are identical.

### Proof

The theorem-ready predicate only quantifies over the current frontier's obligations.

Whether each obligation closes depends only on the current semantically-compatible active claims and the required verifier evidence.

History —

- rejected;
- superseded;
- obsolete;
- scheduler;

— never appears in the current proof implication.

Therefore moving it to the cold archive does not change the predicate.

Q.E.D.

---

# 23. Archive Merkle Binding

Each object in the cold archive:

$$
o_i
$$

has:

$$
h_i=H(o_i).
$$

Then build:

$$
\boxed{
H_{\rm archive}
=
\operatorname{MerkleRoot}(h_1,\ldots,h_n).
}
$$

The hot core stores:

- the archive manifest hash;
- the archive Merkle root.

---

# 24. Archive does not automatically restore a proof

Even if the cold archive contains a claim that was once verified,

rehydrating it does not automatically make it active.

It must be re-determined:

1. status / supersession;
2. semantic compatibility;
3. current audit requirement;
4. domain relation.

The archive only proves:

> "this was that piece of evidence at the time."

not:

> "it is still valid now."

---

# 25. Rejection after compaction

If a hot active claim:

$$
c
$$

is later rejected:

1. $c$ becomes invalid;
2. the seed becomes pending;
3. theorem-ready is false;
4. the merger can search the cold archive for:
   - old descendant certificates;
   - auxiliary duplicate claims;
5. rehydrate them;
6. semantically validate them;
7. append a new active transition.

So GC does not block recovery.

---

# 26. Reference hot/cold compaction

Source:

the Round 13 final reference checkpoint.

The full source contains:

- active A;
- rejected B-v1;
- active corrected B-v2;
- active C;
- 5 audit records;
- an orchestration race ledger;
- aggregate metadata.

Round 14's hot core retains only:

$$
\boxed{
A,\ B\text{-v2},\ C
}
$$

three active evidence summaries,

plus:

- the frontier;
- the semantic policy;
- the archive binding.

The complete Round 13 source checkpoint moves into an immutable cold archive snapshot.

---

# 27. Archive rehydration test

Round 14 machine test:

1. verify the archive object's SHA-256;
2. read back from the cold snapshot:

   `claim-shard-B-v1`;
3. confirm its historical status remains:

   `REJECTED`;
4. the certificate hash stays consistent.

PASS.

---

# 28. Compaction size note

The reference checkpoint itself is small, so size reduction is not this round's main benchmark.

The difference only matters in production, with millions of history records.

The real invariant is:

$$
\boxed{
|H_{\rm hot}|
\propto
\text{current frontier + active claims}
}
$$

not:

$$
\boxed{
\text{total historical events}.
}
$$

---

# 29. Semantic validator actual test

Round 14's actual tests:

## Baseline

$$
T=0.835,
\quad
e=10^{-8}.
$$

Ready:

`true`.

## Stricter arithmetic + slightly higher target

$$
T=0.8350001,
\quad
e=2\times10^{-8},
$$

plus catalog extension:

$$
B_9.
$$

Ready:

`true`.

## Beyond margin capacity

$$
T=0.8350004,
\quad
e=2\times10^{-8}.
$$

Ready:

`false`.

## Catalog-only extension

With the original target / error, the catalog gains:

- $B_9$;
- the Round 02 Fourier dictionary.

Ready:

`true`.

All PASS.

---

# 30. Round 12 strengthening ledger

Round 12's rule:

`dependency hash mismatch -> stale`

is retained as:

`SAFE-CONSERVATIVE`.

Round 14 adds:

`R12-STRENGTHENING-001`

which states:

> a hash mismatch may proceed into an explicit semantic migration; without a migration proof it is still stale.

So the safety bar has not been lowered.

---

# 31. Semantic Migration Registry

Future checkpoints are recommended to store:

```text
migration_rule_id
source_semantics
target_semantics
preconditions
proof_reference
verifier
```

Only rules in the registry may be used automatically by the canonical merger.

The AI cannot invent a migration ad hoc / verbally.

---

# 32. Registered rules in Round 14

## `TARGET-MONOTONICITY-V0.1`

$$
T'\le T.
$$

## `SCALAR-ERROR-MARGIN-CREDIT-V0.1`

$$
T'+e'
\le T+e+s.
$$

## `WITNESS-CATALOG-SUPERSET-V0.1`

the claim's used witnesses:

$$
\subseteq
$$

the current catalog.

## `ANCESTOR-DOMAIN-COVERAGE-V0.1`

the verified ancestor domain covers the descendant obligation.

---

# 33. What is NOT automatically compatible

- an arbitrary geometry rewrite;
- a new support convention;
- changed reflection semantics;
- changed normalization;
- a different floating-point model without an error implication;
- a witness replaced by a non-equivalent shape;
- a target raised beyond the margin;
- a larger root domain.

These require a new proof.

---

# 34. Hot archive policy

The hot state is recommended to retain:

```text
current checkpoint header
current frontier
pending seeds
primary active claim summaries
active A1 audit refs
unresolved FAIL tombstones
migration registry
cold archive root
```

everything else can be frozen.

---

# 35. Tombstones

If a historical record has moved cold, but the current state still needs to know:

> this claim cannot be revived

hot state only needs to retain a small tombstone:

```text
claim_id
status = REJECTED | SUPERSEDED | STALE-BLOCKED
reason_hash
archive_locator
```

avoiding bringing the full record back to hot.

---

# 36. Proof-State Garbage Collection Safety

May be hot-evicted:

- superseded;
- full bodies of rejected claims;
- old audit details;
- obsolete proposals;
- scheduler events.

May not be hot-evicted without a replacement summary:

- the current active claim;
- the current pending seed;
- the current unresolved FAIL;
- the current semantic policy;
- a migration rule used by an active claim;
- the certificate hash / A1 evidence needed by an active claim.

---

# 37. Physical retention

This round does not address:

- whether the raw certificates can really be deleted after some years;
- storage quota;
- legal retention.

The default is:

$$
\boxed{
\text{archive forever until a separate governance decision}.
}
$$

---

# 38. COMPUTE-DEFERRED

## C14-1

Convert the future global $0.835$ checkpoint to the hot-core format.

## C14-2

Have every claim store margin credit.

## C14-3

Build a migration registry validator.

## C14-4

Seal the cold archive into immutable packs monthly / every N checkpoints.

## C14-5

Build an archive rehydration CLI.

---

# 39. Round 15's assigned topic

## AMRAL-LUC-FC-R15
### Global Proof Capacity and Threshold Ladder Automation

Round 14 obtains, for every claim:

$$
\operatorname{Cap}(c).
$$

The next round can upgrade this into:

> without recomputing all the shards, how far can the current global proof state push the target upward?

For the global frontier:

$$
\boxed{
T_{\rm capacity}
=
\min_{p\in\mathcal P}
\max_{c\text{ covers }p}
\operatorname{Cap}(c).
}
$$

This can automatically:

1. find the bottleneck shards;
2. decide the next target;
3. only recompute the shards that constrain the target;
4. build an adaptive lower-bound ladder.

If global compute has not yet started, first use the reference proof to build a complete capacity-scheduler prototype.

---

# 40. Reproducibility checklist

## Semantic compatibility

`FORMALIZED`

## Scalar margin migration

`PROVED`

## Witness catalog extension

`PROVED`

## Claim dominance

`FORMALIZED`

## Minimal active proof core

`FORMALIZED`

## Hot-core compaction theorem

`PROVED`

## Cold archive binding

`IMPLEMENTED`

## Archive rehydration

`PASS`

## Semantic rebase boundary tests

`PASS`

## Destructive evidence deletion

`NOT AUTHORIZED`

---

# 41. Shortest handoff conclusion

Round 14 resolves two long-running problems.

First:

$$
\boxed{
\text{a hash mismatch}
\not\Rightarrow
\text{necessarily recomputing}.
}
$$

As long as there is an explicit implication, for example:

$$
T'+e'
\le T+e+s,
$$

an old claim can legally undergo semantic rebase.

Second:

$$
\boxed{
\text{proof history can keep growing forever;
the hot checkpoint does not have to}.
}
$$

The current theorem only depends on the Minimal Active Proof Core.

The rest of the evidence moves into a content-addressed cold archive.

So the AMRAL distributed proof state is now not only:

- correct;
- concurrent;
- recoverable;

but also beginning to have:

$$
\boxed{
\text{long-term maintainability}.
}
$$