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

**文件代號：** AMRAL-LUC-FC-R08  
**版本：** v0.1  
**日期：** 2026-09-18  
**研究狀態：** Round 08 / Conditional-lift proof compiler / Certificate grammar  
**研究模式：** Human-Directed + Semi-Autonomous AI Mathematical Research  
**研究發起與方法論來源：** Neo.K  
**AI 協力研究者與主要執行者：** Aletheia / ChatGPT, GPT-5.6 Sol  
**母方法論：** Relational Constraint–Handoff Methodology (RCHM)  
**前置文件：** AMRAL-LUC-FC-R00 v0.2；R01–R07 v0.1  

---

# 0. 本輪摘要判定

Round 07 已把第一個實際 improvement milestone 固定為：

$$
T_1=0.8350,
$$

並將 base family：

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

的五維 sublevel region：

$$
\mathcal Q_{<T_1}
$$

改寫為 threshold-conditioned minimizer atlas。

Round 08 的任務不是宣稱大型 atlas 已經完成，而是建立：

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

的完整 proof grammar。

本輪得到以下主要結果。

---

## 結論 A：Mishra erosion lemma 可抽象成一般 convex common-core theorem

令：

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

為 compact convex witness。

固定同一 reflection branch，考慮 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].
$$

box-center placement：

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

任意 box placement：

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

則：

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

若 convex core：

$$
C
$$

滿足：

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

則：

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

這是一般化 common-core theorem。

---

## 結論 B：Reuleaux erosion 是一般 common-core theorem 的特例

若：

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

為 width-one Reuleaux polygon，則：

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

滿足：

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

所以官方 erosion core：

$$
1\mapsto1-\delta
$$

正是一般 common-core theorem 的 closed-form specialization。

---

## 結論 C：Round 02 的一般 Fourier / asymmetric witnesses 也能使用同一 lift machinery

對一般 convex witness，不要求一定是 Reuleaux polygon。

Verifier 只需收到：

1. box-center body $K_0$；
2. motion radius $\delta$；
3. 一個 candidate inner core $C$；
4. 一個可獨立驗證的 inclusion certificate：

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

即可推出：

$$
C
$$

是整個 placement box 的共同內核。

因此 fallback witnesses 可來自：

- regular Reuleaux odd-gons；
- irregular Reuleaux polygons；
- Round 02 finite Fourier dictionary；
- asymmetric constant-width bodies。

不需要另外發明一套 witness-specific proof logic。

---

## 結論 D：建立 nested base/lift certificate theorem

對每個 base atlas leaf：

$$
C_j,
$$

final certificate 必須屬於兩種之一。

### `BASE-PRUNED`

base family common-core lower bound已：

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

### `LIFT-CLOSED`

存在一個 witness：

$$
K_j
$$

與一棵 finite local lift tree，使 witness placement root domain全部被覆蓋，且每一個 lift leaf的：

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

rigorously：

$$
\ge T_1.
$$

若所有 base leaves 均合法分類，則：

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

---

## 結論 E：建立 independent certificate grammar

final proof package 不允許存在：

- unclassified base leaf；
- unresolved lift leaf；
- missing witness subtree；
- unverified root domain；
- search-only numerical value。

Verifier 必須獨立重建：

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

---

## 結論 F：B7 的 $0.8350$ lift root 已固定

對 regular Reuleaux $B_7$：

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

由 Round 07 的 threshold-dependent a-priori domain：

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

即可覆蓋所有可能使 hull area低於：

$$
0.8350
$$

的 $B_7$ translations。

rotation symmetry：

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

因此每個 hard base cell只需啟動固定的三維 local root：

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

---

## 結論 G：$0.8350$ 的幾何 headroom 足以作第一個 milestone，但尚未證

官方三體 rigorous outer ceiling：

$$
0.834781190917.
$$

所以只需增加：

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

即可超過 milestone。

官方四體：

$$
D+B_3+B_5+B_7
$$

search-only optimum：

