# RUN-094 — The Loeffler–Rivero paper read, its hypotheses computed on our actual forms: **C4's direction closes**, and certificate item C1's partner-independence turns out to be a theorem of the source rather than an assumption of PC-001 — with a correction to RUN-093, whose "nonvanishing UNMEASURED" was wrong

**Arm:** 數學戰士「墜衡」 / AMRAL Research Lab
**Subject:** the web line's Track B instruction after [RUN-093](../RUN-093/) — extract the minimal hypotheses from the theorems LR / LLZ / KLZ actually invoke and instantiate them one by one, without presupposing full mod-11 surjectivity; and its demand that existence be kept apart from computability
**Source read:** D. Loeffler and Ó. Rivero, *Eisenstein degeneration of Euler systems*, arXiv:2201.02078v2; J. reine angew. Math. **814** (2024), 241–282 — read 2026-09-15, recorded in `data/external/literature/loeffler-rivero-2201.02078v2/`
**Tools:** `src96_lr_hypotheses_and_c4_direction.py`, `src11_gate_drill.py`
**Logs:** `src96-lr-hypotheses-and-c4-direction.json`, `src11-gate-drill.json`
**Deliverable:** [`handoff/LR-HYPOTHESES-AND-C4-DIRECTION/`](../../packages/LR-HYPOTHESES-AND-C4-DIRECTION/)

**Result. This round did something the previous four did not: it read the paper the whole architecture rests on, and computed its hypotheses on our actual forms. Two things the tree had been carrying as unproved turn out to be theorems, and one thing this line had reported was simply wrong. THE CORRECTION FIRST. RUN-093 reported C4's nonvanishing as UNMEASURED on the grounds that every witness the web line listed needs the overconvergent θ-critical eigenspace. That was wrong. One of those witnesses is the *reducibility ideal*, and it is a theorem: LR Theorem A6.1 (= Bellaïche–Chenevier [BC06, Thm 1]) states the reducibility ideal of the pseudo-character of the Coleman family through `f_β` is exactly `𝔪`, and §A6.2 concludes from maximality that `V(f_β)`, `V_c(f_β)` and both duals are **non-split**. No overconvergent computation is needed; what is needed are hypotheses, and the hypotheses are computable. THE CHAIN, with the computed parts marked. Our auxiliary form sits in LR Definition A1.1 as `ψ = 1`, `τ = χ₈`, `r = 0`, `N = 8` — matched here against the actual q-expansion `a_ℓ = 1 + χ₈(ℓ)ℓ` at ten primes, with the parity condition and with `α = ψ(11) = 1`, `β = 11·χ₈(11) = −11`, which are exactly the roots of `U² + 10U − 11` RUN-091 computed, `β` being the critical-slope one. Definition A1.2's `r = 0` branch asks that for every prime dividing `Np = 88` either that prime divides `cond(ψ/τ)` or the character value there is not 1: at `ℓ = 2`, `2 | 8`; at `ℓ = 11`, `χ₈(11) = −1 ≠ 1` — **11-decent, computed** (and the conductor of `ψ/τ` is *derived* in the gate from the identification, not asserted, so a wrong conductor is caught). Proposition A4.6(ii) then gives **non-criticality** for free, because `r = 0`. Theorem A6.1 and §A6.2 give non-splitness; Corollary A6.3(i) identifies `V(f_β)` as case (3) of Theorem A2.1 — the unique non-split extension that is **crystalline at `p`**. Case (3) has `ψ` as sub, so its class lies in `Ext¹(τε^{−1−r}, ψ) = H¹(Q, ψτ⁻¹ε^{1+r})`, which for our values is **`H¹(Q, Q₁₁(χ₈)(1))`** — precisely the line RUN-092 found and RUN-093 showed has vacuous local conditions at every place; and LR Theorem A4.5 states non-criticality in terms of that very group, an independent confirmation of the bookkeeping. Crystalline puts the class in `H¹_f`; non-split makes it nonzero; RUN-092's `dim H¹_f = 1` then forces **`[Θ_aux] = c_ES/Kum·κ(ε)` with `c_ES/Kum ∈ Q₁₁^×`. C4's DIRECTION IS CLOSED; the scalar stays OPEN.** SECOND, CERTIFICATE ITEM C1. RUN-090 carried the partner-independence of `C_π` as C1's unproved core. It is the source's own result: LR Theorem C1.9 states `c_f(k)` is "a meromorphic function on `V₁` **alone**" — `V₁` being the *auxiliary* family's disc; Remark C1.11 says that although the partner family `g` is used in building `ω_f`, it "is uniquely determined by `f`"; and Theorem C1.13 — which **is** PC-001's formula (1), matched factor for factor here — opens its proof by taking `C = c*_f(r)`, with `C` nonzero. So `C_π` is a functional of the auxiliary family alone. THIRD, THE BF CLASS EXISTS. LR Theorem C1.4 fixes `d ∈ Z_{>1}` with `(d, 6S) = 1` and asserts the **existence** of `κ_d(f,g)` interpolating the finite-level Beilinson–Flach classes — and that hypothesis on `d` is exactly the coprimality PC-001 and Attack 09 already record for their smoothing integer `d = 5`, recomputed here as `gcd(5, 6S) = 1`. So the web line's **B1/B2 are PASS-EXISTENCE** and its **B3/B4 stay UNMEASURED**: the theorem gives a class and an interpolation property, not coordinates. FOURTH, THE PARTNER HYPOTHESIS IS LIGHT. C1.1's Setup asks of the cuspidal partner only that it be ordinary — no residual surjectivity — and both partners are ordinary at 11. The web line's instruction not to assume surjectivity was right, and the gate plants adding it as a defect. A NOTATION TRAP is recorded: LR's `f` is the Eisenstein family and its `g` the cuspidal partner, the reverse of PC-001's letters; and LR normalises by `tr ρ(Frob_ℓ⁻¹) = a_ℓ`, so its second character is `χ₈ε^{−1−r}` where RUN-091's is `χ₈ε^{1+r}` — dual conventions that the gate checks give the **same** Ext group, so RUN-093's dictionary stands. What stays UNMEASURED: the BF coordinates, `c_ES/Kum`, and `Π_E/Π_0`.**

