HANDOFF_B05.md
IUT Valuation Hulls
HANDOFF_B05.md
1 # B05 continuation handoff
2
3 **Accepted checkpoint:** B05; 28 Lean modules + one entry point, 5 new modules,
4 3 negative controls rejected. `verification/b05/verification.json` is the
5 current verification record. The user has expressed an interest in actually
6 bridging Komorebi to Mochizuki's Hodge theaters, not merely analogy.
7
8 ## Confirmed results
9
10 * Local unit saturation iff identical valuation level.
11 * Local nonzero O-multiplier saturation iff reachable at equal/deeper valuation.
12 * Strictly shallower pilot excluded from both closures.
13 * Minimal exponent cost to adjoin a pilot = `a-min(a,b)`; sharp.
14 * For weights s>=1 and depth m, exact total cost `m Σ(s-1)`.
15 * F17 marked reduct plus 1+1 anchor does not determine 1+2; verified field laws.
16 * A discrete approximate witness transfers the scalar upper bound with exact
17 additive loss; witnesses must match the same branch and normalization.
18
19 ## Source-required obligations, unchanged
20
21 Neither the original theta prime-strips and Kummer maps, nor the actual
22 holomorphic hull/determinant/procession normalization, have been instantiated.
23 `IUT312.SourceWitnessTheorem` has no genuine IUT proof term. The existing
24 finite countermodel is not a counterexample to IUT. No abc proof or refutation.
25
26 ## Decisive next mathematical task
27
28 Use the original IUT III Remark 3.9.5(vii) (Ob1–Ob9), Theorem 3.11,
29 Remark 3.11.1, and Corollary 3.12 Step (xi-c)–(xi-f). Build a theorem about the
30 *actual* source-defined possible regions `Pβ` and the construction `φ(P_B)`.
31 Show precisely how the local unit or log-link indeterminacy acts on that hull,
32 and compute the output normalized log-volume before invoking the fixed q-pilot.
33 Then prove the q-pilot scalar is attained, approximated cofinally, or reached
34 with a controlled loss **in the same branch**. A source-backed IPL/SHE/APT
35 certificate must not be treated as a scalar witness by itself.
36
37 This source-instantiation task is the actual research frontier. If it cannot be
38 closed, record the exact missed compatibility and never claim that the small
39 algebraic models settle the original IUT proof.
40
41 ## Verification caveat
42
43 The legacy sequential B03 verification attempt timed out while individually
44 checking files after successfully completing its clean Lake build. A complete
45 B05 parallel per-file audit then ran to completion with all source, compiler,
46 contract, and negative-control checks passing. See logs. The first aborted
47 F17 brute-force draft was replaced by generic algebraic transport lemmas.