# AMRAL × Lebesgue Universal Covering — Round 08
## Conditional-Lift Certificate Compiler for the 0.8350 Milestone

**Document ID:** AMRAL-LUC-FC-R08  
**Version:** v0.1  
**Date:** 2026-09-18  
**Research status:** Round 08 / Conditional-lift proof compiler / Certificate grammar  
**Research mode:** Human-Directed + Semi-Autonomous AI Mathematical Research  
**Research direction and methodology source:** Neo.K  
**AI collaborating researcher and primary executor:** Aletheia / ChatGPT, GPT-5.6 Sol  
**Parent methodology:** Relational Constraint–Handoff Methodology (RCHM)  
**Predecessor documents:** AMRAL-LUC-FC-R00 v0.2; R01–R07 v0.1

---

# 0. This Round's Summary Verdict

Round 07 has already fixed the first actual improvement milestone as:

$$
T_1=0.8350,
$$

and rewrites the five-dimensional sublevel region of the base family:

$$
\mathcal F_3=\{D,B_3,B_5\}
$$

$$
\mathcal Q_{<T_1}
$$

as a threshold-conditioned minimizer atlas.

Round 08's task is not to claim that a large-scale atlas has already been completed, but to establish the full proof grammar for:

$$
\boxed{
\text{base atlas}
+
\text{cell-local witness lift}
+
\text{independent verifier}
}
$$

This round obtains the following main results.

---

## Conclusion A: Mishra's Erosion Lemma Can Be Abstracted into a General Convex Common-Core Theorem

Let:

$$
K\subseteq B_{R_K}(0)
$$

be a compact convex witness.

Fix the same reflection branch, and consider the placement box:

$$
\phi\in[\phi_0-h_\phi,\phi_0+h_\phi],
$$

$$
x\in[x_0-h_x,x_0+h_x],
$$

$$
y\in[y_0-h_y,y_0+h_y].
$$

The box-center placement:

$$
K_0
=
R_{\phi_0}K+t_0.
$$

An arbitrary box placement:

$$
K_g
=
R_\phi K+t.
$$

Then:

$$
\boxed{
d_H(K_0,K_g)
\le
\delta
:=
\sqrt{h_x^2+h_y^2}
+
2R_K\sin\frac{h_\phi}{2}.
}
$$

If the convex core:

$$
C
$$

satisfies:

$$
\boxed{
C+\delta B
\subseteq
K_0,
}
$$

then:

$$
\boxed{
C\subseteq K_g
\quad
\text{for every placement in the box}.
}
$$

This is the generalized common-core theorem.

---

## Conclusion B: Reuleaux Erosion Is a Special Case of the General Common-Core Theorem

If:

$$
K
=
\bigcap_j
B(V_j,1)
$$

is a width-one Reuleaux polygon, then:

$$
\boxed{
C
=
\bigcap_j
B(V_j,1-\delta)
}
$$

satisfies:

$$
C+\delta B
\subseteq K.
$$

So the official erosion core:

$$
1\mapsto1-\delta
$$

is exactly the closed-form specialization of the general common-core theorem.

---

## Conclusion C: Round 02's General Fourier/Asymmetric Witnesses Can Also Use the Same Lift Machinery

For a general convex witness, it is not required to be a Reuleaux polygon.

The verifier need only receive:

1. the box-center body $K_0$;
2. the motion radius $\delta$;
3. a candidate inner core $C$;
4. an independently verifiable inclusion certificate:

   $$
   C+\delta B\subseteq K_0.
   $$

From this it follows that:

$$
C
$$

is the common core of the entire placement box.

Hence fallback witnesses may come from:

- regular Reuleaux odd-gons;
- irregular Reuleaux polygons;
- Round 02's finite Fourier dictionary;
- asymmetric constant-width bodies.

There is no need to invent a separate witness-specific proof logic.

---

## Conclusion D: Establishing the Nested Base/Lift Certificate Theorem

For every base atlas leaf:

$$
C_j,
$$

the final certificate must belong to one of two kinds.

### `BASE-PRUNED`

The base family common-core lower bound already satisfies:

$$
L_{\mathcal F_3}(C_j)\ge T_1.
$$

### `LIFT-CLOSED`

There exists a witness:

$$
K_j
$$

together with a finite local lift tree, such that the witness's placement root domain is entirely covered, and for every lift leaf:

$$
\operatorname{Area}
\operatorname{conv}
(
D,
C_3,
C_5,
C_{K_j}
)
$$

rigorously satisfies:

$$
\ge T_1.
$$

If all base leaves are legally classified, then:

$$
\boxed{
\Lambda
\left(
\mathcal F_3
\cup
\{K_j:\text{some base leaf uses }K_j\}
\right)
\ge T_1.
}
$$

---

## Conclusion E: Establishing an Independent Certificate Grammar

The final proof package may not contain:

- an unclassified base leaf;
- an unresolved lift leaf;
- a missing witness subtree;
- an unverified root domain;
- a search-only numerical value.

The verifier must independently reconstruct:

1. the base root;
2. the deterministic split;
3. each base leaf;
4. each witness lift root;
5. each lift subtree;
6. each leaf's common core;
7. each lower hull area;
8. the floating-point / interval error margin;
9. tree structural identity;
10. all referenced hashes.

---

## Conclusion F: B7's $0.8350$ Lift Root Is Now Fixed

For the regular Reuleaux body $B_7$:

$$
R_7
=
\frac{1}
{
2\sin(3\pi/7)
}
\approx
0.512858431636.
$$

Round 07's threshold-dependent a-priori domain:

$$
\boxed{
|t_7|
\le
0.196935046771
}
$$

already covers every $B_7$ translation that could possibly make the hull area fall below:

$$
0.8350
$$

rotation symmetry:

$$
\boxed{
\phi_7\in[0,2\pi/7).
}
$$

Hence every hard base cell need only activate the fixed three-dimensional local root:

$$
(\phi_7,x_7,y_7).
$$

---

## Conclusion G: The Geometric Headroom at $0.8350$ Is Enough to Serve as the First Milestone, but It Is Not Yet Proved

The official rigorous three-body outer ceiling:

$$
0.834781190917.
$$

So only the following increase is needed:

$$
\boxed{
0.8350-0.834781190917
=
0.000218809083
}
$$

to exceed the milestone.

The official four-body:

$$
D+B_3+B_5+B_7
$$

search-only optimum:

$$
0.836494901
$$

is higher than the milestone by:

$$
\boxed{
0.001494901.
}
$$

This provides numerical headroom, but it is not a proof.

---

This round's overall verdict:

$$
\boxed{
\text{CONDITIONAL-LIFT CERTIFICATE COMPILER: CLOSED}
}
$$

$$
\boxed{
\text{GENERIC CONVEX COMMON-CORE INTERFACE: CLOSED}
}
$$

$$
\boxed{
a_{\mathrm{Leb}}\ge0.8350:
\text{COMPUTE-DEFERRED}
}
$$

---

# 1. The General Placement-Box Motion Bound

Let:

$$
K\subseteq B_{R_K}(0).
$$

Consider, within the same reflection component:

$$
g_0(x)
=
R_{\phi_0}x+t_0,
$$

and:

$$
g(x)
=
R_\phi x+t.
$$

Assume:

$$
|\phi-\phi_0|
\le
h_\phi,
$$

and:

$$
|t_x-t_{0x}|
\le
h_x,
$$

$$
|t_y-t_{0y}|
\le
h_y.
$$

For any:

$$
x\in K,
$$

we have:

$$
\begin{aligned}
\|g(x)-g_0(x)\|
&\le
\|t-t_0\|
+
\|
(R_\phi-R_{\phi_0})x
\|\\
&\le
\sqrt{h_x^2+h_y^2}
+
2R_K
\sin
\frac{|\phi-\phi_0|}{2}\\
&\le
\sqrt{h_x^2+h_y^2}
+
2R_K
\sin
\frac{h_\phi}{2}.
\end{aligned}
$$

So:

$$
\boxed{
d_H(gK,g_0K)
\le
\delta
=
\sqrt{h_x^2+h_y^2}
+
2R_K
\sin\frac{h_\phi}{2}.
}
$$

This exactly reproduces the displacement bound used by the official Reuleaux box erosion.

---

# 2. General Convex Common-Core Theorem

## Theorem 2.1

Let:

$$
K_0
$$

and every:

$$
K_g
$$

in the placement box satisfy:

$$
d_H(K_0,K_g)\le\delta.
$$

If the compact convex:

$$
C
$$

satisfies:

$$
C+\delta B
\subseteq
K_0,
$$

then:

$$
\boxed{
C\subseteq K_g
}
$$

holds for every placement in the box.

### Proof

The Hausdorff inequality, for convex support functions, is equivalent to:

$$
|h_{K_g}(u)-h_{K_0}(u)|
\le
\delta
$$

for all:

$$
u\in S^1.
$$

So:

$$
h_{K_g}(u)
\ge
h_{K_0}(u)-\delta.
$$

On the other hand:

$$
C+\delta B
\subseteq
K_0
$$