---

## The correction to RUN-093

RUN-093 §3 said the transverse class's nonvanishing was `UNMEASURED` because "every witness the request lists needs the overconvergent θ-critical eigenspace". That sentence was wrong about one of the five witnesses. The reducibility ideal is settled in the literature, and its hypotheses are arithmetic conditions on our own form. RUN-093's other findings — the local conditions, the dictionary, the `L(−1,χ₈)` computation — stand unchanged; only the nonvanishing verdict moves.

The `v₁₁(L(−1,χ₈)) = 0` computation also stands, and keeps its meaning: it closes the *classical cuspidal-congruence* route to the witness. The witness that works comes from the family's pseudocharacter, not from a congruence.

## The chain, and who proved what

| step | statement | source | label |
| --- | --- | --- | --- |
| (a) | our form is `E₂(1,χ₈)`: `ψ = 1`, `τ = χ₈`, `r = 0`, `N = 8`; `α = 1`, `β = −11` | LR Def. A1.1 | **COMPUTED_HERE** (q-expansion at 10 primes, parity, both roots) |
| (b) | 11-decency | LR Def. A1.2 | **COMPUTED_HERE** (`ℓ = 2`: `2 | 8`; `ℓ = 11`: `χ₈(11) = −1`) |
| (c) | `f_β` non-critical | LR Prop. A4.6(ii) | CITED_THEOREM + verified hypotheses |
| (d) | reducibility ideal `= 𝔪` | LR Thm. A6.1 (= [BC06, Thm 1]) | CITED_THEOREM |
| (e) | all four representations non-split | LR §A6.2 | CITED_THEOREM |
| (f) | `V(f_β)` = case (3): non-split, **crystalline at `p`** | LR Cor. A6.3(i), Thm. A2.1 | CITED_THEOREM |
| (g) | case (3)'s class lies in `H¹(Q, Q₁₁(χ₈)(1))` | Ext bookkeeping | **COMPUTED_HERE**; confirmed by LR Thm. A4.5's phrasing |
| (h) | `dim H¹_f = 1`, spanned by `κ(ε)`; local conditions vacuous | RUN-092, RUN-093 | **COMPUTED_HERE** |

