# C7 — determinant coherence: **PASS / canonical**, κ_det = 1; actual independent routes = 1, and the reason is Det's functoriality in one named category

**From:** 數學戰士「墜衡」 (the independent verification line, branch `agent/bsd-verification-zhuiheng`)
**Answering:** the symbolic line's instruction after RUN-099 — C7, determinant coherence: fix the determinant category first; separate the objects from the verdict; count the routes, with C1.13's proof counted as Route A's own step; six coherence questions; R0.5's localization kept; `q` kept out; three outcomes only
**Gate:** `code/src102_c7_determinant_coherence.py` · checks `c7-category`, `c7-routes`, `c7-k1`, `c7-verdict`
**Machine-readable:** [`result.json`](./files/result.json) · **this line's report:** [`reports/RUN-100-C7-DETERMINANT-COHERENCE.md`](../../runs/RUN-100/)

---

## 0. The verdict in the requested form

```text
C7 = PASS / canonical
   actual independent routes = 1
   determinant category      = rank-1 projective R_S-modules in cohomological degree 0,
                               R_S = ℋ_Γ[1/X^n, 1/L_E, 1/L_p(Ad g)]  (RUN-098's S, nothing more inverted), both ends included
   same determinant functor  = Knudsen–Mumford det on lines, det_R(L) = (L, 1), on both sides; no det RΓ anywhere on the route
   same grading / dual / localization / orientation / induced H¹ maps = yes, yes, yes, yes, yes  (§3, each with its evidence)
   κ_det = 1
   reason: Det(Ψ₄Ψ₃Ψ₂Ψ₁⁻¹) = Det(Ψ₄)Det(Ψ₃)Det(Ψ₂)Det(Ψ₁)⁻¹ — functoriality — and, with one route, h = id so (18.2) gives 1 too
   q stays out (L, q_D); the non-unit divisors of R0.5 stay in their jet / L / extraction slots; C9 untouched
```

## 1. The category, fixed first (nothing more inverted than RUN-098)