is equivalent to:

$$
h_C(u)+\delta
\le
h_{K_0}(u).
$$

Hence:

$$
h_C(u)
\le
h_{K_0}(u)-\delta
\le
h_{K_g}(u)
$$

for all $u$.

By support-function containment:

$$
C\subseteq K_g.
$$

Q.E.D.

---

# 3. The Core Interface Does Not Require an Explicit Minkowski Erosion

Conceptually one may write:

$$
K_0\ominus\delta B.
$$

But the computational verifier does not actually need to compute the exact erosion.

It suffices to provide any:

$$
C
$$

satisfying:

$$
\boxed{
h_C(u)+\delta
\le
h_{K_0}(u)
\quad
\forall u.
}
$$

Hence core providers can be divided into three classes.

---

## `REULEAUX-EROSION`

For:

$$
K
=
\bigcap_jB(V_j,1),
$$

directly:

$$
C
=
\bigcap_jB(V_j,1-\delta).
$$

The verifier must recompute:

- the nonempty condition;
- circle–circle intersections;
- all-disk membership.

---

## `ANALYTIC-SUPPORT-CORE`

If:

$$
h_K-\delta
$$

is itself already known to be a legal support function, it may be used directly.

For example, Round 02's safely interiorized trigonometric bodies can use this route when the curvature margin is large enough.

---

## `CERTIFIED-SUPPORT-CORE`

Any convex:

$$
C
$$

with a finite representation, as long as it is accompanied by a Round-03-type finite support certificate for:

$$
\boxed{
h_C+\delta\le h_{K_0}
}
$$

Hence the generic witness interface does not depend on the Reuleaux closed form.

---

# 4. Reuleaux specialization

A width-one regular / irregular Reuleaux polygon:

$$
K
=
\bigcap_jB(V_j,1).
$$

Let:

$$
0\le\delta<1.
$$

Define:

$$
C_\delta
=
\bigcap_jB(V_j,1-\delta).
$$

If:

$$
x\in C_\delta
$$

and for any:

$$
z\in\delta B,
$$

then for all:

$$
j,
$$

we have:

$$
\|x+z-V_j\|
\le
\|x-V_j\|+\|z\|
\le
1.
$$

So:

$$
x+\delta B
\subseteq
K.
$$

That is:

$$
C_\delta+\delta B
\subseteq K.
$$

By the General Convex Common-Core Theorem:

$$
C_\delta
$$

is the common core of the entire placement box.

---

# 5. Base cell common cores

The base family:

$$
D+B_3+B_5.
$$

For the base box:

$$
C_{\mathrm{base}},
$$

let:

$$
h_{x3},h_{y3}
$$

be the translation half-widths of $B_3$.

Since $B_3$'s orientation is fixed:

$$
\boxed{
\delta_3
=
\sqrt{
h_{x3}^2+h_{y3}^2
}.
}
$$

For $B_5$:

$$
\boxed{
\delta_5
=
\sqrt{
h_{x5}^2+h_{y5}^2
}
+
2R_5\sin\frac{h_{\phi5}}2.
}
$$

The common cores:

$$
C_3
=
B_3^{\mathrm{center}}
\ominus
\delta_3B,
$$

$$
C_5
=
B_5^{\mathrm{center}}
\ominus
\delta_5B.
$$

In the Reuleaux closed form these are just the defining disk radii:

$$
1-\delta_3,
\qquad
1-\delta_5.
$$

---

# 6. B7 local lift root

For the milestone:

$$
T_1=0.8350,
$$

Round 07 has already obtained:

$$
\boxed{
|t_7|
\le
t_7^\star
=
0.196935046771.
}
$$

rotation symmetry:

$$
\boxed{
\phi_7
\in
[0,2\pi/7).
}
$$

Hence the local root box can be taken as:

$$
\boxed{
\phi_7
\in
[0,2\pi/7),
}
$$

$$
x_7,y_7
\in
[-t_7^\star,t_7^\star].
$$

Although the corners of the square have:

$$
|t_7|>t_7^\star,
$$

these points are themselves already excluded by the a-priori area bound, so they do not break soundness.

A radial prune can also be added inside the local search.

---

# 7. B7 lift-box core

For the lift-box center:

$$
(\phi_0,x_0,y_0)
$$

with half-widths:

$$
(h_\phi,h_x,h_y),
$$

let:

$$
R_7
=
\frac1{2\sin(3\pi/7)}
\approx
0.512858431636.
$$

motion radius:

$$
\boxed{
\delta_7
=
\sqrt{h_x^2+h_y^2}
+
2R_7
\sin
\frac{h_\phi}{2}.
}
$$

