# RUN-034 — Round 31: the second backend's root, marker and 9,278 leaves pass again here, and its lower ledger is Round 30's leaf for leaf — the same polygons, their membership decided again in MPFR; the queue is this tree's atlas; the wrapper rounds its exact inputs to nearest, so §3's directed rule holds for its outputs only

**Arm:** 懸衡 (Xuán Héng) / AMRAL Research Lab
**Date:** 2026-09-27
**Subject:** `AMRAL_Lebesgue_Finite_Closure_Round_31_Cross_Backend_Publication_Candidate_v0.1.md` (AMRAL-LUC-FC-R31, dated 2026-09-20) and its package, read from the archive:

- `MPFR_ROOT_REPLAY.json`, `MPFR_MARKER70_REPLAY.json`, `MPFR_LOWER_REPLAY.json`, `MPFR_BACKEND_LOCK.json`,
  `PUBLICATION_CANDIDATE_SHARD_70.json`, `BULK_MIGRATION_QUEUE.json`, `CORRECTION_LEDGER.json`, `VALIDATION.json`,
  `State_Crystal`;
- the 23 `mpfr_lower_*.json` chunks and the ledger (9,278 leaf records), and Round 27's to Round 30's files again;
- five scripts, read only after this tree's replays were computed, and never run.

**Tools:** [`run034_round31_mpfr_replay.py`](../code/run034_round31_mpfr_replay.py) — RUN-031's directed root and RUN-033's
replays; marker 70's polygon rebuilt from RUN-032's integer-interval support bounds under the package's normals and
ceiling, through an exact polar hull; RUN-030's continuation over RUN-029's atlas for the queue; the corrected exact
kernel
**Logs:** [`run034-round31-mpfr-replay.json`](../data/gate-logs/run034-round31-mpfr-replay.json)

**Verdict: PASS for the root, marker 70's bound and the false negative behind its correction, all 9,278 lower leaves,
the migration queue and the lock. PARTIAL for §3's rule as written: the wrapper loads every exact rational rounded to
nearest, and directs only its results.**

- **The root.**
  - The MPFR bisection starts from T_M = 1673/2000. Its d⋆ bracket is a dyadic interval exactly 2⁻²²¹ wide, and its
    t₃, t₅ and t₇ are 3.1–4.2×10⁻⁶⁷ wide, as stated (d⋆ 2.97×10⁻⁶⁷).
  - The intervals nest. This tree's brackets (about 10⁻⁹⁰, RUN-031) lie inside the A1 replay's (Round 30), those
    inside MPFR's, and MPFR's inside Round 28's, for d⋆ and for each t_n. §0 and §4 say "overlap"; it is containment.
- **Marker 70.**
  - The MPFR record is Round 29's file: density 4,096, area 0.8349075014501105, margin 9.24985499×10⁻⁵.
  - The polygon is rebuilt here from this tree's integer support bounds, under the package's normals
    (round(10⁹·(cos, sin)), reduced by their gcd) and its 10⁻²⁶ ceiling.
    - With every constraint kept, it has 1,317 active constraints, and its exact area's numerator and denominator
      have 22,754 and 22,755 bits. That is the MPFR record, and the A1 replay's count.
    - With the candidates reduced in floating point, as the emitter does, it has 1,284 constraints and 21,944 /
      21,945 bits. That is Round 29's file.
    - The two areas are 3.3×10⁻⁵⁰ apart. So §5's "与 Round29 显示值一致" holds to the displayed digits; beyond them
      the MPFR polygon is the A1 polygon, not Round 29's.
  - The false negative reproduces. Counting the arcs next to the active piece as well gives 0.92016 (1,068 active
    constraints), §6's U ≈ 0.9201: safe, and unable to certify.
- **The 9,278 lower leaves.**
  - The MPFR ledger is Round 30's A1 ledger leaf for leaf: path, density, hull-vertex count and margin, on all 9,278.
    §9 explains the equal histograms by the shared candidate policy. The margins are equal too: the same polygons,
    their membership decided again in MPFR.
  - So the MPFR replay inherits the A1 rule, one contact point per direction, the union winner's. Its thinnest leaf,
    3.5423707501×10⁻⁹ at 2,048, is that rule's loss: the leaf has 2.22×10⁻⁵ with every contact point (RUN-033).
  - This tree's certificate (RUN-033) passes all 9,278 at these densities.
- **The queue.**
  - Its 63 geometry-complete cells are exactly the cells of this tree's atlas that close by depth 40 under the
    package's pad (RUN-029, and RUN-030's continuation). Each is queued at the next even depth at or above its
    closing depth: 7 at 30, 12 at 32, 19 at 34, 13 at 36, 6 at 38 and 6 at 40. That is 51 by 36, 57 by 38 and 63 by
    40: §15's figures.
  - Its 14 residual cells are the 14 still open at 40. The volume and ratio it gives each at its last recorded depth
    (36 for five, 38 for eight, 40 for one) are this tree's continuation's to 10⁻¹², and Round 27's records. At 40
    all 14 still contract (largest V₄₀/V₃₈ 0.6077).
  - Cell 70 comes first, the only publication candidate; the rest follow by depth, then cell number. Every marker
    margin in the queue is null, so nothing in it ranks cells by the margins §17 speaks of.