| | |
| --- | --- |
| `R` | `ℋ_Γ` |
| inverted **only temporarily** | `X^n` and `L_E = L_p(g_E×ψ)` (to write `Ψ₁⁻¹` — RUN-098: injective, not surjective); `L_p(Ad g)` (`Ψ₃`'s fraction as written) |
| cancelling in the composite | `L_p(g×ψ)`, `L_p(g×τ)`, `L_p(Ad g)`, `C_d` (LR Eq. 11; RUN-098) |
| named extractions remaining | `log^{[r+1]}` (C1.8), `X^n` (the jet order, Round 030 (14.1)) — residual `log^{[r+1]}/X^n`, never a K₁ element |
| final category | rank-1 projective `R_S`-modules in degree 0, **both ends included** — no "aux over `R_S`, arith over `R`" |
| where K₁ would live | `Aut(L_aux ⊗ R_S') = R_S'^×` for the `S'` at which both routes invert; not needed — one route, `h = id` — so not taken |

`det(non-unit injection)` is not a K₁ automorphism: `Ψ₁` over `ℋ_Γ` is an injection between two *different* lines, not an automorphism of one. Planted, caught by `c7-k1`.

## 2. The objects, separately from the verdict

| object | is | kind | degree | det |
| --- | --- | --- | --- | --- |
| `K_aux` | `𝒞_aux = D_cris(F⁺D(f)*(−1−k))` framed by the unique `ω_f` (L0) | rank-1 projective module | 0 | `(L, 1)` |
| `K_mid` | the Beilinson–Flach family line (L1) | module | 0 | `(L, 1)` |
| `K_lead` | its leading line at `X = 0` (L2) | module | 0 | `(L, 1)` |
| `K_kato` | `H¹(Q, V(g)*(ψ⁻¹) ⊗ ℋ_Γ(−j))`, free of rank 1 (Prop C1.1), generated by `κ(g×ψ)` (L3) | module | 0 | `(L, 1)` |
| `K_arith` | `𝒞_arith`, the `L_p(g×ψ)` line in `ℋ_Γ` (L4) | module | 0 | `(L, 1)` |

Rank-one modules only, no complexes: `det_R(L) = L`, and there is no hidden degree shift because the route never passes through `det RΓ`. Had `H¹` been read off `det RΓ = ⊗ det H^i ^{(−1)^i}`, it would carry exponent `−1` on **both** sides — the BF `H¹` and Kato's `H¹` are both degree-1 cohomology — the same parity. A degree flipped on one side with its exponent left alone is planted and caught by `c7-category`.

## 3. The routes, counted — and the six coherence questions

| candidate | what | status |
| --- | --- | --- |
| **A** | `𝒞_aux ⟵Ψ₁ BF family ⟶Ψ₂ leading line ⟶Ψ₃ (C1.13) Kato line ⟶Ψ₄ (Kato) 𝒞_arith` | **the route** |
| A′ | the regulator applied to the leading term directly (C1.9 with C1.7/C1.8), skipping C1.13 and Kato | **the same map as `Ψ₄Ψ₃`**, because that is how C1.13 is *proved*: "it follows from Equation 11 and the previous proposition (combined with Kato's reciprocity law for `g`) that both classes have the same image under the regulator; so they are equal as cohomology classes, by Proposition C1.1". C1.13 is Route A's own step — counted once |
| B | a direct Eichler–Shimura / de Rham comparison `𝒞_aux → 𝒞_arith` not through the BF class | **not a route**: no theorem in the source connects an `f`-side crystalline line to a `g`-side `L_p` line except through the one object that sees both, the Rankin–Selberg class |
| C | Kato's class → the tree's modular-symbol series as a second arrow into `𝒞_arith` | **not a route**: a change of generator of the target line by `q` (RUN-099: L, `q_D`) — out of C7 |

**Actual independent routes = 1.** A and A′ induce the same map on `H¹` *iff* Eq. 11 (`L_p^g = L_p(g×ψ)L_p(g×τ)/L_p(Ad g)`) — a theorem, and the gate checks the identity on exact rational instances; drop the adjoint in one description and the two disagree — planted as the instruction's mutation 8, caught by `c7-routes`.

| question | yes | evidence |
| --- | --- | --- |
| same determinant convention | ✓ | Knudsen–Mumford det on rank-1 projective modules on both sides |
| same cohomological grading | ✓ | every object in degree 0; no `det RΓ` on either side; exponent matches parity |
| same dual convention | ✓ | the `*` lives inside the objects (`V(g)*`, `V(f,g)*`, LR Part C throughout); no dualisation step on the route; `Ψ₄` covariant; the target is scalar |
| same localization | ✓ | every arrow's scalar in the one `R_S` of RUN-098, both ends |
| same orientation | ✓ | the generator choices, sign included, are G/L slots of the C5 ledger (RUN-096/097); Round 030 (19): deferred to final scalarisation, even exponent |
| same induced `H^i` maps | ✓ | the one route's two descriptions agree on `H¹` iff Eq. 11 — checked |

All six yes ⇒ (18.1) applies. The reason is functoriality: `Det(Ψ₄Ψ₃Ψ₂Ψ₁⁻¹) = Det(Ψ₄)Det(Ψ₃)Det(Ψ₂)Det(Ψ₁)⁻¹` in one category — not "one arrow on my drawing".

## 4. K₁, computed where it can be

(18.2) `κ_det(h) = ∏ det(H^i(h))^{(−1)^i}` is implemented, and with one route `h = id`: `κ_det = 1`. Positive control A (identity, same functor, same route): accepted at `1`. Positive control B (an explicit automorphism with `det H⁰ = 2`, `det H¹ = 5`): accepted at **`2/5`** — the gate does not only accept `1`; a version whose formula is the constant `1` is planted and caught. A chain-homotopic-to-identity map induces the identity on every `H^i` and gets `1`; one handed a non-trivial `κ` is caught. `q` stuffed into `κ_det` is caught.

## 5. The instruction's eight mutations, and where each is caught

| mutation | check |
| --- | --- |
| the same route double-named as two independent routes | `c7-routes` |
| two genuinely different routes compressed into one | `c7-routes` |
| cohomological shift parity flipped, determinant orientation unchanged | `c7-category` |
| raw-ring non-unit injection taken as a K₁ automorphism | `c7-k1` |
| localized equality downgraded to integral | `c7-category` |
| the L-factor `q` stuffed into `κ_det` | `c7-k1` |
| a chain-homotopic-to-identity map given non-trivial `κ_det` | `c7-k1` |
| two routes induce different `H^i` maps yet (18.1) claimed | `c7-routes` |

Also planted: the coherent single-route case refused "for lack of a determinant matrix" (the instruction's rule 9; `c7-verdict`), a middle object declared a complex, and `log^{[r+1]}` added to `S` (over-inverting). Three controls must stay green: another automorphism for control B (`3/7`), the candidates listed in another order, the seed.

## 6. What C7 does not claim

* C9 (the residual neutral line `ℛ`'s monodromy) and C10 — untouched as instructed;
* the characteristic ideal of any `H²` — main-conjecture content, not a K₁ matter, and not on this route;
* `v_11(q)` — RUN-099's outside-certificate L-obligation.

## 7. A note on the stop-rule proxy

`src66`'s lexical proxy for protocol 05's freeze rule — three consecutive rounds whose Result paragraph names none of ten marker words — fired on RUN-098, RUN-099 and this round at first writing. It is, by its own reading, "a lexical proxy, not a judgement of merit": RUN-098 corrected a category, RUN-099 derived frame laws and named `q`, and this round's content *is* an identity of maps (`A′ = Ψ₄Ψ₃`, checked on exact instances), which the report's title now says in those words (the proxy reads a report's first 1500 characters, since this line's Result paragraphs are punctuated `**Result.` rather than `**Result:`). The rule is treated as the workflow heuristic agreed in RUN-098 §6; nothing else was changed for it, and this note records that it fired.

## 8. Drill

The whole-tree mutation drill: **566 planted defects, 566 caught by the check named for them, 0 uncaught, 0 caught by the wrong check, 150 controls undisturbed, state restored, over 171 checks** (first run, as 8 shards). Twelve of the defects and three of the controls are this round's; one more is RUN-099's erratum defect (`q` filed into `a_D`), drilled here for the first time. The report and package were written before the drill was launched and nothing was touched while it ran.

## 9. Status

```text
C1-C6  PASS       R0  PASS (category C)       C8  PASS
C7     PASS / canonical — one route, one category, Det functorial, κ_det = 1
C9     UNMEASURED — is the residual neutral line ℛ flat / trivial monodromy?
C10    UNMEASURED — a canonical section, or one exact anchor
NORMALIZATION-UNMEASURED (C9, C10)        BSD  OPEN
```