box-center corners:

$$
V_j^{(0)}.
$$

common Reuleaux core:

$$
\boxed{
C_7
=
\bigcap_{j=1}^7
B(V_j^{(0)},1-\delta_7).
}
$$

If this intersection is empty:

the hull-core prune cannot be used.

This leaf must:

- split;
- or use the a-priori area bound;
- or switch to a different witness.

---

# 8. Combined lift lower bound

For the base cell:

$$
C_{\mathrm{base}}
$$

and the B7 placement box:

$$
B_7^{\mathrm{box}},
$$

the hull of any actual configuration contains:

$$
\boxed{
H_{\mathrm{core}}
=
\operatorname{conv}
(
D
\cup
C_3
\cup
C_5
\cup
C_7
).
}
$$

So:

$$
\boxed{
\operatorname{Area}
H_{\mathrm{actual}}
\ge
\operatorname{Area}
H_{\mathrm{core}}.
}
$$

Hence, as long as the verifier can prove:

$$
\boxed{
\operatorname{Area}
H_{\mathrm{core}}
\ge
T_1,
}
$$

the entire:

$$
C_{\mathrm{base}}
\times
B_7^{\mathrm{box}}
$$

can be pruned.

---

# 9. Inner-point lower witness

To avoid having the verifier depend on the search's exact hull routine, for every curved core one may take only verified boundary inner points:

$$
P_{\mathrm{core}}
\subseteq
C_{\mathrm{core}}.
$$

Let:

$$
P_D
$$

be the inscribed polygon of the disk.

Then:

$$
\operatorname{conv}
\left(
P_D
\cup
P_3
\cup
P_5
\cup
P_7
\right)
\subseteq
H_{\mathrm{core}}.
$$

So its polygon hull area:

$$
A_{\mathrm{inner}}
$$

is a rigorously one-sided lower witness.

If the upper bound on floating-point arithmetic error:

$$
e_{\mathrm{fp}}
$$

has been independently estimated, the leaf acceptance condition can be written directly as:

$$
\boxed{
A_{\mathrm{inner}}
-
e_{\mathrm{fp}}
\ge
T_1.
}
$$

This is cleaner than depending on the emitter's exact-area value.

---

# 10. Base tree grammar

The base tree of the final certificate uses a deterministic binary split.

Every node has only the following types.

## `SPLIT`

Records:

- the split axis;
- the split-rule version;
- children are implicit.

## `BASE-PRUNED`

The verifier recomputes the base common-core lower bound and checks:

$$
\ge T_1.
$$

## `LIFT-CLOSED`

Records:

- the witness id;
- the lift-certificate hash;
- the witness root-domain id.

The final certificate does not allow an:

`UNRESOLVED`

leaf.

---

# 11. Lift tree grammar

Every:

`LIFT-CLOSED`

base leaf points to a local witness tree.

Local nodes:

## `SPLIT`

Splits one witness placement dimension.

## `PRUNED`

The verifier recomputes:

$$
A_{\mathrm{inner}}
-
e_{\mathrm{fp}}
\ge T_1.
$$

The final lift tree does not allow:

- a stuck leaf;
- a missing child;
- an unconsumed stream;
- an unknown witness id.

---

# 12. Nested Certificate Soundness Theorem

## Theorem 12.1

If:

1. the base root domain covers all base placements that could possibly make the base hull:

   $$
   <T_1
   $$

2. the base tree is a deterministic partition of the root;

3. every base leaf is either:

   - a valid `BASE-PRUNED`; or
   - a valid `LIFT-CLOSED`;

4. for every `LIFT-CLOSED` leaf, its referenced witness lift tree covers the entire relevant placement root of that witness;

5. every lift leaf has a valid common-core lower witness:

   $$
   \ge T_1;
   $$

6. all tree streams are fully consumed, with no missing / unclassified node;

then, letting:

$$
\mathcal B
$$

be all the witnesses actually used in the certificate,

we have:

$$
\boxed{
\Lambda
(
\mathcal F_3\cup\mathcal B
)
\ge
T_1.
}
$$

### Proof

Take any full-family placement.

Its base projection falls into some base leaf.

If the leaf is:

`BASE-PRUNED`,

then the base hull is already:

$$
\ge T_1.
$$

The full hull is larger still.

If the leaf is:

`LIFT-CLOSED`

with witness $K$, then in that full placement, $K$'s placement must fall into some leaf of the lift tree.

That leaf's common core is contained in all the corresponding actual bodies.

So the full hull contains the verifier's inner-hull witness, whose area is:

$$
\ge T_1.
$$

This holds for any full placement.

Q.E.D.

---

# 13. Multi-Witness Fallback Does Not Increase the Joint Dimension

Suppose some base cell cannot be closed by:

$$
B_7
$$

alone.

One may:

1. first split the base cell;
2. try again on the child cells with:

   $$
   B_7;
   $$

3. for children that still fail, try:

   $$
   B_9,
   B_{11},
   K_{\mathrm{Fourier}},
   \ldots
   $$

As long as every final base leaf is closed by the complete 3-D root of at least one witness:

$$
\boxed{
\text{global batch lower bound still holds}.
}
$$

There is no need to build the joint Cartesian product of:

$$
(\phi_7,x_7,y_7,\phi_9,x_9,y_9,\ldots)
$$

---

# 14. Generic witness catalog interface

Every witness record contains at least:

```text
witness_id
representation_type
diameter
constant_width_status
centering_gauge
symmetry_period
reflection_symmetry
rotation_radius_bound
translation_domain_rule
core_provider_type
support_or_geometry_hash
```

Supported core providers:

- `REULEAUX-EROSION`
- `ANALYTIC-SUPPORT-CORE`
- `CERTIFIED-SUPPORT-CORE`

This means the verifier never needs to know how the witness was selected by the search.

---

# 15. Separation of Responsibilities Between the Search Emitter and the Verifier

## The search emitter may:

- use an exact hull routine;
- use heuristic priority;
- use a floating-point optimizer to find witnesses;
- use a cache;
- use parallel scheduling;
- guess the next split axis.

## The independent verifier may rely only on:

- certificate bytes;
- public mathematical constants;
- independent core reconstruction;
- the deterministic split rule;
- a simple convex hull / shoelace computation;
- rigorous floating-point / interval error bounds;
- cryptographic hashes.

So:

$$
\boxed{
\text{search can be smart and complex; the verifier must be simple and independent}.
}
$$

---

# 16. Verifier invariants

The final verifier checks at least the following.

## V1 — Header

- magic/version;
- threshold;
- base family ids;
- witness catalog;
- root domains;
- split rule;
- arithmetic error policy.

## V2 — Base root coverage

Checks that the translation domain is not smaller than:

$$
t_3(T_1),
\qquad
t_5(T_1).
$$

rotation:

$$
\phi_5
\in
[0,2\pi/5).
$$

## V3 — Witness root coverage

For $B_7$:

$$
\phi_7
\in
[0,2\pi/7),
$$

$$
x_7,y_7
\in
[-t_7^\star,t_7^\star].
$$

## V4 — Split coverage

The union of children must cover the parent.

There may be no gap.

## V5 — Common-core validity

Recompute:

$$
\delta_i.
$$

For Reuleaux:

- the core radius is positive;
- it is nonempty;
- the reconstructed corners lie within all defining disks.

For a generic support core:

- verify:

  $$
  h_C+\delta\le h_{K_0}.
  $$

## V6 — Inner witness validity

All polygon witness points genuinely lie within the common core.

## V7 — Area

Recompute the convex hull.

Acceptance condition:

$$
A_{\mathrm{inner}}-e_{\mathrm{fp}}\ge T_1.
$$

## V8 — Tree structure

For a binary tree:

$$
N=2L-1
$$

if it has a single root.

For a seed forest:

$$
N=2L-S
$$

where $S$ is the seed count.

## V9 — Exhaustion

The bit/tag stream must be consumed exactly to completion.

## V10 — Base-leaf completeness

Every base leaf must be either:

- base-pruned; or
- referencing a valid lift tree.

---

# 17. Certificate stream proposal

This round does not commit to a fixed binary encoding, but it does fix the semantic grammar.

Header:

```text
MAGIC = LUCFC08
VERSION
TARGET
BASE_FAMILY
BASE_ROOT
BASE_SPLIT_RULE
WITNESS_CATALOG_HASH
ARITHMETIC_POLICY
```

Base stream token:

```text
S axis
B proof_mode
L witness_id lift_hash
```

where:

- `S` = split;
- `B` = base-pruned leaf;
- `L` = lift-closed leaf.

Lift stream:

```text
S axis
P proof_mode
```

where every leaf of the final tree must be:

`P`

.

---

# 18. Certificate package manifest

Every package contains at least:

```text
manifest.json
base_tree.bin
base_tree.sha256

witness_catalog.json

lift/
    <base_cell_id>/
        witness_id.txt
        lift_tree.bin
        lift_tree.sha256
        verification_summary.json

arithmetic/
    fp_error_policy.json

verification/
    verifier_version.txt
    final_summary.json
```