$$
0.836494901
$$

比 milestone高：

$$
\boxed{
0.001494901.
}
$$

這提供 numerical headroom，但不是 proof。

---

本輪總判定：

$$
\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. 一般 placement-box motion bound

令：

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

考慮同一 reflection component 中：

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

與：

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

假設：

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

以及：

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

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

對任意：

$$
x\in K,
$$

有：

$$
\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}
$$

所以：

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

這正好重現官方 Reuleaux box erosion使用的位移界。

---

# 2. General Convex Common-Core Theorem

## 定理 2.1

令：

$$
K_0
$$

與 placement box中所有：

$$
K_g
$$

滿足：

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

若 compact convex：

$$
C
$$

滿足：

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

則：

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

對 box 中所有 placement 成立。

### 證明

Hausdorff inequality 對 convex support functions 等價於：

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

對所有：

$$
u\in S^1.
$$

所以：

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

另一方面：

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

等價於：

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

故：

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

對所有 $u$。

由 support-function containment：

$$
C\subseteq K_g.
$$

Q.E.D.

---

# 3. Core interface 不要求顯式 Minkowski erosion

概念上可寫：

$$
K_0\ominus\delta B.
$$

但 computational verifier 不必真的算出 exact erosion。

只要提供任意：

$$
C
$$

滿足：

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

即可。

因此 core provider 可分三類。

---

## `REULEAUX-EROSION`

對：

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

直接：

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

Verifier 必須重算：

- nonempty condition；
- circle-circle intersections；
- all-disk membership。

---

## `ANALYTIC-SUPPORT-CORE`

若：

$$
h_K-\delta
$$

本身已知為合法 support function，可直接用。

例如 Round 02 安全 interiorized trigonometric bodies，在 curvature margin 足夠大時可使用此路徑。

---

## `CERTIFIED-SUPPORT-CORE`

任意 finite representation的 convex：

$$
C
$$

只要另附：

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

的 Round 03-type finite support certificate。

因此 generic witness interface 不依賴 Reuleaux closed form。

---

# 4. Reuleaux specialization

width-one regular / irregular Reuleaux polygon：

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

令：

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

定義：

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

若：

$$
x\in C_\delta
$$

且任意：

$$
z\in\delta B,
$$

則對所有：

$$
j,
$$

有：

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

所以：

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

即：

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

由 General Convex Common-Core Theorem：

$$
C_\delta
$$

是整個 placement box 的共同內核。

---

# 5. Base cell common cores

base family：

$$
D+B_3+B_5.
$$

對 base box：

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

令：

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

為 $B_3$ translation halfwidth。

因 $B_3$ orientation fixed：

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

對 $B_5$：

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

共同內核：

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

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

Reuleaux closed form時就是 defining disk radii：

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

---

# 6. B7 local lift root

對 milestone：

$$
T_1=0.8350,
$$

Round 07 已得到：

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

rotation symmetry：

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

因此 local root box可取：

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

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

square corners雖有：

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

但這些 points 本身已由 a-priori area bound排除，不會破壞 soundness。

也可在 local search 中加 radial prune。

---

# 7. B7 lift-box core

對 lift box中心：

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

與 halfwidths：

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

令：

$$
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).
}
$$

若此 intersection empty：

不能使用 hull-core prune。

此 leaf 必須：

- split；
- 或用 a-priori area bound；
- 或改用其他 witness。

---

# 8. Combined lift lower bound

對 base cell：

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

與 B7 placement box：

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

任意 actual configuration 的 hull 都包含：

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

所以：

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

因此只要 verifier 能證：

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

整個：

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

即可 prune。

---

# 9. Inner-point lower witness

為避免 verifier依賴 search 的 exact hull routine，可對每個 curved core只取 verified boundary inner points：

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

令：

$$
P_D
$$

為 disk 的 inscribed polygon。

則：

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

所以其 polygon hull area：

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

是 rigorously one-sided lower witness。