- **The lock.**
  - Its wrapper digest and four script digests are the shipped files', and every shipped script is pinned.
  - The two library digests are the document's and the shard's. The binaries are not in the archive, so they are
    not checked.
  - Both corrections are CORRECTED: the first a safe-side false negative, the second with no mathematical effect.
- **What the package ships**, read after this tree's rebuild and never run.
  - `r31_mpfr_backend.py` (153 lines) is a ctypes wrapper at 640 bits over 16 MPFR calls.
    - It loads every exact rational rounded to nearest, p and q as integers and then p/q, and directs only the
      result. So §3's "exact Fraction → MPFR directed → exact dyadic Fraction" holds for the outputs, while each input
      sits within 2⁻⁶⁴⁰ of the rational it stands for.
    - An enclosure can therefore miss by up to about 2⁻⁶⁴⁰ relative. Every decision it feeds here has vastly more
      room, so this is covered in practice, but not by construction.
    - Its sine and cosine take the directed values at both ends, plus ±1 wherever a critical point may lie inside.
  - `r31_mpfr_lower_chunk.py` (146 lines) reads the MPFR root, not Round 28's intervals.
    - Three of its functions are A1's, syntax tree for syntax tree: the core support (candidates in binary64), the
      float midpoint and the margin.
    - It keeps the union winner's point per direction, as A1 does.
    - It decodes Round 28's topology and axis stream and asserts only that 9,278 leaves come out.
  - `r31_mpfr_marker70.py` (101 lines) uses 4,096 normals at 10⁹ and the 10⁻²⁶ ceiling, and counts the sectors the
    interval spans. Its comment still says it adds adjacent sectors "defensively": the first version, corrected away.
  - `r31_cross_root.py` (35 lines) bisects from 1673/2000, 220 times.
  - `r31_aggregate.py` (26 lines) globs `mpfr_lower_*.json` in the reference folder, a pattern its own ledger also
    matches. Where chunks overlap, the later file wins. The shipped chunks sit in a subfolder, beside a copy of the
    ledger.
  - Four of the five load from an absolute path.

Drill: 19 / 19 plants caught by exactly the named checks, 4 / 4 controls undisturbed, 207 / 207 must-stay-green
assertions held. Each of the ten checks was blinded in turn, and each was reported blind in exactly as many cases as
plants name it.

This run uses the exact kernel as corrected after RUN-031 (every envelope segment checked in closed form); the
correction is committed before it.

---

## What Round 31 claims

1. **A second backend** (§0–3). No gmpy2, python-flint or Arb binding is available, so libMPFR 4.2.2 and GMP are
   called through a minimal ctypes wrapper: exact loads, directed rounding, the field operations, sqrt, sin, cos,
   acos, atan2, π, comparison, exact dyadic extraction. The rule is exact Fraction → MPFR directed → exact dyadic
   Fraction.
2. **The root** (§4). From T_M = 1673/2000, a monotone directed bisection gives d⋆ about 2.97×10⁻⁶⁷ wide; t₃, t₅, t₇
   all overlap Round 28's intervals.
3. **Marker 70** (§5–6). Only the Reuleaux sector arithmetic moves to MPFR: 0.8349075014501105, as Round 29 shows. A
   first verifier also counted the adjacent pieces and got U ≈ 0.9201, a false negative (R31-MPFR-MARKER-001).
4. **The lower tree** (§7–10). 9,278 / 9,278 pass, none inconclusive; the density histogram is Round 30's, "because
   the finite candidate policy is the same, but the core enclosure backend differs"; the least margin is
   3.5423707501×10⁻⁹.
5. **The gate** (§11–14, §18–19). Two backends and two implementations, strict inequalities and pinned dependencies
   make marker 70's shard a PUBLICATION-CANDIDATE-SHARD: mature enough for a formal proof package or external audit,
   not a proof of the bound, and not a formal verification of the libraries.
6. **The rest** (§15–17, §20–22). Γ(36) = 51/77, Γ(38) ≥ 57, Γ(40) ≥ 63; the geometry-complete cells are queued for
   arithmetic migration, the residual for the B₇ wave; for marker 70, 0 leaves needed a resplit; a_Leb ≥ 0.835 is NOT
   CERTIFIED.

## A — sources

**A0.** 39 anchors. Round 31 has no reference list.

## W — rebuilt

| check | Round 31 | rebuilt | result |
| --- | --- | --- | --- |
| W1 | §0, §4 | the MPFR root between this tree's brackets, the A1 replay's and Round 28's | PASS; nested, a 2⁻²²¹ dyadic d⋆ |
| W2 | §5–6 | marker 70's polygon, three ways | PASS; MPFR = every constraint = A1; Round 29 = float-reduced; 0.92016 reproduced |
| W3 | §7–10 | the MPFR ledger against Round 30's; this tree's certificate | PASS; leaf for leaf, margins included |
| W4 | §15–17 | the queue against this tree's atlas and its continuation | PASS; 63 closed by 40, 14 open, depths and volumes as recorded |
| W5 | §12–13, §20 | the lock against the scripts; the corrections | PASS; the binaries not here |
| W6 | — | the scripts | inputs to nearest; the lower replay shares A1's rule and three functions |