Search logs may be stored separately, but they are not part of the theorem-critical path.

---

# 19. Root-domain constants for $T_1=0.8350$

## Base

$$
\boxed{
t_3
=
0.194856180909
}
$$

$$
\boxed{
t_5
=
0.197820670401
}
$$

$$
\boxed{
\phi_5
\in
[0,2\pi/5).
}
$$

---

## B7

$$
\boxed{
R_7
\approx
0.512858431636
}
$$

$$
\boxed{
t_7
=
0.196935046771
}
$$

$$
\boxed{
\phi_7
\in
[0,2\pi/7).
}
$$

---

# 20. Milestone headroom audit

official three-body outer ceiling:

$$
A_3^{\mathrm{ceil}}
=
0.834781190917.
$$

milestone:

$$
T_1
=
0.835.
$$

required strict increase:

$$
\boxed{
T_1-A_3^{\mathrm{ceil}}
=
0.000218809083.
}
$$

official full four-body search-only ceiling:

$$
A_{357}^{\mathrm{search}}
=
0.836494901.
$$

search headroom above milestone:

$$
\boxed{
A_{357}^{\mathrm{search}}
-
T_1
=
0.001494901.
}
$$

ratio:

$$
\frac{
0.001494901
}{
0.000218809083
}
\approx
6.83.
$$

So the search evidence shows that the milestone is not sitting right against the four-body numerical ceiling.

But this is not a proof of feasibility.

---

# 21. Base-first scheduler

Proposed:

```text
QUEUE <- base root

while QUEUE not empty:
    C <- pop highest-priority base cell

    if base_lower(C) >= T:
        emit BASE-PRUNED
        continue

    if width(C) > h_base:
        split base cell
        continue

    for K in witness_priority_pool:
        result = try_close_full_witness_root(C, K)

        if result == CLOSED:
            emit LIFT-CLOSED(K, certificate)
            break

    if no witness closes C:
        if width(C) > h_base_min:
            split C
        else:
            emit COMPUTE-DEFERRED / unresolved
```

The final theorem certificate may not contain `unresolved`.

The search phase may.

---

# 22. Witness-first local scheduler

For a fixed base cell:

```text
try_close_full_witness_root(C, K):

    queue <- witness root

    while queue:
        B <- pop

        if apriori_bound(C, B) >= T:
            prune

        elif common_core_hull_lower(C, B) >= T:
            prune

        elif width(B) <= h_lift_min:
            FAIL
            return UNRESOLVED

        else:
            split witness box

    return CLOSED
```

---

# 23. Why failure of B7 on a coarse base cell is not evidence against B7

If the B7 local tree, on the base cell:

$$
C
$$

leaves behind an unresolved lift leaf, this can only mean:

> at the current base-cell / lift-box resolution, the common-core bound is not strong enough.

It does not mean that there actually exists:

$$
q\in C
$$

such that:

$$
J_{B_7}(H(q))<T_1.
$$

The correct order is:

1. refine the witness boxes;
2. refine the base cell;
3. improve the common-core representation;
4. improve the arithmetic;
5. and only as a last resort mark B7 as a cell failure.

---

# 24. Certified negative result for one witness

To actually prove that:

$$
B_7
$$

cannot close some base region on its own, it is not enough to rely merely on the failure of a lower certificate.

One needs to find an explicit:

$$
q\in C
$$

and:

$$
g_7
$$

such that:

$$
\operatorname{Area}
\operatorname{conv}
(
H_{\mathcal F_3}(q)
\cup
g_7B_7
)
<
T_1.
$$

and then verify with a rigorous outer hull area that:

$$
<T_1.
$$

Only then is:

`B7-CELL-COUNTEREXAMPLE`

obtained. Otherwise, only record:

`B7-NOT-YET-CERTIFIED`

---

# 25. General witness core verifier

For `CERTIFIED-SUPPORT-CORE`:

one needs to prove:

$$
h_C(u)+\delta
\le
h_{K_0}(u)
$$

for:

$$
u\in S^1.
$$

Round 03 already has a finite support-direction certificate.

So the verifier can nest a:

$$
\boxed{
\text{Core Inclusion Certificate}
}
$$

whose output is:

$$
\eta_{\mathrm{core}}
\le0.
$$

provided:

$$
\max_u
[
h_C(u)+\delta-h_{K_0}(u)
]
\le0.
$$

This fully plugs Round 02's Fourier witnesses into Round 08.

---

# 26. Safety margins

The final leaf acceptance condition should not be written as:

$$
A_{\mathrm{num}}\ge T.
$$

