# AMRAL × Lebesgue Universal Covering — Round 31
## Cross-Backend Arithmetic Replay and First Publication-Candidate Shard

**Document ID:** AMRAL-LUC-FC-R31  
**Version:** v0.1  
**Date:** 2026-09-20  
**Research status:** Round 31 / MPFR cross-backend replay / Local publication-candidate promotion  
**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–R30 v0.1  

---

# 0. Round summary

Round 30 already completed implementation-level A1 for the marker70/$B_7$ whole shard:

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

But the two verifiers still shared:

`mpmath.iv / libmp`.

Round 31 finds a second, system-level backend:

$$
\boxed{\text{libMPFR 4.2.2 + GMP}}
$$

and builds a minimal directed-rounding wrapper directly on the C ABI / `ctypes`.

This round re-verifies:

## MPFR root

$$
\boxed{
t_3,t_5,t_7
\text{ all overlap PASS against the Round 28 directed intervals}.
}
$$

## MPFR marker70 upper

$$
\boxed{
U_{70}^{\rm MPFR}
=
0.8349075014501105
<
0.835.
}
$$

margin:

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

## MPFR full lower tree

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

inconclusive:

$$
\boxed{0}.
$$

minimum exact rational lower margin:

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

So the marker70/$B_7$ whole shard now has:

1. an emitter implementation;
2. an independent A1 implementation;
3. an mpmath/libmp backend;
4. an independent libMPFR/GMP backend;
5. strict upper/lower inequalities that all pass.

Therefore the local shard status is upgraded to:

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

Note:

$$
\boxed{
\text{publication-candidate shard}
\ne
\text{global theorem}.
}
$$

globally:

$$
a_{\mathrm{Leb}}\ge0.835
$$

is still not certified.

---

# 1. Second arithmetic backend

The environment does not have:

- gmpy2;
- python-flint;
- an Arb Python binding.

But the system's dynamic libraries include:

$$
\boxed{\texttt{libmpfr.so.6}}
$$

and:

$$
\boxed{\texttt{libgmp.so.10}}.
$$

Round 31 calls the C ABI directly.

---

# 2. Minimal MPFR trust surface

The wrapper exposes only what the current proof actually needs:

- exact integer / rational load;
- RNDD / RNDU;
- add/sub/mul/div;
- sqrt;
- sin;
- cos;
- acos;
- atan2;
- pi;
- comparison;
- exact dyadic endpoint extraction.

The whole CAS is not treated as a proof dependency.

---

# 3. Fraction → MPFR → Fraction rule

Round 30 already discovered that:

$$
\text{exact rational}
\to
\text{binary64}
\to
\text{interval}
$$

destroys ultra-narrow intervals.

Round 31 fixes this as:

$$
\boxed{
\text{exact Fraction}
\to
\text{MPFR directed}
\to
\text{exact dyadic Fraction}.
}
$$

Any transcendental endpoint is retrieved in full as an MPFR dyadic value.

---

# 4. MPFR root replay

Starting again from:

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

monotone directed bisection is performed.

This gives a $d_\star$ interval width of about:

$$
2.97\times10^{-67}.
$$

Then recomputing:

$$
t_3,t_5,t_7.
$$

all three overlap with the Round 28 mpmath/libmp intervals:

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

---

# 5. MPFR marker upper

marker70 still uses:

- an exact rational marker point;
- finite integer normals;
- a rational half-plane outer polygon;
- an exact rational polar hull / line intersections / shoelace.

The only thing replaced:

> All of the directed transcendental arithmetic for the Reuleaux support sector is recomputed entirely by MPFR.

Result:

$$
\boxed{
0.8349075014501105
}
$$

which agrees with the value displayed in Round 29.

---

# 6. Initial conservative marker false negative

The first version of the MPFR marker verifier additionally included adjacent Reuleaux pieces outside the active sector as extra upper candidates.

This is still a one-sided safe upper bound,

but excessively loose:

$$
U\approx0.9201.
$$

So the marker fails to pass.

This is not a false proof,

only a false negative / inconclusive result.

Fix:

> Only include pieces that can genuinely be active within the directed sector interval.

After the fix, the exact outer certificate PASSes.

Logged as:

`R31-MPFR-MARKER-001`.

---

# 7. MPFR lower replay semantics

Round 31's full lower verifier uses:

- the MPFR-reconstructed root;
- explicit topology;
- explicit witness split axes;
- defining-disk common-core geometry;
- an independent support-candidate generator;
- fixed-grid integer rationalization;
- an exact integer monotone hull;
- exact rational area comparison.

Acceptance is still:

$$
A_{\rm rational}
>
\frac{167}{200}.
$$

---

# 8. Full MPFR lower result

Total leaves:

$$
9278.
$$

PASS:

$$
\boxed{9278}.
$$

inconclusive:

$$
\boxed{0}.
$$

---

# 9. MPFR density distribution

$$
512:8174,
$$

$$
1024:869,
$$

$$
2048:163,
$$

$$
4096:56,
$$

$$
8192:12,
$$

$$
16384:4.
$$

This is the same density histogram obtained by the Round 30 A1 implementation.

That is because the finite candidate policy is the same,

but the core enclosure arithmetic backend is different.

---

# 10. Minimum MPFR margin

Thinnest:

```text
11010110100110101001110111
```

margin:

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

Still strictly positive.

