Ledger: M4b now BUILT (was confirmed-classical) in 04 and 06

Author: Hdpbilly

docs/adelic-machine/04-coupling-invariant.md

@@ -214,14 +214,13 @@ one — the actual research contribution, or the place the approach stalls.
   *value-identified* product-formula theorem, because it reduces to unique
   factorization + the existing congruence certificate (exact only because the value
   is identified).
-- **Plausibly formalizable, classical (📊 confirmed, was "the prize/stall"):** **M4b** —
-  the finite-precision gauge bound over *live* prefixes (§3.3). The scratch probe
-  settled it: the deviation is `Θ(1/q_n²)` with effective `C = 1` (Hurwitz), so M4b is
-  *reachable* — but it reduces to the classical CF convergent bound (the non-Arch legs
-  are exact constants), so it is **mechanical** Lean labor, not research. Formalization
-  handle: the FDRS `bracket_invariant` (`|det| = 1`) gives `|p_n/q_n − p_{n-1}/q_{n-1}|
-  = 1/(q_n q_{n-1})`, chained to the convergent bound; `steps_qCur_unbounded` gives
-  `q_n → ∞`; the non-Arch factor is the exact product-formula constant `1/|x|`.
+- **BUILT ✅ (was "the prize/stall", now machine-checked):** **M4b** — the finite-precision
+  gauge bound `| |p_n/q_n|·P − 1 | ≤ P/q_n` (`GaugeBound.lean`: `gauge_bound`, +
+  `gauge_product_tendsto` for `Π_n → 1`). The scratch probe settled the shape (`Θ(1/q_n²)`,
+  `C = 1`, Hurwitz); the Lean proof assembles Mathlib's `abs_sub_convs_le` (whose own proof
+  goes through `fib(n+2) ≤ denom` — the gauge growth, FDRS's `steps_qCur_unbounded` /
+  `bracket_invariant` in Mathlib form) + the product-formula constant `P`. It **is** the
+  classical CF convergent bound in adelic costume — mechanical assembly, not new math.
 - **Genuinely open / may not work:** any *additive* coupling law (§3.2 boundary); the
   full restricted-product (L3) version.
 - **The failure mode that did NOT occur:** the worry was that the gauge bound might have

docs/adelic-machine/06-anti-confabulation.md

@@ -103,7 +103,7 @@ classical.
 | read `v_p` off the emitted stream (`padic_valuation_from_stream`) | `06`(this), bridge | ✅ BUILT (`ValuationStream.lean`) |
 | restricted product / genuine adeles | `05` M3 | 🔨/🔬 (optional, after M2/M4a) |
 | **M4a** exact soundness (value identified) | `04`§4, `05` M4a | ✅ BUILT (`product_formula_place`) |
-| **M4b** `gauge_bound` (finite live prefixes) | `04`§3.3, `05` M4b | 📊 CONFIRMED classical (probe: `C=1`, `Θ(1/q_n²)`, Hurwitz) → reachable, mechanical Lean, NOT a stall |
+| **M4b** `gauge_bound` (finite live prefixes) | `04`§3.3, `05` M4b | ✅ BUILT (`GaugeBound.lean`: `gauge_bound`, `gauge_product_tendsto`); classical (Hurwitz), assembled from Mathlib CF + M4a |
 | p²-corner p-adic bihomographic *soundness* (Axis I at `p`) | `03`§3d | 🔨 (algebra ✅ M0a; congruence-trap soundness next) |
 | `ProductFormulaResidual` is symbolic-exponent, **not** `log p` | `03`§6 | 🔨 (NF1: `log p ∉ ℚ`) |