# AMRAL × Lebesgue Universal Covering — Round 05
## Global Candidate-Cell Branch-and-Bound and the Saturation Gate

**Document ID:** AMRAL-LUC-FC-R05  
**Version:** v0.1  
**Date:** 2026-09-18  
**Research status:** Round 05 / Formal push / Saturation theory  
**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  
**Parent methodology:** Relational Constraint–Handoff Methodology (RCHM)  
**Prerequisite documents:** AMRAL-LUC-FC-R00 v0.2; R01–R04 v0.1

---

# 0. Round Summary and Verdict

Rounds 01–04 have already completed the three-layer finite-resolution compiler:

$$
\text{target}
\to
\text{placement}
\to
\text{candidate cover}.
$$

So Round 05 no longer asks:

> Can it be made finite?

but instead asks:

$$
\boxed{
\text{When can a finite hierarchy actually stop at a finite level?}
}
$$

This round arrives at six core conclusions.

---

## Conclusion A: Convergence Does Not Equal Finite Saturation

If we only have:

$$
L_n\uparrow L
$$

or:

$$
U_n\downarrow U,
$$

together with an explicit error:

$$
\varepsilon_n\to0,
$$

this does not imply:

$$
\exists n_\star:
L_{n_\star}=L.
$$

Therefore:

$$
\boxed{
\text{finite-resolution convergence}
\not\Rightarrow
\text{finite exact closure}.
}
$$

Round 04's polygon hierarchy and the Zeng-type finite hierarchy must both separately address the question of whether finite attainment holds.

---

## Conclusion B: The Finite Hard-Witness Family Is a Complete Lower-Bound Language

For a finite:

$$
\mathcal F
=
\{K_1,\ldots,K_m\}
$$

define:

$$
\boxed{
\Lambda(\mathcal F)
=
\min_{g_1,\ldots,g_m\in E(2)}
\operatorname{Area}
\left(
\operatorname{conv}
\bigcup_{i=1}^m
g_iK_i
\right).
}
$$

Then:

$$
\Lambda(\mathcal F)
\le
a_{\mathrm{Leb}}.
$$

More importantly:

$$
\boxed{
a_{\mathrm{Leb}}
=
\sup_{\mathcal F\ \mathrm{finite}}
\Lambda(\mathcal F).
}
$$

So finite witness families are complete in the limit.

---

## Conclusion C: Establishing the Finite-Witness Cardinality Hierarchy

Let:

$$
\lambda_m
$$

be the best finite-witness lower bound obtainable among all sets of at most $m$ unit constant-width witnesses.

Then:

$$
\boxed{
\lambda_1
\le
\lambda_2
\le
\cdots
\le
a_{\mathrm{Leb}},
}
$$

and:

$$
\boxed{
\lambda_m
\to
a_{\mathrm{Leb}}.
}
$$

Every level:

$$
\lambda_m
$$

attains its maximum.

---

## Conclusion D: No False Permanent Saturation

If:

$$
\lambda_m
<
a_{\mathrm{Leb}},
$$

then there exists:

$$
m'>m
$$

such that:

$$
\boxed{
\lambda_{m'}
>
\lambda_m.
}
$$

So the finite-witness hierarchy can never permanently plateau below the true value.

If it appears stuck, that means either:

- witnesses capable of excluding every current minimizer have not yet been found; or
- exact saturation has genuinely already been reached.

---

## Conclusion E: The Stopping Condition for Exact Finite Saturation Collapses to a Single Matching Certificate

If there exists a finite witness family:

$$
\mathcal F_\star
$$

and a universal cover:

$$
U_\star
$$

such that:

$$
\boxed{
\Lambda(\mathcal F_\star)
=
\operatorname{Area}(U_\star)
=
A_\star,
}
$$

then:

$$
\boxed{
a_{\mathrm{Leb}}
=
A_\star.
}
$$

This is the project's exact finite saturation criterion.

---

## Conclusion F: Candidate-Cell Branch-and-Bound Has Safe Pruning Rules

Every support cell has:

1. an outer-polygon non-universality prune;
2. a cell area lower-bound prune;
3. recursive refinement;
4. an eventual-prune theorem for cells that are strictly non-universal or strictly suboptimal.

As a result, the hierarchy's active cells progressively concentrate on:

$$
\boxed{
W(U)=0
}
$$

and on the frontier where the area approaches the optimum.

---

This round's overall determination:

$$
\boxed{
\text{SATURATION GATE: FORMALIZED}
}
$$

but:

$$
\boxed{
\text{FINITE ATTAINMENT: OPEN}
}
$$

---

# 1. Why Convergence Alone Is Not Enough

Consider the simplest finite-grid approximation:

$$
x_n
=
\frac{\lfloor n\alpha\rfloor}{n},
$$

where:

$$
\alpha
$$

is an irrational number.

Then:

$$
x_n\to\alpha,
$$

but in general:

$$
x_n\neq\alpha
$$

for every finite:

$$
n.
$$

So from:

$$
|x_n-\alpha|
\to0
$$

one cannot infer:

$$
\exists n:
x_n=\alpha.
$$

The geometric hierarchy is no different.

Even if:

$$
A^{\mathrm{poly}}_{M,q}
-
\beta_{M,q}
\le
a_{\mathrm{Leb}}
\le
A^{\mathrm{poly}}_{M,q},
$$

and:

$$
\beta_{M,q}\to0,
$$

this alone still cannot establish that some finite:

$$
(M,q)
$$

has already achieved exact equality.

Round 05 therefore formally separates:

$$
\boxed{
\text{convergence}
}
$$

from:

$$
\boxed{
\text{finite attainment}.
}
$$

---

# 2. Finite witness lower functional

Let:

$$
\mathcal W_1^0
$$

be Round 01's centered unit constant-width target family.

Let:

$$
D
=
B_{1/2}(0)
$$

be the unit-diameter disk.

Consider a finite family:

$$
\mathcal F
=
\{D,K_2,\ldots,K_m\},
\qquad
K_i\in\mathcal W_1^0.
$$

Define:

$$
\boxed{
\Lambda(\mathcal F)
=
\inf_{g_1,\ldots,g_m\in E(2)}
\operatorname{Area}
\left(
\operatorname{conv}
\bigcup_i g_iK_i
\right).
}
$$

Since the same isometry can be applied to the whole configuration jointly, the disk may be fixed:

$$
g_1D=D.
$$

---

# 3. Finite witness lower bound theorem

## Theorem 3.1

For any finite:

$$
\mathcal F,
$$

we have:

$$
\boxed{
\Lambda(\mathcal F)
\le
a_{\mathrm{Leb}}.
}
$$

### Proof

Take any universal cover:

$$
U.
$$

For every:

$$
K_i\in\mathcal F,
$$

there exists:

$$
g_i\in E(2)
$$

such that:

$$
g_iK_i
\subseteq
U.
$$

Since:

$$
U
$$

is convex:

$$
\operatorname{conv}
\bigcup_i g_iK_i
\subseteq
U.
$$

Therefore:

$$
\operatorname{Area}(U)
\ge
\operatorname{Area}
\left(
\operatorname{conv}
\bigcup_i g_iK_i
\right)
\ge
\Lambda(\mathcal F).
$$

Taking the infimum over universal covers:

$$
a_{\mathrm{Leb}}
\ge
\Lambda(\mathcal F).
$$

Q.E.D.

---

# 4. The Minimum of $\Lambda(\mathcal F)$ Is Attained

Round 05 does not want to quietly treat:

$$
\inf
$$

as a:

$$
\min
$$

without establishing attainment.

Given a known universal-cover upper bound:

$$
\bar A,
$$

a finite family:

$$
\mathcal F
$$

can always be jointly accommodated by some universal cover of area:

$$
\le\bar A.
$$

So when computing:

$$
\Lambda(\mathcal F)
$$

one may restrict to the candidate class:

$$
\mathcal C_{\bar A}.
$$

Round 04 already proved:

$$
\mathcal C_{\bar A}
$$

is compact.

For a fixed target:

$$
K,
$$

the set:

$$
\mathcal C(K)
=
\{U\in\mathcal C_{\bar A}:K\text{ fits in }U\}
$$

is closed.

Therefore:

$$
\bigcap_{K\in\mathcal F}
\mathcal C(K)
$$

is a nonempty compact set.

The area functional is continuous with respect to Hausdorff convergence of convex bodies, so there exists:

$$
U_{\mathcal F}
$$

such that:

$$
\operatorname{Area}(U_{\mathcal F})
=
\min
\left\{
\operatorname{Area}(U):
U\text{ covers every }K\in\mathcal F
\right\}.
$$

The convex hull of any placement is itself a cover; conversely every cover contains the placement hull.

Hence:

$$
\boxed{
\Lambda(\mathcal F)
=
\min
\left\{
\operatorname{Area}(U):
U\text{ covers }\mathcal F
\right\}.
}
$$

So:

$$
\boxed{
\inf
\text{ can be promoted to }
\min.
}
$$

---

# 5. Fit-set closedness

This is a necessary interface for the compactness argument that follows.

## Theorem 5.1

For a fixed compact target $K$:

$$
\mathcal C(K)
=
\{U\in\mathcal C_{\bar A}:K\text{ fits in }U\}
$$

is closed in the Hausdorff topology.

### Proof

Let:

$$
U_n\to U
$$

with every:

$$
U_n
$$

able to accommodate:

$$
g_nK.
$$

By Round 04:

$$
U_n
\subseteq
B_R
$$

uniformly bounded.

So:

$$
g_nK
\subseteq
B_R.
$$

The rotation/reflection component lies in the compact:

$$
O(2).
$$

The translation component is bounded because $g_nK$ is bounded.

So a subsequence can be taken:

$$
g_{n_j}\to g.
$$

From:

$$
g_{n_j}K
\subseteq
U_{n_j}
$$

together with Hausdorff convergence, we obtain:

$$
gK\subseteq U.
$$

Q.E.D.

---

# 6. Finite-witness completeness theorem

## Theorem 6.1

$$
\boxed{
a_{\mathrm{Leb}}
=
\sup_{\mathcal F\subset\mathcal W_1^0,\ \mathcal F\ finite,\ D\in\mathcal F}
\Lambda(\mathcal F).
}
$$

### First direction

By Theorem 3.1:

$$
\Lambda(\mathcal F)
\le
a_{\mathrm{Leb}}
$$

holds for every finite family.

So:

$$
\sup_{\mathcal F\ finite}
\Lambda(\mathcal F)
\le
a_{\mathrm{Leb}}.
$$

---

### Second direction

Suppose for contradiction there exists:

$$
A
<
a_{\mathrm{Leb}}
$$

such that:

$$
\Lambda(\mathcal F)
\le A
$$

holds for every finite:

$$
\mathcal F.
$$

Consider the compact candidate class:

$$
\mathcal C_A
=
\left\{
U:
\begin{array}{l}
B_{1/2}(0)\subseteq U,\\
U\text{ compact convex},\\
\operatorname{Area}(U)\le A
\end{array}
\right\}.
$$

If:

$$
A<\frac{\pi}{4},
$$

then not even the disk fits, and a contradiction is immediate.

So it suffices to take:

$$
A\ge\frac{\pi}{4}.
$$

For each:

$$
K\in\mathcal W_1^0,
$$

define the closed set:

$$
S_K
=
\{U\in\mathcal C_A:K\text{ fits in }U\}.
$$

Suppose every finite:

$$
K_1,\ldots,K_m
$$

satisfies:

$$
\Lambda(\{D,K_1,\ldots,K_m\})\le A.
$$

Then:

$$
S_{K_1}\cap\cdots\cap S_{K_m}
\neq\varnothing.
$$

So the family:

$$
\{S_K\}_{K\in\mathcal W_1^0}
$$

has the finite intersection property.

Since:

$$
\mathcal C_A
$$

is compact, it follows that:

$$
\bigcap_{K\in\mathcal W_1^0}
S_K
\neq\varnothing.
$$

That is, there exists:

$$
U\in\mathcal C_A
$$

that accommodates all unit constant-width targets.

By Round 01's constant-width reduction, $U$ is a Lebesgue universal cover.

Therefore:

$$
a_{\mathrm{Leb}}
\le
A,
$$

contradicting:

$$
A<a_{\mathrm{Leb}}.
$$

So for any:

$$
A<a_{\mathrm{Leb}},
$$

there exists a finite:

$$
\mathcal F
$$

such that:

$$
\Lambda(\mathcal F)>A.
$$

Therefore:

$$
\sup_{\mathcal F\ finite}
\Lambda(\mathcal F)
\ge
a_{\mathrm{Leb}}.
$$

Q.E.D.

---

# 7. Finite-witness cardinality hierarchy

Define:

$$
\boxed{
\lambda_m
=
\sup
\left\{
\Lambda(\mathcal F):
D\in\mathcal F,
\ |\mathcal F|\le m
\right\}.
}
$$

Then clearly:

$$
\lambda_m
\le
\lambda_{m+1}
\le
a_{\mathrm{Leb}}.
$$

By Theorem 6.1:

$$
\boxed{
\lim_{m\to\infty}\lambda_m
=
a_{\mathrm{Leb}}.
}
$$

---

# 8. Every $\lambda_m$ Is Attained

To promote:

$$
\sup
$$

to:

$$
\max,
$$

consider the target tuple:

$$
(K_1,\ldots,K_m)
\in
(\mathcal W_1^0)^m
$$

where:

$$
K_1=D.
$$

Round 01 already proved:

$$
\mathcal W_1^0
$$

is compact.

What must be proved is that:

$$
\Lambda(K_1,\ldots,K_m)
$$

is continuous in the tuple.

---

# 9. Uniform Continuity of the Finite-Witness Value

Suppose:

$$
d_H(K_i,L_i)
\le
\varepsilon
$$

for every:

$$
i.
$$

Let:

$$
U_K
$$

be the optimal finite-family cover for the $K$-tuple.

Since the family contains the disk, we may anchor it:

$$
B_{1/2}(0)\subseteq U_K.
$$

and:

$$
\operatorname{Area}(U_K)
\le
\bar A.
$$

Round 04 gives:

$$
U_K\subseteq B_R,
\qquad
R=2\bar A.
$$

Using the optimal placements of the $K_i$:

$$
g_iK_i\subseteq U_K.
$$

By the Hausdorff distance:

$$
g_iL_i
\subseteq
g_iK_i+\varepsilon B
\subseteq
U_K+\varepsilon B.
$$

So:

$$
\Lambda(L_1,\ldots,L_m)
\le
\operatorname{Area}(U_K+\varepsilon B).
$$

By the Steiner formula:

$$
\operatorname{Area}(U_K+\varepsilon B)
=
\Lambda(K_1,\ldots,K_m)
+
\varepsilon\operatorname{Per}(U_K)
+
\pi\varepsilon^2.
$$

And:

$$
\operatorname{Per}(U_K)
\le
2\pi R
=
4\pi\bar A.
$$

So:

$$
\Lambda(L)
-
\Lambda(K)
\le
4\pi\bar A\varepsilon
+
\pi\varepsilon^2.
$$

Exchanging $K,L$:

$$
\boxed{
|\Lambda(K)-\Lambda(L)|
\le
4\pi\bar A\varepsilon
+
\pi\varepsilon^2.
}
$$

Hence:

$$
\Lambda
$$

is continuous on the compact product target space.

So:

$$
\boxed{
\lambda_m
\text{ is attained for every finite }m.
}
$$

We may write:

$$
\lambda_m
=
\max_{|\mathcal F|\le m}
\Lambda(\mathcal F).
$$

---

# 10. Where the Known Published Lower Bound Sits in This Ladder

For:

$$
m=1,
$$

there is only the disk witness:

$$
D=B_{1/2},
$$

so:

$$
\boxed{
\lambda_1
=
\frac{\pi}{4}
\approx
0.7853981634.
}
$$

Mishra 2026 uses the finite constant-width family:

- disk;
- Reuleaux triangle;
- Reuleaux pentagon;

obtaining the strict lower bound:

$$
0.8344.
$$

So at minimum we may record:

$$
\boxed{
\lambda_3
\ge
0.8344.
}
$$

This does not mean:

$$
\lambda_3=0.8344.
$$

The Mishra result only supplies the certified lower contribution of that finite family.

Currently Gibbs has proved:

$$
a_{\mathrm{Leb}}
\le
0.8440935944.
$$

So the publicly known squeeze is at least:

$$
0.8344
\le
a_{\mathrm{Leb}}
\le
0.8440935944.
$$

Gap:

$$
\boxed{
0.0096935944.
}
$$

---

# 11. No False Permanent Saturation theorem

## Theorem 11.1

If:

$$
\lambda_m
<
a_{\mathrm{Leb}},
$$

then there exists:

$$
m'>m
$$

such that:

$$
\boxed{
\lambda_{m'}
>
\lambda_m.
}
$$

### Proof

Since:

$$
\lambda_m
$$

is attained, choose a maximizing family:

$$
\mathcal F_m
$$

such that:

$$
\Lambda(\mathcal F_m)
=
\lambda_m.
$$

Let:

$$
\mathcal M_m
$$

be the set of all minimizing covers that:

- cover $\mathcal F_m$;
- have area exactly:

$$
\lambda_m.
$$

It is compact.

Since:

$$
\lambda_m
<
a_{\mathrm{Leb}},
$$

no:

$$
U\in\mathcal M_m
$$

is universal.

So for every:

$$
U\in\mathcal M_m,
$$

there exists:

$$
K_U\in\mathcal W_1^0
$$

such that:

$$
K_U
$$

does not fit in $U$.

For fixed:

$$
K,
$$

the fit set:

$$
S_K
$$

is closed.

So the non-fit set:

$$
N_K
=
\mathcal M_m\setminus S_K
$$

is open in:

$$
\mathcal M_m.
$$

The family:

$$
\{N_{K_U}\}_{U\in\mathcal M_m}
$$

covers the compact:

$$
\mathcal M_m.
$$

So there exists a finite subcover:

$$
N_{K_1},
\ldots,
N_{K_r}.
$$

Let:

$$
\mathcal F'
=
\mathcal F_m
\cup
\{K_1,\ldots,K_r\}.
$$

If:

$$
\Lambda(\mathcal F')
=
\lambda_m,
$$

then there exists a minimizing cover of area:

$$
\lambda_m
$$

$$
U'
$$

covering:

$$
\mathcal F'.
$$

Since it also covers:

$$
\mathcal F_m,
$$

we have:

$$
U'\in\mathcal M_m.
$$

But the finite-subcover property means every:

$$
U\in\mathcal M_m
$$

fails to cover at least one of:

$$
K_1,\ldots,K_r.
$$

Contradiction.

Therefore:

$$
\Lambda(\mathcal F')
>
\lambda_m.
$$

Taking:

$$
m'=m+r,
$$

gives:

$$
\lambda_{m'}
>
\lambda_m.
$$

Q.E.D.

---

# 12. No False Plateau corollary

If there exists:

$$
m_0
$$

such that:

$$
\lambda_m
=
L
$$

for all:

$$
m\ge m_0,
$$

then:

$$
\boxed{
L=a_{\mathrm{Leb}}.
}
$$

That is:

$$
\boxed{
\text{finite-witness hierarchy cannot permanently plateau below truth}.
}
$$

Note:

observing several consecutive levels with the same numerical value does not by itself prove a permanent plateau.

An exact certificate is required.

---

# 13. Saturation dichotomy

Round 05 splits exact closure into two logically possible regimes.

## Regime I: Finite-attainment

There exists:

$$
m_\star<\infty
$$

such that:

$$
\boxed{
\lambda_{m_\star}
=
a_{\mathrm{Leb}}.
}
$$

In this case there exists a finite witness family:

$$
\mathcal F_\star
$$

that exactly saturates the lower bound.

---

## Regime II: Asymptotic-only

For every finite:

$$
m,
$$

we have:

$$
\lambda_m
<
a_{\mathrm{Leb}},
$$

but:

$$
\lambda_m
\uparrow
a_{\mathrm{Leb}}.
$$

In this case no single finite witness family locks in the true value.

So:

$$
\boxed{
\text{exact finite closure}
}
$$

is not automatically guaranteed by compactness.

This is precisely the central saturation question that must be tested and proved in the future.

---

# 14. Exact finite saturation theorem

## Theorem 14.1

Suppose there exists a finite witness family:

$$
\mathcal F_\star
$$

and a universal cover:

$$
U_\star
$$

such that:

$$
\Lambda(\mathcal F_\star)
\ge
A_\star
$$

and:

$$
\operatorname{Area}(U_\star)
\le
A_\star.
$$

Then:

$$
\boxed{
a_{\mathrm{Leb}}
=
A_\star.
}
$$

### Proof

By the finite witness lower theorem:

$$
a_{\mathrm{Leb}}
\ge
\Lambda(\mathcal F_\star)
\ge
A_\star.
$$

By the universal upper candidate:

$$
a_{\mathrm{Leb}}
\le
\operatorname{Area}(U_\star)
\le
A_\star.
$$

So equality holds.

Q.E.D.

---

# 15. Saturation gap

For a finite witness family:

$$
\mathcal F
$$

and a certified universal cover:

$$
U,
$$

define:

$$
\boxed{
\Gamma(\mathcal F,U)
=
\operatorname{Area}(U)
-
\Lambda(\mathcal F).
}
$$

We necessarily have:

$$
\Gamma\ge0.
$$

If:

$$
\boxed{
\Gamma=0,
}
$$

then exact finite saturation holds.

So after Round 05, AMRAL need no longer chase only:

- a higher lower bound;
- a lower upper bound;

but can instead chase:

$$
\boxed{
\Gamma\downarrow0.
}
$$

---

# 16. Primal–dual squeeze ladder

Let:

$$
\mathcal F_1
\subseteq
\mathcal F_2
\subseteq
\cdots
$$

be witness families formed by progressively adding hard targets.

Define:

$$
L_n
=
\Lambda(\mathcal F_n).
$$

If:

$$
U_n
$$

are progressively improved, certified universal candidates, define:

$$
A_n
=
\operatorname{Area}(U_n).
$$

Then:

$$
\boxed{
L_n
\le
a_{\mathrm{Leb}}
\le
A_n.
}
$$

If:

$$
\mathcal F_n
\subseteq
\mathcal F_{n+1},
$$

then:

$$
L_{n+1}\ge L_n.
$$

If only area-improving universal surgery is accepted:

$$
A_{n+1}\le A_n.
$$

So:

$$
\boxed{
L_n
\uparrow,
\qquad
A_n
\downarrow.
}
$$

Define the squeeze gap:

$$
G_n
=
A_n-L_n.
$$

The research goal becomes:

$$
\boxed{
G_n\to0
}
$$

or finite:

$$
G_n=0.
$$

---

# 17. Witness-exchange interpretation

If the finite lower minimizer:

$$
U_{\mathcal F}
$$

is not universal, then:

$$
W(U_{\mathcal F})>0.
$$

The adversarial target oracle from Rounds 01–03 can search for:

$$
K_{\mathrm{new}}
$$

such that:

$$
M_{U_{\mathcal F}}(K_{\mathrm{new}})>0.
$$

and add it to:

$$
\mathcal F.
$$

But a single witness does not guarantee that:

$$
\Lambda
$$

immediately rises strictly, since some other existing minimizer might still be able to accommodate it.

Theorem 11.1 shows that what is actually needed is:

> to find a finite witness batch that simultaneously covers/excludes the entire current minimizer set.

So the next stage of witness exchange should not merely search for:

$$
\text{one violated target}
$$

but should instead search for:

$$
\boxed{
\text{a minimizer-set separating witness batch}.
}
$$

---

# 18. Candidate support cell

Round 04's support-height quantization defines candidate cells.

Let:

$$
\mathbf b
=
(b_0,\ldots,b_{M-1})
$$

be the upward-quantized support vector.

Define the cell:

$$
\boxed{
\mathfrak C(\mathbf b)
=
\left\{
U\in\mathcal C_{\bar A}:
\underline b_j
\le
h_U(u_j)
\le
b_j
\right\},
}
$$

where:

$$
\underline b_j
=
\max
\left\{
\frac12,
b_j-q
\right\}.
$$

Outer polygon:

$$
\boxed{
P_{\mathbf b}
=
\bigcap_j
\{x:x\cdot u_j\le b_j\}.
}
$$

For any:

$$
U\in\mathfrak C(\mathbf b),
$$

we have:

$$
U\subseteq P_{\mathbf b}.
$$

---

# 19. Cell-local Hausdorff error

Let:

$$
R_{\mathbf b}
=
\max_{x\in P_{\mathbf b}}
\|x\|.
$$

Then for:

$$
U\in\mathfrak C(\mathbf b)
$$

we have:

$$
U\subseteq P_{\mathbf b}
$$

and both are contained in:

$$
B_{R_{\mathbf b}}.
$$

Take any:

$$
v\in S^1
$$

and its nearest grid direction:

$$
u_j
$$

such that:

$$
\|v-u_j\|
\le
d_M.
$$

By the cell's lower support:

$$
h_U(u_j)
\ge
b_j-q.
$$

Therefore:

$$
\begin{aligned}
h_{P_{\mathbf b}}(v)
&\le
b_j
+
R_{\mathbf b}d_M,\\
h_U(v)
&\ge
b_j-q
-
R_{\mathbf b}d_M.
\end{aligned}
$$

So:

$$
\boxed{
d_H(U,P_{\mathbf b})
\le
\varepsilon_{\mathbf b}
:=
q+2R_{\mathbf b}d_M.
}
$$

This is typically tighter than Round 04's global:

$$
\varepsilon_{M,q}.
$$

---

# 20. Consistent cell area lower bound

Since:

$$
P_{\mathbf b}
\subseteq
U+\varepsilon_{\mathbf b}B,
$$

the Steiner formula gives:

$$
\operatorname{Area}(P_{\mathbf b})
\le
\operatorname{Area}(U)
+
\varepsilon_{\mathbf b}\operatorname{Per}(U)
+
\pi\varepsilon_{\mathbf b}^2.
$$

And:

$$
U\subseteq P_{\mathbf b}
$$

with convex perimeter monotone under inclusion:

$$
\operatorname{Per}(U)
\le
\operatorname{Per}(P_{\mathbf b}).
$$

So:

$$
\boxed{
\operatorname{Area}(U)
\ge
\operatorname{Area}(P_{\mathbf b})
-
\operatorname{Per}(P_{\mathbf b})
\varepsilon_{\mathbf b}
-
\pi\varepsilon_{\mathbf b}^2.
}
$$

Define:

$$
\boxed{
\operatorname{LB}_{\mathrm{outer}}(\mathbf b)
=
\operatorname{Area}(P_{\mathbf b})
-
\operatorname{Per}(P_{\mathbf b})
\varepsilon_{\mathbf b}
-
\pi\varepsilon_{\mathbf b}^2.
}
$$

This is a safe, cell-local, resolution-consistent area lower bound.

---

# 21. Support-envelope area lower bound

There is also an independent cell lower bound.

Every:

$$
U\in\mathfrak C(\mathbf b)
$$

contains:

$$
B_r(0),
\qquad
r=\frac12.
$$

Since:

$$
U\subseteq B_R,
$$

the support function is $R$-Lipschitz.

So:

$$
h_U(\theta)
\ge
\ell_{\mathbf b}(\theta),
$$

where:

$$
\boxed{
\ell_{\mathbf b}(\theta)
=
\max
\left\{
r,
\max_j
[
\underline b_j
-
R\|u_\theta-u_j\|
]
\right\}.
}
$$

The planar Cauchy perimeter formula:

$$
\operatorname{Per}(U)
=
\int_0^{2\pi}
h_U(\theta)\,d\theta.
$$

Therefore:

$$
\operatorname{Per}(U)
\ge
\int_0^{2\pi}
\ell_{\mathbf b}(\theta)\,d\theta.
$$

On the other hand, the Minkowski area formula:

$$
\operatorname{Area}(U)
=
\frac12
\int h_U\,dS_U.
$$

Since:

$$
h_U\ge r
$$

and:

$$
S_U(S^1)
=
\operatorname{Per}(U),
$$

we have:

$$
\operatorname{Area}(U)
\ge
\frac r2
\operatorname{Per}(U).
$$

So:

$$
\boxed{
\operatorname{Area}(U)
\ge
\frac r2
\int_0^{2\pi}
\ell_{\mathbf b}(\theta)\,d\theta.
}
$$

For:

$$
r=\frac12,
$$

this is:

$$
\boxed{
\operatorname{LB}_{\mathrm{env}}(\mathbf b)
=
\frac14
\int_0^{2\pi}
\ell_{\mathbf b}(\theta)\,d\theta.
}
$$

---

# 22. Single-protrusion area lower bound

If:

$$
B_r(0)\subseteq U
$$

and:

$$
h_U(u)\ge s\ge r,
$$

then $U$ contains at least:

$$
\operatorname{conv}(B_r,x)
$$

for some:

$$
x
$$

satisfying:

$$
\|x\|\ge s.
$$

Define:

$$
\boxed{
\Phi_r(s)
=
\pi r^2
+
r\sqrt{s^2-r^2}
-
r^2
\arccos\frac rs.
}
$$

Then:

$$
\operatorname{Area}(U)
\ge
\Phi_r(s).
$$

and:

$$
\Phi_r
$$

is monotonically increasing in:

$$
s\ge r.
$$

So the cell can additionally take:

$$
\boxed{
\operatorname{LB}_{\mathrm{tip}}(\mathbf b)
=
\max_j
\Phi_r(\underline b_j).
}
$$

---

# 23. Combined cell area lower bound

This round proposes:

$$
\boxed{
\operatorname{LB}_{\mathrm{cell}}(\mathbf b)
=
\max
\left\{
\pi r^2,
\operatorname{LB}_{\mathrm{outer}},
\operatorname{LB}_{\mathrm{env}},
\operatorname{LB}_{\mathrm{tip}}
\right\}.
}
$$

All of these are safe lower bounds.

In practice only the lower-computational-cost subset need be enabled.

---

# 24. Candidate-cell prune rules

Suppose there is currently a certified universal incumbent:

$$
U^+
$$

of area:

$$
A^+
=
\operatorname{Area}(U^+).
$$

For a candidate cell:

$$
\mathfrak C(\mathbf b)
$$

there are two main safe prunes.

---

## Rule P1: Outer non-universality prune

If the outer polygon:

$$
P_{\mathbf b}
$$

has been proved by Rounds 02–03 to satisfy:

$$
W(P_{\mathbf b})>0,
$$

then, since:

$$
U\subseteq P_{\mathbf b}
$$

for every:

$$
U
$$

in the cell, it must be that:

$$
U
$$

is also non-universal.

So the entire cell is pruned.

---

## Rule P2: Area prune

If:

$$
\boxed{
\operatorname{LB}_{\mathrm{cell}}(\mathbf b)
\ge
A^+,
}
$$

then this cell cannot possibly improve on the incumbent.

The entire cell is pruned.

---

# 25. Active cell

If:

- the outer polygon has not yet been proved non-universal; and
- the area lower bound is still less than:

$$
A^+;
$$

then the cell is marked:

$$
\boxed{
\text{ACTIVE CELL}.
}
$$

For an active cell, one may:

- increase the normal-direction resolution;
- shrink the support interval;
- or proceed directly to local inward surgery / witness search.

---

# 26. Strictly Non-Universal Cells Are Eventually Pruned

Consider nested cells:

$$
\mathfrak C_n
$$

whose resolution:

$$
\varepsilon_n\to0
$$

converges to a candidate:

$$
U.
$$

Suppose:

$$
W(U)
=
\delta
>
0.
$$

The outer polygons:

$$
P_n
$$

satisfy:

$$
d_H(P_n,U)
\le
\varepsilon_n.
$$

By Round 04:

$$
|W(P_n)-W(U)|
\le
\varepsilon_n.
$$

So once:

$$
\varepsilon_n<\frac\delta2,
$$

we have:

$$
W(P_n)
>
\frac\delta2
>
0.
$$

Therefore:

$$
P_n
$$

is proved non-universal, and the cell is pruned by P1.

So:

$$
\boxed{
\text{strictly non-universal limit candidates cannot survive infinite refinement}.
}
$$

---

# 27. Strictly Suboptimal Cells Are Also Eventually Area-Pruned

Suppose nested cells converge to:

$$
U
$$

with:

$$
\operatorname{Area}(U)
>
A^+
+
\delta.
$$

Since:

$$
d_H(P_n,U)\to0
$$

and area is continuous with respect to Hausdorff convergence of convex bodies:

$$
\operatorname{LB}_{\mathrm{outer}}(\mathfrak C_n)
\to
\operatorname{Area}(U).
$$

So for sufficiently large:

$$
n,
$$

we have:

$$
\operatorname{LB}_{\mathrm{cell}}(\mathfrak C_n)
>
A^+.
$$

So P2 prunes it.

Hence:

$$
\boxed{
\text{strictly area-suboptimal limit candidates cannot survive infinite refinement}.
}
$$

---

# 28. Active-cell localization theorem

If:

$$
A_n^+
\downarrow
a_{\mathrm{Leb}}
$$

and the candidate-cell resolution:

$$
\to0,
$$

then the limit of any nested active-cell sequence that survives forever:

$$
U_\infty
$$

must satisfy:

$$
W(U_\infty)\le0
$$

and:

$$
\operatorname{Area}(U_\infty)
=
a_{\mathrm{Leb}}.
$$

In other words:

$$
\boxed{
\text{branch-and-bound active cells asymptotically localize to optimal universal covers}.
}
$$

This is still not a finite-termination theorem.

It is an asymptotic localization theorem.

---

# 29. Exact stopping criterion

Round 05 can now state very clearly:

candidate-cell branch-and-bound can approximate the optimum arbitrarily closely, without limit.

Finite exact stopping instead requires an additional locking event:

$$
\boxed{
\Lambda(\mathcal F_\star)
=
\operatorname{Area}(U_\star).
}
$$

So the main workflow is not:

> wait for a cell to shrink to a single point on its own.

but rather:

1. branch-and-bound finds candidate upper bounds;
2. active targets form a finite witness lower family;
3. the witness lower optimizer, in turn, produces new hard targets;
4. upper surgery and lower witness exchange advance together;
5. as soon as lower = upper, exact closure is immediate.

---

# 30. Saturation architecture

The whole of AMRAL-LUC-FC can now be written as:

$$
\boxed{
\begin{array}{c}
\text{Candidate Cover Search}\\
\downarrow\\
U_n,\ A_n
\end{array}
}
\qquad
\boxed{
\begin{array}{c}
\text{Hard Witness Search}\\
\downarrow\\
\mathcal F_n,\ L_n
\end{array}
}
$$

coupled in the middle by:

$$
\boxed{
L_n
\le
a_{\mathrm{Leb}}
\le
A_n
}
$$

If:

$$
A_n-L_n>0,
$$

then:

- the upper side searches for a removable boundary;
- the lower side searches for minimizer-set separating witnesses.

If:

$$
A_n-L_n=0,
$$

then:

$$
\boxed{
\text{CLOSE}.
}
$$

---

# 31. Interfaces with Existing 2026 Research

## Mishra route

Mishra's:

- disk;
- Reuleaux triangle;
- Reuleaux pentagon;

is exactly a finite witness family.

Its 2026 certificate proves:

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

Round 05 regards it as:

$$
\boxed{
\text{a known node of the finite-witness ladder}.
}
$$

---

## Zeng route

Zeng establishes:

$$
\Lambda_M
$$

a finite-dimensional Reuleaux-type hierarchy, and proves:

$$
a_{\mathrm{Leb}}
=
\lim_M\Lambda_M.
$$

Round 05's:

$$
\lambda_m
$$

is not the same hierarchy.

The difference:

- $\Lambda_M$: bounds finite-arc representation complexity;
- $\lambda_m$: bounds the cardinality of the finite hard-witness family.

The two can form a two-axis program:

$$
\boxed{
\text{representation complexity}
\times
\text{witness cardinality}.
}
$$

Future work should study whether a branch correspondence exists between:

$$
\Lambda_M
\leftrightarrow
\lambda_m
$$

Currently:

`CROSS-MAP: OPEN`

---

# 32. New Finite-Attainment Conjecture

This round does not presuppose that exact finite saturation necessarily exists.

We propose:

## Finite Witness Attainment Conjecture

There exists:

$$
m_\star<\infty
$$

such that:

$$
\boxed{
\lambda_{m_\star}
=
a_{\mathrm{Leb}}.
}
$$

Equivalently, there exists a finite:

$$
\mathcal F_\star
$$

such that:

$$
\Lambda(\mathcal F_\star)
=
a_{\mathrm{Leb}}.
$$

This conjecture:

- may be true;
- may also be false;
- can be continually tested by the AMRAL hierarchy;
- should not be prematurely declared on the basis of numerical stabilization.

---

# 33. Stronger Branch-Type Version

Even if the Finite Witness Attainment Conjecture is false, there might still exist:

$$
\boxed{
\text{finite branch types}
}
$$

rather than finite witness points.

That is:

$$
\mathcal F_\star
=
\bigcup_{\alpha=1}^{N}
\mathcal B_\alpha
$$

where each:

$$
\mathcal B_\alpha
$$

is a compact low-dimensional family, with the whole being saturated.

So Round 00's finite-closure definition is preserved as:

> a finite number of saturated branch types, not requiring a finite number of isolated objects.

This is a fallback generalization of Finite Witness Attainment.

---

# 34. COMPUTE-DEFERRED

Round 05's main theorems do not require large-scale computation.

The following tasks now have clear inputs/outputs.

## C05-1: Mishra three-witness reconstruction

Reconstruct:

$$
\mathcal F_3
=
\{
D,
R_3,
R_5
\}.
$$

Goals:

- independently reproduce lower certificate;
- find its minimizer set;
- analyze which hard targets are still missing.

---

## C05-2: Minimizer-set witness batch search

Input:

$$
\mathcal F_n.
$$

Find:

$$
\operatorname{Argmin}
\Lambda(\mathcal F_n).
$$

Search the minimizer samples for violated constant-width targets.

The goal is not a single target, but a finite batch:

$$
\{K_1,\ldots,K_r\}
$$

covering the non-fit neighborhoods of the entire minimizer set.

---

## C05-3: Candidate-cell branch-and-bound prototype

For every cell compute:

- outer polygon;
- $R_{\mathbf b}$;
- $\varepsilon_{\mathbf b}$;
- area;
- perimeter;
- $\operatorname{LB}_{\mathrm{outer}}$;
- optional $\operatorname{LB}_{\mathrm{env}}$;
- outer universality status.

---

## C05-4: Upper/lower squeeze dashboard

Each round save:

$$
L_n,
\qquad
A_n,
\qquad
G_n=A_n-L_n.
$$

and also save:

- witness count;
- active candidate cells;
- pruned cells;
- exact / deferred gates.

---

# 35. Assigned topic for Round 06

## AMRAL-LUC-FC-R06
### Finite Witness Exchange Compiler and Minimizer-Set Separation

The next round focuses primarily on the lower side.

Main goals:

1. represent:

$$
\operatorname{Argmin}\Lambda(\mathcal F)
$$

as a searchable compact configuration domain;

2. establish the violated-target oracle:

$$
U
\mapsto
K_U;
$$

3. establish a minimizer-set separating finite batch compiler;

4. use the Mishra three-witness family as the first external benchmark node;

5. study whether the lower bound strictly rises after adding the $4,5,\ldots$-th hard witness;

6. record witness ancestry:
   - REUSED;
   - REDUCED;
   - EXTENSION;
   - NOVEL;
   - FALSE-POSITIVE.

Round 06's goal does not require computing a giant certificate in one pass.

If computation is heavy:

`COMPUTE-DEFERRED`

but the proof graph must keep shrinking.

---

# 36. Reproducibility checklist

## Convergence vs attainment separation

`CLOSED`

## Finite witness lower theorem

`PROVED`

## Finite witness lower value attainment

`PROVED`

## Finite-witness completeness

`PROVED`

## Cardinality hierarchy convergence

`PROVED`

## Level attainment

`PROVED`

## No false permanent plateau

`PROVED`

## Exact finite saturation criterion

`PROVED`

## Candidate-cell area lower bound

`PROVED`

## Outer non-universal prune

`PROVED`

## Strict non-universal eventual prune

`PROVED`

## Strict area-suboptimal eventual prune

`PROVED`

## Exact finite witness attainment

`OPEN`

## New numerical bound

`NONE`

---

# 37. Shortest Handoff Conclusion

Round 05 rewrites "saturation" from a vague concept into two explicit levels.

Level one:

$$
\boxed{
a_{\mathrm{Leb}}
=
\sup_{\mathcal F\ finite}
\Lambda(\mathcal F)
=
\lim_{m\to\infty}\lambda_m.
}
$$

This means finite hard-witness families are complete in the limit.

Level two:

$$
\boxed{
\exists m_\star:
\lambda_{m_\star}=a_{\mathrm{Leb}}
\ ? 
}
$$

This is the real question of exact finite saturation.

If there exist:

$$
\mathcal F_\star,
\qquad
U_\star
$$

such that:

$$
\boxed{
\Lambda(\mathcal F_\star)
=
\operatorname{Area}(U_\star),
}
$$

then the Lebesgue universal covering problem achieves exact closure immediately.

At the same time, candidate-cell branch-and-bound already has:

- a nonuniversality prune;
- an area prune;
- asymptotic optimal-frontier localization.

So starting from Round 06, the research core formally shifts from:

$$
\text{finite approximation}
$$

toward:

$$
\boxed{
\text{finite witness discovery and saturation}.
}
$$

---

# References

1. J. C. Baez, K. Bagdasaryan, P. Gibbs, *The Lebesgue Universal Covering Problem*, arXiv:1502.01251.
2. P. Gibbs, *An Upper Bound for Lebesgue's Covering Problem*, arXiv:1810.10089, 2018.
3. U. Mishra, *Curves of constant width and Lebesgue's covering problem*, arXiv:2608.30538, 2026.
4. S. Zeng, *An exact hierarchy for Lebesgue's universal covering constant and a certified 0.834 lower bound*, arXiv:2609.01284, 2026.
5. R. Schneider, *Convex Bodies: The Brunn–Minkowski Theory*.
6. Neo.K + Aletheia, *AMRAL × Lebesgue Universal Covering — Round 00–04*, 2026-09-18.

---

# 38. Declaration

This round does not claim:

- that the Finite Witness Attainment Conjecture has been proved;
- that some finite witness family has already reached the true value;
- an improvement on the currently published lower/upper bound;
- that the Lebesgue universal covering problem has been solved.

What this round accomplishes is:

$$
\boxed{
\text{finite-resolution hierarchy}
\to
\text{formal saturation theory}
}
$$

and:

$$
\boxed{
\text{exact closure}
\iff
\text{finite lower witness matches certified universal upper candidate}
}
$$

In the AMRAL proof graph, this marks the boundary between the approximation phase and the entry into the witness-saturation phase.