but rather as:

$$
\boxed{
A_{\mathrm{num}}
-
e_{\mathrm{geom}}
-
e_{\mathrm{fp}}
\ge
T.
}
$$

where:

- $e_{\mathrm{geom}}$: a one-sided geometric deficit, if the inner-boundary sampling is not exact;
- $e_{\mathrm{fp}}$: the floating-point error bound.

If verified inner points are used directly:

$$
e_{\mathrm{geom}}=0
$$

relative to that inner polygon — but the gap from the curved core to the inner polygon is already a one-sided deficit in the safe direction, so it needs no compensation.

The search emitter may use the exact core hull plus this deficit to speed things up, but the verifier's acceptance is based on its own one-sided quantity.

---

# 27. Independent verifier should be intentionally weaker than search

This is an important advantage of the Mishra 2026 proof architecture, and this round preserves it.

The search may prune a leaf because:

$$
L_{\mathrm{search}}
\ge
T+\Delta.
$$

The verifier need only prove:

$$
L_{\mathrm{verify}}
\ge
T.
$$

If:

$$
L_{\mathrm{verify}}
\le
L_{\mathrm{search}},
$$

and the gap has an explicit bound:

$$
\Delta,
$$

the proof still holds.

Hence the verifier does not need to replicate the search's most complex hull machinery.

---

# 28. Generic certificate theorem for arbitrary witness catalog

Let:

$$
\mathcal K_{\mathrm{cat}}
$$

be a finite witness catalog.

Every witness has:

1. a legal diameter-one / constant-width proof;
2. its full relevant placement root;
3. a common-core provider;
4. an independent core verifier.

If every retained leaf of the base atlas is fully closed by some witness in the catalog, then:

$$
\boxed{
\Lambda
\left(
\mathcal F_3
\cup
\mathcal K_{\mathrm{used}}
\right)
\ge
T_1.
}
$$

So the certificate itself does not need to fix in advance that:

$$
B_7
$$

will necessarily succeed.

---

# 29. $B_7$ first, Fourier fallback

Round 08 proposes the following witness priority:

1. $B_7$;
2. $B_{11}$;
3. $B_{13}$;
4. $B_9$;
5. the low-degree asymmetric Fourier dictionary;
6. adaptive target-oracle output.

This ordering affects only efficiency, not correctness.

Round 07's fixed-seed search ranking is merely a priority signal.

---

# 30. Certificate-size control

If every base cell stores a complete witness tree, there may be a great deal of duplication.

Deduplication is possible:

if multiple base cells share exactly the same:

- witness id;
- base core signature;
- witness root;
- split pattern;

they can be hash-consed.

But the verifier must still be able to confirm that the certificate reference is valid for that base cell.

So the dedup key must include at least:

$$
\boxed{
\text{base-cell geometry hash}.
}
$$

It cannot be shared based on the witness-tree bytes alone.

---

# 31. Formal proof obligations for implementation

Before local implementation, each of the following functions must be tagged with its proof role.

## `base_box_lower(C)`

Requirement:

$$
\le
\inf_{q\in C}
A_{\mathcal F_3}(q).
$$

## `motion_delta(B,K)`

Requirement:

$$
\ge
\sup_{g\in B}
d_H(gK,g_0K).
$$

## `core(K_0,\delta)`

Requirement:

$$
C+\delta B\subseteq K_0.
$$

## `lift_box_lower(C,B,K)`

Requirement:

$$
\le
\inf_{q\in C,g\in B}
\operatorname{Area}
\operatorname{conv}
(
H_{\mathcal F_3}(q)
\cup
gK
).
$$

## `split(parent)`

Requires that the union of children covers the parent.

## `root_domain(K,T)`

Requires that every placement that could possibly make the area:

$$
<T
$$

lies within the root.

If any obligation is not proved:

`NOT PROOF PATH`

---

# 32. Local compute handoff specification

This round's package includes:

`AMRAL_LUC_FC_Round_08_LOCAL_COMPUTE_SPEC.json`

The first formal run on the local end:

```text
TARGET = 0.8350
BASE = D + B3 + B5
PRIMARY_WITNESS = B7

BASE:
    build threshold atlas
    use official domain / erosion
    retain only unresolved sublevel cells

LIFT:
    for each retained base cell:
        run complete B7 3-D conditional lift tree

OUTPUT:
    base_manifest
    retained_cells
    per-cell B7 verdict
    lift tree hashes
    unresolved cells
    node counts
    worst verified slack
```

If unresolved cells > 0:

only then does the second stage launch the fallback witness pool.

---