---

# 11. Cross-backend theorem state

The same local shard now has:

## Backend A

`mpmath.iv / libmp`

Round 28 emitter + Round 30 A1.

## Backend B

`libMPFR 4.2.2 / GMP`

Round 31 full replay.

Both sides independently prove:

- the root;
- the marker upper bound;
- every lower leaf.

So a backend-specific silent rounding defect would have to simultaneously produce compatible errors in two different arithmetic stacks — credibility is substantially raised.

This is still not a formal proof of the two libraries,

but it satisfies the publication-candidate cross-backend gate as defined by this program.

---

# 12. MPFR backend pin

Round 31 pins:

## MPFR

resolved ELF:

```text
/usr/lib/x86_64-linux-gnu/libmpfr.so.6.2.2
```

SHA-256:

```text
4e3ccf5b442fc91054b0153140fe62939009f98ca1367f45de62376d5b18d28c
```

## GMP

```text
/usr/lib/x86_64-linux-gnu/libgmp.so.10.5.0
```

SHA-256:

```text
d15e1585c6c267296459570c8ac217ca9123044bcd4e896d2f686b32333445d2
```

The wrapper and the replay scripts are also all content-hashed.

---

# 13. Publication-candidate gate

Round 31 defines, locally:

`PUBLICATION-CANDIDATE-SHARD`

Conditions:

1. directed root/path two-backend replay;
2. upper marker two-backend replay;
3. lower-tree independent implementation A1;
4. lower-tree independent arithmetic-backend replay;
5. every claimed inequality is strict;
6. dependency hashes pinned.

marker70/B7:

$$
\boxed{
\text{ALL LOCAL CONDITIONS MET}.
}
$$

---

# 14. What publication-candidate means

It means:

> This individual shard has now reached a maturity level ready to enter a formal proof package / external audit.

It does not mean:

> that the Lebesgue lower bound has been proved.

because the global theorem still needs coverage of all root/base/shard obligations.

---

# 15. Global geometry still incomplete

Latest common budget:

$$
\Gamma_{B_7}(36)=51/77.
$$

Known higher budgets:

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

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

There is still a geometry residual.

So a publication-candidate shard cannot change the global theorem status.

---

# 16. Bulk arithmetic migration queue

Round 31 splits the full-atlas cells into:

## Geometry complete

enters the:

$$
\boxed{
\text{ARITHMETIC-MIGRATION QUEUE}.
}
$$

For each one, in order:

1. explicit topology / axis streams;
2. directed root/path;
3. marker upper;
4. bulk lower migration;
5. implementation A1;
6. MPFR cross-backend;
7. publication-candidate promotion.

## Geometry residual

continues the:

$$
B_7
$$

closure wave.

Full arithmetic-migration cost should not be spent while the lift tree is not yet complete.

---

# 17. Migration economics

Round 28 / 30 / 31 have already shown:

> arithmetic migration itself has not caused any geometry resplit.

For marker70:

$$
\boxed{
0\text{ leaves require resplit}.
}
$$

So it is currently reasonable to conjecture:

> most geometry-complete shards that already carry a thicker margin can be bulk-migrated directly.

But this is only an engineering hypothesis,

and it must be verified shard by shard.

---

# 18. Cross-backend scope boundary

Round 31 does not claim:

> that the MPFR implementation is formally verified.

The real mathematical certificate still rests on a software trust base.

Current approach:

1. shrink the trust surface;
2. pin source/binary;
3. use different libraries;
4. use different implementations;
5. strict rational final comparisons.

This is a practical computer-assisted-proof architecture,

not foundational formal verification.

---

# 19. Current local status lattice

marker70/B7:

`REFERENCE-COMPLETE`

↓

`ARITHMETICALLY-CLOSED-PROTOTYPE`

↓

`A1-VERIFIED-PINNED-PROTOTYPE`

↓

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

But globally:

$$
\boxed{
\texttt{THEOREM-READY=false}.
}
$$

---

# 20. Correction ledger

## R31-MPFR-MARKER-001

overly broad active-sector candidate set caused safe false-negative marker upper.

fixed.

## R31-BACKEND-LOCK-001

first ldconfig parsing helper generated an invalid `/` path and failed before manifest generation.

fixed; no mathematical effect.

---

# 21. Round 32

## Bulk Publication-Candidate Migration and Global Residual Closure

The next round begins with two teams working in parallel:

### Arithmetic team

Takes the next, cheapest batch of cells from the geometry-complete queue,

and in bulk performs:

- Round28 lower migration;
- Round29 marker upper;
- Round30 A1;
- Round31 MPFR cross-backend.

Tallies:

$$
\boxed{
\text{publication-candidate coverage fraction}.
}
$$

### Geometry team

Chases only the still-residual cells,

completing a new common-budget:

$$
d=40,\ 42,\ldots
$$

closure wave.

Ultimate goal:

> geometry coverage and publication-candidate arithmetic coverage begin to converge on the same atlas.

---

# 22. Shortest handoff

Round 31 closes the marker70 shard's last local arithmetic-redundancy gate:

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

So:

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

now reasonably holds at local shard scope.

The main question going forward is no longer:

> Can this one shard be rigorously replayed?

but rather:

$$
\boxed{
\text{Can this level of maturity be spread, in bulk, to all final shards}.
}
$$

The global theorem still stands at:

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