若 floating arithmetic誤差上界：

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

已被獨立估計，leaf acceptance condition 可直接寫成：

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

這比依賴 emitter exact-area value更乾淨。

---

# 10. Base tree grammar

final certificate 的 base tree使用 deterministic binary split。

每個 node 只有以下類型。

## `SPLIT`

記錄：

- split axis；
- split rule version；
- children implicit。

## `BASE-PRUNED`

verifier 重算 base common-core lower bound並檢查：

$$
\ge T_1.
$$

## `LIFT-CLOSED`

記錄：

- witness id；
- lift-certificate hash；
- witness root domain id。

final certificate 不允許：

`UNRESOLVED`

leaf。

---

# 11. Lift tree grammar

每個：

`LIFT-CLOSED`

base leaf指向一棵 local witness tree。

local node：

## `SPLIT`

split one witness placement dimension。

## `PRUNED`

verifier重算：

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

final lift tree不允許：

- stuck leaf；
- missing child；
- unconsumed stream；
- unknown witness id。

---

# 12. Nested Certificate Soundness Theorem

## 定理 12.1

若：

1. base root domain覆蓋所有可能使 base hull：

   $$
   <T_1
   $$

   的 base placements；

2. base tree deterministic partition root；

3. 每個 base leaf為：

   - valid `BASE-PRUNED`；或
   - valid `LIFT-CLOSED`；

4. 對每個 `LIFT-CLOSED` leaf，其 referenced witness lift tree覆蓋該 witness的全部 relevant placement root；

5. 每個 lift leaf都有 valid common-core lower witness：

   $$
   \ge T_1;
   $$

6. 所有 tree streams完整消耗，沒有 missing / unclassified node；

則令：

$$
\mathcal B
$$

為 certificate 中實際被使用的所有 witnesses，

有：

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

### 證明

任取 full family placement。

其 base projection落在某 base leaf。

若 leaf：

`BASE-PRUNED`，

則 base hull已：

$$
\ge T_1.
$$

full hull更大。

若 leaf：

`LIFT-CLOSED`

with witness $K$，該 full placement中 $K$ 的 placement 必落在 lift tree某 leaf。

該 leaf common core包含於所有對應 actual bodies。

所以 full hull包含 verifier 的 inner hull witness，area：

$$
\ge T_1.
$$

任意 full placement皆成立。

Q.E.D.

---

# 13. Multi-witness fallback 不增加 joint dimension

假設某 base cell不能被：

$$
B_7
$$

單獨 close。

可：

1. 先 split base cell；
2. 對 child cells再次試：

   $$
   B_7;
   $$

3. 對仍失敗 children再試：

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

只要每個 final base leaf被至少一個 witness的完整 3-D root close：

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

不需要建立：

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

的 joint Cartesian product。

---

# 14. Generic witness catalog interface

每個 witness record至少包含：

```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 provider：

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

這使 verifier無需知道 witness是如何被 search 選中的。

---

# 15. Search emitter 與 verifier 的權責分離

## Search emitter 可以：

- 使用 exact hull routine；
- 使用 heuristic priority；
- 用 floating optimizer找 witness；
- 用 cache；
- 使用 parallel scheduling；
- 猜下一個 split axis。

## Independent verifier 只能依賴：

- certificate bytes；
- public mathematical constants；
- independent core reconstruction；
- deterministic split rule；
- simple convex hull / shoelace；
- rigorous floating / interval error；
- cryptographic hashes。

所以：

$$
\boxed{
\text{search can be smart and complex；
verifier 必須簡單且 independent}.
}
$$

---

# 16. Verifier invariants

final verifier至少檢查：

## V1 — Header

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

## V2 — Base root coverage

檢查 translation domain不小於：

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

rotation：

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

## V3 — Witness root coverage

對 $B_7$：

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

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

## V4 — Split coverage

children union必須覆蓋 parent。

不可有 gap。

## V5 — Common-core validity

重新計算：

$$
\delta_i.
$$

對 Reuleaux：

- core radius positive；
- nonempty；
- reconstructed corners位於全部 defining disks。

對 generic support core：

- 驗證：

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

## V6 — Inner witness validity

所有 polygon witness points確實位於 common core。

## V7 — Area

重新算 convex hull。

接受條件：

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

## V8 — Tree structure

對 binary tree：

$$
N=2L-1
$$

若 single root。

對 seed forest：

$$
N=2L-S
$$

其中 $S$ 是 seed count。

## V9 — Exhaustion

bit / tag stream必須恰好消耗完。

## V10 — Base-leaf completeness

每個 base leaf必須：

- base-pruned；或
- 引用一個 valid lift tree。

---

# 17. Certificate stream proposal

本輪不綁死 binary encoding，但固定 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
```