## P — the package

**P1.**

- The 23 chunks cover the 9,278 leaves once, in order. Each summary is its rows', and together they are the ledger,
  whose two shipped copies have one digest.
- The replay file's totals, density counts, least margin and its path are the ledger's, with no missing index.
- The shard record's root flags, path audit, marker figures, and Round 28, Round 30 and Round 31 lower figures are
  the replays'; its backend pair is the Round 30 and Round 31 locks'.
- The residual queue is Round 27's record of the cells without a known complete edge, figure for figure.
- The crystal carries 9278/9278, 3.5423707501×10⁻⁹, both library digests, the shard's status and 51/77.

**P2.**

- `VALIDATION.json` describes the document and the crystal correctly: SHA-256, bytes, `$$` counts, both flags.
- Its eight digests are the archive's, and its twelve checks follow from the data.

## Round 31, read

| Round 31 | statement | verdict | note |
| --- | --- | --- | --- |
| §0, §4 | the MPFR root overlaps Round 28's | PASS | nested: this tree inside A1, A1 inside MPFR, MPFR inside Round 28 (W1) |
| §1–2 | a second backend through a minimal wrapper | PASS | as described (W6) |
| §3 | exact Fraction → MPFR directed → exact dyadic Fraction | PARTIAL | the outputs are directed and read back exactly; the inputs are loaded to nearest (W6) |
| §5 | marker 70's MPFR upper bound, Round 29's value | PASS | the every-constraint polygon, which is A1's; Round 29's is the float-reduced one, 3.3×10⁻⁵⁰ away (W2) |
| §6, §20 | R31-MPFR-MARKER-001 | PASS | 0.92016 reproduced; the script's comment still describes the first version (W2, W6) |
| §7–10 | 9,278 / 9,278; the histogram; the least margin | PASS | Round 30's ledger leaf for leaf; the least margin is the A1 rule's loss (W3) |
| §11–14 | the gate's six conditions; PUBLICATION-CANDIDATE-SHARD | PASS | as the package sets them; this tree's integer replays of the three parts do not rest on either backend |
| §12 | the pins | PASS | the scripts' digests; the libraries' as stated, not checkable here (W5) |
| §15–17 | the global budget; the queue; no resplit | PASS | W4; RUN-031 for the resplit |
| §18–22 | scope; the lattice; Round 32 | PASS / n/a | |

## The status registry

Round 31's 20 judgments are reviewed, and its 3 first-used phrases defined: `R31-MPFR-MARKER-001`,
`ALL LOCAL CONDITIONS MET` and `ARITHMETIC-MIGRATION QUEUE`. Census v5 adds none.

| verdict | judgments |
| --- | ---: |
| PASS | 16 |
| n/a | 4 |

The three PASS reviews of PUBLICATION-CANDIDATE-SHARD carry W6's caveat about the wrapper's inputs.

## The drill

| kind | cases | named checks |
| --- | ---: | --- |
| the document's least margin | 1 | A0 |
| a root interval; the stated width | 2 | W1 |
| marker 70's area | 1 | W2 (also P1) |
| the area's numerator bits | 1 | W2 |
| the thinnest leaf's margin; a leaf's density | 2 | W3 (also P1) |
| this tree's certificate failing a leaf | 1 | W3 |
| a queued cell's depth | 1 | W4 |
| a residual cell's volume | 1 | W4 (also P1) |
| a pinned script digest; a correction's effect | 2 | W5 |
| the scripts' facts | 1 | W6 |
| a chunk's pass count; the shard's MPFR margin; the crystal's 9278/9278 | 3 | P1 |
| a VALIDATION digest; a VALIDATION check | 2 | P2 |
| a review dropped | 1 | R1 |

Four controls:

- the unmodified inputs;
- the document with CRLF line endings;
- the queue with its keys sorted;
- the shard with its keys sorted.

**19 / 19 plants, 4 / 4 controls, 207 / 207 must-stay-green assertions; no check without a plant.**

| check blinded | cases reported blind | plants naming it |
| --- | ---: | ---: |
| A0 | 1 | 1 |
| W1 | 2 | 2 |
| W2 | 2 | 2 |
| W3 | 3 | 3 |
| W4 | 2 | 2 |
| W5 | 2 | 2 |
| W6 | 1 | 1 |
| P1 | 7 | 7 |
| P2 | 2 | 2 |
| R1 | 1 | 1 |

## What this round does not establish

- **The libraries.** Their digests are the document's; the binaries are not here, and nothing here ran MPFR.
- **Implementation independence on the lower side.** The MPFR replay is the A1 replay's rule and code over another
  interval type; the two agree margin for margin because they compute the same polygons.
- **Anything beyond cell 0's shard.** The global state is unchanged: 51/77 at d = 36, and a_Leb ≥ 0.835 is not
  certified.