# 33. Prototype / sanity tests included in package

This round includes two code-level tests.

## S1 — General common-core random support check

Uses the analytic constant-width support:

$$
h(\theta)
=
\frac12
+
0.02\cos3\theta.
$$

curvature:

$$
h+h''
=
\frac12
-
0.16\cos3\theta
\ge0.34.
$$

Build a small placement box.

Take:

$$
C
$$

with support:

$$
h_C
=
h_{K_0}-\delta.
$$

Since the curvature margin:

$$
0.34-\delta>0,
$$

$C$ is legal.

Randomly draw box placements and verify:

$$
h_C\le h_{K_g}.
$$

---

## S2 — B7 root constants

Verify:

$$
R_7,
$$

$$
t_7(0.8350),
$$

and:

$$
2\pi/7.
$$

---

# 34. COMPUTE-DEFERRED

## C08-1 — Base atlas emission

Actually generate:

$$
\mathcal A_{0.835}.
$$

## C08-2 — B7 conditional-lift run

Run the full B7 root on every retained base cell.

## C08-3 — Independent replay

After the search completes, replay it with an independent verifier.

## C08-4 — Fallback batch

Run the other witnesses only on cells that B7 did not close.

## C08-5 — Full package checksum

Generate:

- source hashes;
- certificate hashes;
- the manifest;
- the environment lock;
- the replay command.

---

# 35. Round 09 Assigned Topic

## AMRAL-LUC-FC-R09
### Adaptive Atlas Refinement and Certificate-Cost Minimization

If the heavy compute has not yet come back:

Round 09 may continue studying how to reduce:

- base retained cells;
- lift tree size;
- witness trials;
- verifier cost.

Focus points:

1. lower-bound-aware base split;
2. margin-aware witness split;
3. support-signature clustering;
4. symmetry quotient;
5. branch reuse;
6. certificate complexity theorem.

If the local end has already reported back:

directly ingest:

$$
\mathcal A_{0.835}
$$

and the B7 lift results, and begin closure / counterexample analysis.

---

# 36. Reproducibility checklist

## Generic convex motion bound

`PROVED`

## General common-core theorem

`PROVED`

## Reuleaux erosion as specialization

`PROVED`

## Generic Fourier/asymmetric witness interface

`PROVED AS CERTIFICATE INTERFACE`

## Nested base/lift soundness

`PROVED`

## B7 $0.8350$ root domain

`FIXED`

## Certificate grammar

`SPECIFIED`

## Independent verifier invariants

`SPECIFIED`

## General common-core sanity

`PASS`

## $0.8350$ lower bound

`NOT YET CERTIFIED`

---

# 37. Shortest Handoff Conclusion

Round 08 completes:

$$
\boxed{
\text{base 5-D atlas leaf}
\to
\text{one local 3-D witness tree}
\to
\text{independent lower certificate}.
}
$$

More importantly:

$$
\boxed{
\text{Reuleaux-specific erosion}
\to
\text{generic convex common-core interface}.
}
$$

So future witnesses are no longer restricted to:

$$
B_7,B_9,\ldots
$$

and can instead plug directly into the whole of Round 02's legal constant-width dictionary.

The proof condition for the first actual milestone is now fully fixed:

> For every base-atlas leaf of $D+B_3+B_5$ with $A<0.8350$, there must be either `BASE-PRUNED` or at least one complete, valid witness lift certificate.

Once all leaves are closed:

$$
\boxed{
a_{\mathrm{Leb}}\ge0.8350.
}
$$

The heavy computation is currently still marked:

`COMPUTE-DEFERRED`

The atlas/lift computation that has not been run is not being written up as a proved result.

---

# References

1. U. Mishra, *Curves of constant width and Lebesgue's covering problem*, arXiv:2608.30538, 2026.
2. U. Mishra, `Ujjwal238/universal-cover-problem`, official public source repository, 2026.
3. P. Gibbs, *An Upper Bound for Lebesgue's Covering Problem*, arXiv:1810.10089, 2018.
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–07*, 2026-09-18.

---

# 38. Declaration

This round does not claim that:

- $a_{\mathrm{Leb}}\ge0.8350$ has been proved;
- B7 has closed the entire base sublevel atlas;
- the generic support-core verifier has completed formal proof-assistant verification;
- the local atlas / lift certificate has actually finished running.

What this round completes is:

$$
\boxed{
\text{Conditional Lift}
\to
\text{a complete certificate architecture}.
}
$$

So from now on, local-end output can be directly classified as:

- theorem-critical certificate;
- search-only data;
- unresolved computation;

rather than remaining all mixed together.