```text
⇒  [Θ_aux] = c_ES/Kum · κ(ε),   c_ES/Kum ∈ Q₁₁^×
   C4-direction  CLOSED
   C4-exact-scalar  OPEN
```

## Certificate item C1 — partner-independence is the source's own

| | |
| --- | --- |
| **Thm C1.9** | `c_f(k)` is "a meromorphic function on `V₁` alone", regular and non-vanishing at integer weights `k ⩾ −1` except possibly `k = r`, where it is regular |
| **Thm C1.10** | there exist an integer `n ⩾ 0` and a **unique** isomorphism `ω_f` over `O(V₁)` |
| **Remark C1.11** | `g` is used in constructing `ω_f`, but it "is uniquely determined by `f`" |
| **Thm C1.13** | the degeneration formula; proof opens "Taking `C = c*_f(r)`", `C ∈ L^×` nonzero |

The dictionary to PC-001 (1), checked complete in both directions by the gate:

| LR Theorem C1.13 | PC-001 (1) |
| --- | --- |
| `C` (= `c*_f(r)`, nonzero) | `C_π` |
| `C_d(f_β, g, j)` | `𝒮₅(t)` |
| `L_p(g ⊗ τ, j−1−r)` | `λ_i(t)` |
| `L_p(Ad g)` | `D_i` |
| `log^{[r+1]}` | `j(t) = log(1+t)/log₁₁(12)` |
| `κ(g × ψ)` | the Kato class / `z_i` |

So PC-001's formula is a faithful transcription of C1.13, and `C_π = C = c*_f(r)` is a functional of the auxiliary family alone — **partner-independent by theorem**, and nonzero.

## Track B, in the format asked for

```text
theorem used:  Loeffler-Rivero, Eisenstein degeneration of Euler systems (arXiv:2201.02078v2),
               Theorem C1.4 (existence), C1.1 Setup (hypotheses), Thm C1.9 / Rmk C1.11 / Thm C1.13.

389.a1:  PASS = [ ordinary at 11 (a_11 = -4, unit root 7) ]
         UNMEASURED = [ ]            FAIL = [ ]
19.a1 :  PASS = [ ordinary at 11 (a_11 =  3, unit root 3) ]
         UNMEASURED = [ ]            FAIL = [ ]
auxiliary side: PASS = [ 11-decent, non-critical, d = 5 with (d, 6S) = 1 ]

NOT REQUIRED by the theorem: full mod-11 surjectivity of the residual representation.

BF existence:   BF_E = PASS-EXISTENCE       BF_0 = PASS-EXISTENCE      (LR Thm C1.4, one theorem, two g)
finite-level precursor:  E = UNMEASURED     0 = UNMEASURED

common auxiliary data:      the Eisenstein family f = E_k(1,chi_8) and its disc V_1; the critical
                            stabilisation beta = -11; the smoothing d = 5; the cyclotomic coordinate
                            gamma = 12; the canonical Eisenstein quotient; c_f, omega_f, C = c*_f(r).
partner-specific data:      a_11 and the unit root; lambda_i = L_p(g (x) chi_8); D_i = L_p(Ad g);
                            the Kato class kappa(g x psi).

C1 smallest remaining blocker:  not partner-independence (now a theorem) and not existence (now a
                            theorem) — it is the ABSENCE OF COORDINATES: no computed representative
                            of kappa_d(f,g), hence none of B_{E,2} or r_{0,1}.
next executable object:     a finite-level Rankin-Eisenstein / Beilinson-Flach class _dBF[f_k, g_l]
                            at an integer weight k != r, which is what Theorem C1.4 interpolates.
                            This tree cannot build it: it needs etale cohomology of modular curves
                            with coefficients, not modular symbols. Naming the missing engine
                            precisely: an etale/motivic Rankin-Eisenstein class engine.
```

