# AMRAL × Lebesgue Universal Covering — Round 30
## Independent A1 Whole-Shard Replay and Backend Pinning

**Document ID:** AMRAL-LUC-FC-R30  
**Version:** v0.1  
**Date:** 2026-09-20  
**Research status:** Round 30 / Independent whole-shard replay / Backend dependency locking  
**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  
**Prerequisite documents:** AMRAL-LUC-FC-R00 v0.2; R01–R29 v0.1  

---

# 0. This round's summary

Round 29 established the first arithmetic whole-shard prototype:

$$
\text{marker70 upper}
\to
\text{directed root/path}
\to
9278\text{-leaf }B_7\text{ lower tree}.
$$

But still missing:

> a second, genuinely independent, complete lower replay.

Round 30 completes this gate.

## Root / path A1

Starting from the exact value:

$$
T_M=\frac{1673}{2000}
$$

redo the monotone directed bisection, and independently recompute:

$$
t_3,t_5,t_7.
$$

After fixing a verifier script bug — an overly-narrow rational interval that had first been cast to binary64 — all three, against Round 28's directed root:

$$
\boxed{
\text{all overlap PASS}.
}
$$

## Marker70 upper A1

Without using the emitter's scipy candidate constraint reduction, build the exact cyclic polar hull directly from the full set of rational support constraints.

Result:

$$
\boxed{\text{PASS}}.
$$

outer:

$$
0.8349075014501105.
$$

margin:

$$
\boxed{
9.24985499\times10^{-5}.
}
$$

## 9278 lower leaves — full A1

Round 30's second implementation does not use Round 28's:

- `Body.support/contact` candidate generator;
- SciPy convex-hull candidate reduction;
- Round 28 density decisions;
- Round 28's Fraction hull code.

Instead it uses:

1. the defining-disk representation;
2. direct intersection-of-disks support candidates for each direction;
3. a union support winner;
4. fixed-grid integer rationalization;
5. an exact integer monotone hull;
6. directed defining-disk membership;
7. exact integer/rational area comparison.

Result:

$$
\boxed{
9278/9278\text{ A1-PASS}.
}
$$

inconclusive:

$$
\boxed{0}.
$$

The second verifier's thinnest leaf margin:

$$
\boxed{
3.54237075\times10^{-9}>0.
}
$$

path:

```text
11010110100110101001110111
```

This differs from Round 28 emitter's thinnest leaf.

So the independent verifier does change the finite inner polygon and the margin ordering, but the whole tree is still complete.

This round therefore raises the marker70/B7 shard to:

$$
\boxed{
\texttt{A1-VERIFIED-PINNED-PROTOTYPE-SHARD}.
}
$$

But it is still not raised to:

`PUBLICATION-CANDIDATE`.

Reason:

> although the two implementations are independent, they still share the same mpmath.iv/libmp directed arithmetic backend.

The backend is already source/version pinned, but backend trust independence is not yet complete.

Therefore:

$$
\boxed{
a_{\mathrm{Leb}}\ge0.835
\text{ remains NOT CERTIFIED}.
}
$$

---

# 1. A1 means implementation independence

Round 30 draws a clear distinction between:

## Implementation A1

The second verifier does not share:

- candidate generation;
- convex-hull reduction;
- density selection;
- the pass/fail ledger.

## Backend independence

Whether the second verifier uses a different, correctly-rounded arithmetic engine.

This round closes the first item.

The second item remains OPEN.

---

# 2. Independent lower candidate geometry

Round 28's emitter took common-core boundary candidates from the piecewise support/contact representation.

Round 30 instead generates support candidates directly from the defining disks:

$$
G=\bigcap_jD(V_j,\rho)
$$

For a unit direction:

$$
u,
$$

each disk has a candidate:

$$
V_j+\rho u.
$$

If the candidate lies within all of the defining disks, it is a legal arc candidate for the intersection boundary.

---

# 3. Corner candidates

The circle-circle intersections of two defining circles:

$$
\partial D(V_i,\rho),
\qquad
\partial D(V_j,\rho)
$$

are also core boundary candidates, if they lie within all of the defining disks at the same time.

Round 30 independently enumerates these points.

---

# 4. Support candidate selection

For each direction $u$:

- arc candidates;
- valid circle intersections;

take:

$$
\boxed{
p_G(u)
=
\arg\max_{p\in\text{candidate set}}
u\cdot p.
}
$$