其中：

- `S` = split；
- `B` = base-pruned leaf；
- `L` = lift-closed leaf。

Lift stream：

```text
S axis
P proof_mode
```

其中 final tree全部 leaf都必須：

`P`

。

---

# 18. Certificate package manifest

每個 package至少：

```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可另外保存，但不屬 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.
$$

所以 search evidence顯示 milestone不是貼著四體 numerical ceiling。

但這不是 proof of feasibility。

---

# 21. Base-first scheduler

建議：

```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
```

final theorem certificate不能含 unresolved。

search phase可以。

---

# 22. Witness-first local scheduler

對 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

若 B7 local tree在 base cell：

$$
C
$$

留下 unresolved lift leaf，只能表示：

> 在目前 base-cell / lift-box resolution下，common-core bound不夠強。

不代表存在 actual：

$$
q\in C
$$

使：

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

應依序：

1. refine witness boxes；
2. refine base cell；
3. improve common-core representation；
4. improve arithmetic；
5. 最後才把 B7標為 cell failure。

---

# 24. Certified negative result for one witness

若要真的證：

$$
B_7
$$

無法單獨關閉某 base region，不能只靠 lower certificate失敗。

需要找一個 explicit：

$$
q\in C
$$

與：

$$
g_7
$$

使：

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

再用 rigorous outer hull area驗證：

$$
<T_1.
$$

此時才得到：

`B7-CELL-COUNTEREXAMPLE`

否則只記：

`B7-NOT-YET-CERTIFIED`

---

# 25. General witness core verifier

對 `CERTIFIED-SUPPORT-CORE`：

需要證：

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

對：

$$
u\in S^1.
$$

Round 03 已有 finite support-direction certificate。

所以 verifier可嵌套：

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

其輸出為：

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

只要：

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

這就把 Round 02 Fourier witnesses完整接入 Round 08。

---

# 26. Safety margins

final leaf acceptance不應寫：

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

而應寫：

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

其中：

- $e_{\mathrm{geom}}$：若 inner boundary sampling未精確，為 one-sided geometric deficit；
- $e_{\mathrm{fp}}$：floating error bound。

若直接使用 verified inner points：

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

相對於該 inner polygon，但 curved core到 inner polygon的差本來就是往下，不需補。

search emitter可以利用 exact core hull + deficit加速，但 verifier acceptance以自身 one-sided quantity為準。

---

# 27. Independent verifier should be intentionally weaker than search

這是 Mishra 2026 proof architecture 的重要優點，本輪保留。

search 可 prune leaf因：

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

verifier只需證：

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

若：

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

且差距有 explicit bound：

$$
\Delta,
$$

proof仍成立。

因此 verifier不必複製 search 最複雜的 hull machinery。

---

# 28. Generic certificate theorem for arbitrary witness catalog

令：

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

為 finite witness catalog。

每個 witness都具備：

1. legal diameter-one / constant-width proof；
2. full relevant placement root；
3. common-core provider；
4. independent core verifier。

若 base atlas每個 retained leaf都被 catalog某個 witness完整 close，則：

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

所以證書本身不需要預先固定：

$$
B_7
$$

一定成功。

---

# 29. $B_7$ first, Fourier fallback

Round 08 建議 witness priority：

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

此順序只影響效率，不影響 correctness。

Round 07 fixed-seed search ranking只是 priority signal。

---

# 30. Certificate-size control

如果每個 base cell都保存完整 witness tree，可能重複很多。

可做 dedup：

若多個 base cells共用完全相同：

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

可 hash-cons。

但 verifier必須仍能確認 certificate reference 對該 base cell有效。

所以 dedup key至少包含：

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

不能只按 witness tree bytes共用。

---

# 31. Formal proof obligations for implementation

本地端實作前，必須把下列函數各自標記 proof role。

## `base_box_lower(C)`

要求：

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

## `motion_delta(B,K)`

要求：

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

## `core(K_0,\delta)`

要求：

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

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

要求：

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

## `split(parent)`

要求 children union覆蓋 parent。

## `root_domain(K,T)`

要求所有 placement可能使 area：

$$
<T
$$

者均在 root內。

任一 obligation 未證：

`NOT PROOF PATH`

---

# 32. Local compute handoff specification

本輪 package附：

`AMRAL_LUC_FC_Round_08_LOCAL_COMPUTE_SPEC.json`

本地端第一個正式 run：

```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
```

若 unresolved cells > 0：

第二階段才啟動 fallback witness pool。

---

# 33. Prototype / sanity tests included in package

本輪附兩個 code-level tests。

## S1 — General common-core random support check

使用 analytic constant-width support：

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

curvature：

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

建立小 placement box。

取：

$$
C
$$

support：

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

因 curvature margin：

$$
0.34-\delta>0,
$$

$C$ legal。

隨機抽 box placements，驗：

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

---

## S2 — B7 root constants

驗：

$$
R_7,
$$

$$
t_7(0.8350),
$$

以及：

$$
2\pi/7.
$$

---

# 34. COMPUTE-DEFERRED

## C08-1 — Base atlas emission

真正生成：

$$
\mathcal A_{0.835}.
$$

## C08-2 — B7 conditional-lift run

每個 base retained cell跑 full B7 root。

## C08-3 — Independent replay

search 完成後由獨立 verifier重播。

## C08-4 — Fallback batch

只有 B7未關閉 cells才跑其他 witnesses。

## C08-5 — Full package checksum

生成：

- source hashes；
- certificate hashes；
- manifest；
- environment lock；
- replay command。

---

# 35. Round 09 指定題目

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

如果 heavy compute 尚未回來：

Round 09 可繼續研究如何減少：

- base retained cells；
- lift tree size；
- witness trials；
- verifier cost。

重點：

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。

如果本地端已回傳：

直接 ingest：

$$
\mathcal A_{0.835}
$$

與 B7 lift結果，開始 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. 最短交接結論

Round 08 完成：

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

更重要的是：

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

所以 future witnesses 不再受限於：

$$
B_7,B_9,\ldots
$$

而可以直接接 Round 02 的全部 legal constant-width dictionary。

第一個實際 milestone的 proof condition現在完全固定：

> 對 $D+B_3+B_5$ 的每個 $A<0.8350$ base atlas leaf，必須有 `BASE-PRUNED` 或至少一個完整 valid witness lift certificate。

全部 leaf閉合後：

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

目前 heavy computation仍標：

`COMPUTE-DEFERRED`

沒有把未跑的 atlas / lift計算寫成已證結果。

---

# 參考文獻

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. 宣告

本輪沒有宣稱：

- $a_{\mathrm{Leb}}\ge0.8350$ 已證；
- B7 已關閉全部 base sublevel atlas；
- generic support-core verifier 已完成正式 proof-assistant verification；
- local atlas / lift certificate 已實際跑完。

本輪完成的是：

$$
\boxed{
\text{Conditional Lift}
\to
\text{完整 certificate architecture}.
}
$$

因此之後本地端的輸出可以被直接判斷為：

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

而不再混在一起。