Against the web line's Case A–D: this is **Case A with one qualification** — the BF classes exist canonically for both partners by theorem, every actual hypothesis passes, the auxiliary construction is theorem-level common — and the remaining C1 blocker is *not* a Perrin-Riou/Coleman normalisation comparison but the absence of any computed representative.

## What the tree's own checks caught

Adding this gate turned `claim-ladder` **red**. The cause was in the new gate, not in the old check: gate logs in this tree use a top-level `"source"` field as a **string** naming the corpus document that round compiled — `src45`'s stop rule reads it to decide whether the last three rounds each brought in something new — and this gate had written a dict there. Fixed by following the convention, which is also the honest record: this round *did* compile a document the tree had never held.

## The drill

**474 defects, 474 caught by the check named for each**, 0 uncaught, 0 caught by the wrong check, 126 controls undisturbed, over 144 checks.

The 12 planted for this gate, over its six checks `lr-identification`, `lr-decency`, `lr-ext-group`, `lr-partner-dictionary`, `lr-bf-existence`, `lr-verdict` — each caught by the check named for it (`lr-verdict` goes red alongside, since the verdict rests on all of them):

| planted defect | named check | went red |
| --- | --- | --- |
| psi and tau are swapped in the Loeffler-Rivero identification | `lr-identification` | `lr-identification`, `lr-decency`, `lr-verdict` |
| the auxiliary weight is read as r = 1 instead of r = 0 | `lr-identification` | `lr-identification`, `lr-decency`, `lr-ext-group`, `lr-verdict` |
| tau's conductor is taken as 4 instead of 8 | `lr-identification` | `lr-identification`, `lr-decency`, `lr-verdict` |
| the conductor of psi/tau is declared 88, so decency would pass trivially at 11 | `lr-decency` | `lr-decency`, `lr-verdict` |
| the Ext twist of Theorem A2.1 case (3) is read as eps^(-1-r) | `lr-ext-group` | `lr-ext-group`, `lr-verdict` |
| full mod-11 surjectivity is added to the partner hypotheses the paper does not require | `lr-partner-dictionary` | `lr-partner-dictionary`, `lr-verdict` |
| the smoothing integer is taken as 6, which is not coprime to 6S | `lr-bf-existence` | `lr-bf-existence`, `lr-verdict` |
| the smoothing integer is taken as 1, below Theorem C1.4's d > 1 | `lr-bf-existence` | `lr-bf-existence`, `lr-verdict` |
| the nonvanishing is relabelled COMPUTED_HERE when it is a cited theorem | `lr-verdict` | `lr-verdict` |
| C4's direction is closed without requiring both membership and nonvanishing | `lr-verdict` | `lr-verdict` |
| a value is claimed for the comparison scalar c_ES/Kum | `lr-verdict` | `lr-verdict` |
| the Beilinson-Flach coordinates are claimed to be in hand | `lr-verdict` | `lr-verdict` |


## What this round does not claim

* **No BF class is computed.** Existence is a cited theorem; coordinates, a finite-level representative, `B_{E,2}` and `r_{0,1}` remain `UNMEASURED`.
* **No scalar.** `c_ES/Kum` is untouched; `Π_E/Π_0` is untouched.
* **Nothing in the paper is proved here.** Every LR statement is `CITED_THEOREM`; what this gate computes is their hypotheses, and it plants a defect for relabelling the nonvanishing as `COMPUTED_HERE`.
* The extracts file is a working record in this line's own words with the paper's numbering — not a copy of the paper.
* **BSD remains open.**