This path does not depend on Round 28's `Body.piece/contact` implementation.

---

# 5. Union winner

For:

$$
D,G_3,G_5,G_7
$$

obtain a candidate for each:

$$
p_i(u).
$$

then select:

$$
\boxed{
p(u)
=
\arg\max_i u\cdot p_i(u).
}
$$

Apply a minimal perturbation toward the interior, then quantize onto a fixed rational grid:

$$
10^{-17}\mathbb Z^2.
$$

Candidate generation is still not a premise of the proof.

---

# 6. Independent exact hull

Round 30 does not call SciPy's ConvexHull to determine the final rational polygon.

For the integer-grid points:

$$
(X_i,Y_i)\in\mathbb Z^2
$$

it builds the monotone hull directly using the exact integer orientation predicate:

$$
\operatorname{orient}(a,b,c)
=
(b-a)\times(c-a)
$$

So the convex ordering is entirely independent of the emitter.

---

# 7. Directed point membership

For the final integer-grid hull vertices:

- disk:
  an exact integer check;
- Reuleaux common cores:
  directed center rectangles + a radius lower bound;
- require:
  $$
  D_{\max}^2<\rho_{\rm lo}^2.
  $$

Any membership uncertainty:

`A1-INCONCLUSIVE`.

This round:

$$
\boxed{0}.
$$

---

# 8. Exact A1 area

Fix the grid denominator:

$$
Q=10^{17}.
$$

The polygon's shoelace numerator is an exact integer.

area:

$$
A
=
\frac{|S|}{2Q^2}.
$$

This is compared against:

$$
\frac{167}{200}
$$

directly by integer cross-multiplication.

There is no floating-point acceptance anywhere.

---

# 9. Full lower replay result

Total leaves:

$$
9278.
$$

A1 PASS:

$$
\boxed{9278}.
$$

A1 inconclusive:

$$
\boxed{0}.
$$

---

# 10. A1 density distribution

The second verifier's density:

## 512

$$
8174
$$

leaves.

## 1024

$$
869.
$$

## 2048

$$
163.
$$

## 4096

$$
56.
$$

## 8192

$$
12.
$$

## 16384

$$
4.
$$

Round 30 has no leaf that requires 32768.

This is noticeably different from Round 28's density distribution, further showing that the two finite-certificate generators are not the same.

---

# 11. A different weakest leaf

Round 28 emitter's minimum rational margin: about:

$$
3.1949\times10^{-8}.
$$

Round 30 A1's minimum:

$$
\boxed{
3.5424\times10^{-9}.
}
$$

corresponding to a different path.

This does not mean Round 30 is closer to the true hull minimum.

It only means that different inner-polygon approximations carry different losses.

What matters is:

$$
\boxed{
\min A_{\rm A1}>\frac{167}{200}.
}
$$

---

# 12. Root A1 verifier bug

The first root A1 audit incorrectly reported that:

$$
t_3,t_5,t_7
$$

were all non-overlapping.

The cause was not a mathematical contradiction.

It was a script bug:

> an exact rational $d_\star$ interval about $10^{-64}$ wide was first cast to binary64.

This directly perturbed the interval's position to the $10^{-17}$ level.

Round 30 correction:

`R30-A1-ROOT-001`.

After the fix:

- exact decimal rational endpoints;
- directed tmax;

all three:

$$
\boxed{\text{overlap PASS}.}
$$

---

# 13. Why this bug is useful

It proves that:

> the arithmetic verifier itself must also be audited.

Writing the word `interval` does not by itself make it sound.

In particular:

$$
\boxed{
\text{exact}\to\text{float}\to\text{interval}
}
$$

is not directed arithmetic.

This kind of implicit narrowing/collapse must be forbidden.

---

# 14. Backend pinning

Round 30 locks down:

- the Python interpreter version;
- the mpmath version;
- the hash of the entire mpmath Python-source package;
- the hash of every `libmp/*.py` file;
- the `fractions.py` hash;
- the A1 verifier script hashes.

backend identity:

$$
\boxed{
\texttt{PINNED-MPMATH-LIBMP-PROTOTYPE-v0.1}.
}
$$

---

# 15. What pinning means

Pinning guarantees:

> a future replay will know exactly which set of source bytes was used.

It does not automatically guarantee:

> that the backend implementation has been proven correctly rounded by an independent audit.

So:

$$
\boxed{
\text{reproducibility}
\ne
\text{backend trust proof}.
}
$$

---

# 16. Backend trust state

Currently:

$$
\boxed{
\texttt{PINNED-REPRODUCIBLE-PROTOTYPE}
}
$$

but:

$$
\boxed{
\texttt{TRUST-AUDIT-OPEN}.
}
$$

So Round 29's originally planned:

`PUBLICATION-CANDIDATE-SHARD`

is still not granted.

---

# 17. Whole-shard A1 state

marker70/B7:

## Root/path

A1 PASS.

## Marker upper

A1 PASS.

## B7 lower

$$
9278/9278
$$

A1 PASS.

## Arithmetic backend

PINNED.

## Independent backend trust

OPEN.

So:

$$
\boxed{
\texttt{A1-VERIFIED-PINNED-PROTOTYPE-SHARD}.
}
$$

---

# 18. Status lattice

Round 30 fixes:

## `ARITHMETICALLY-CLOSED-PROTOTYPE`

single-implementation upper/lower PASS.

## `A1-VERIFIED-PINNED-PROTOTYPE`

second-implementation replay PASS + backend source pinned.

## `PUBLICATION-CANDIDATE`

further requires:

- a backend trust audit;
- or an independent, second, correctly-rounded backend cross-replay.

## `THEOREM-READY`

further requires:

- the global atlas / root / all shards to be current;
- independent merge;
- no pending obligations.

---

# 19. Marker-upper scope

Round 29 already achieved:

$$
77/77
$$

marker-emitter arithmetic PASS.

Round 30's whole-shard gate only needs marker70's A1, which already PASSes.

When Round 30 attempted to extend this to the full 77-marker A1, the high-density markers made interactive batch computation very costly.

So the full 77-marker A1 is not this round's gate.

Production can replay them in shards; this does not affect marker70 whole-shard's local A1 status.

---

# 20. Global geometry state unchanged

Round 30's arithmetic work does not change the geometric closure ledger.

The latest complete common-budget remains:

$$
\boxed{
51/77\text{ at }d=36.
}
$$

Known higher-budget strict closures remain at least:

$$
\Gamma_{B7}(38)\ge57,
$$

$$
\Gamma_{B7}(40)\ge63.
$$

Arithmetic A1 success must not be treated as global geometry completion.

---

# 21. What remains before publication-candidate shard

The local shard now has essentially one thing left:

$$
\boxed{
\text{backend trust independence}.
}
$$

Candidate paths:

1. replay the directed geometry using MPFR/MPFI;
2. replay using Arb ball arithmetic;
3. use a formally audited interval kernel;
4. carry out an independent proof/audit of the current libmp rounding primitives.

Only once a second backend can replay:

- the root;
- the marker upper;
- the 9278 lower-membership checks;

and equally PASS, should marker70/B7 be raised to:

$$
\boxed{\texttt{PUBLICATION-CANDIDATE-SHARD}.}
$$

---

# 22. Round 31

## Cross-Backend Arithmetic Replay and Bulk Shard Migration

Next round's priorities:

1. check whether the environment can stand up an MPFR/Arb-class second backend;
2. if it can:
   - a marker70 whole-shard cross-backend replay;
3. if it cannot:
   - reduce the interval-primitive reduction to smaller rational bounds;
   - reduce the trust surface exposed to the transcendental backend;
4. simultaneously begin batch Round28/29-style migration for other geometry-complete cells;
5. turn the full 77-marker A1 into sharded, async-style proof jobs;
6. continue advancing the global geometry residual independently.

---

# 23. Shortest handoff

What Round 30 truly closes:

$$
\boxed{
\text{whole-shard independent implementation replay}.
}
$$

marker70/B7:

$$
\boxed{
\text{root PASS}
+
\text{upper PASS}
+
9278/9278\text{ lower PASS}.
}
$$

And the second lower verifier uses a different finite-geometry algorithm.

So the local shard now has exactly one clear arithmetic-trust gap left:

$$
\boxed{
\text{same backend}
\ne
\text{independent backend}.
}
$$

So the most accurate current status is:

$$
\boxed{
\texttt{A1-VERIFIED-PINNED-PROTOTYPE-SHARD}
}
$$

and not a publication theorem.

Globally, it remains the case that:

$$
\boxed{
a_{\mathrm{Leb}}\ge0.835
\text{ NOT CERTIFIED}.
}
$$