**T-III-4-015 witness form for separable isogenies**: If `φ` is
separable and has a finite kernel, and at least one fiber has
cardinality = `sepDegree`, then `#ker φ = deg φ`. 

**III.4.10(c), good-fibre form — the W-3 headline**: a separable isogeny `β` over an
algebraically closed field, with a coordinate-ring witness `cd` for its pullback
(module-finite) and the cofinite pullback-evaluation coherence for its stored point
map, has `Nat.card β.kernel = β.degree`. 

**Witness-parametric Silverman V.1.2 (`1 − π` separable)**.

Given a witness isogeny `β` (the "true" `1 − π`) whose ω-pullback coefficient is
`1` in `K(E)` and satisfies the T-II-4-004 separability criterion, `β` is
separable. The hypothesis `h_coeff : omegaPullbackCoeff W β = 1` is the
Silverman III.5.3 result at `m = 1` (combined with III.5.2 additivity applied
to the decomposition `1 + (-1)·π`, using `π* ω = 0`).

Reference: Silverman V.1.2 (uses III.5.5 with `m = 1, n = -1`). 

**Witness-parametric Silverman III.5.5 (coefficient form)**.

Given `β : Isogeny E E` and `c : F`, suppose:
* the ω-pullback coefficient of `β` is `algebraMap F _ c`;
* separability of `β` is equivalent to the ω-pullback coefficient being nonzero
  (this is T-II-4-004 specialized to `β`).

Then `β.IsSeparable ↔ c ≠ 0` in `F`.

Reference: Silverman III.5.5. 

**V.1.3 sharp residual** (Silverman III.4.10c): the degree of the
isogeny `1 − π` equals the number of `F_q`-rational points of `E`.

**[2026-05-29 ROUND-9 rewire — R2 embeddings-classification.]** Now PROVED axiom-clean
*modulo the single embedding↔kernel count* `isogOneSub_negFrobenius_sepDegree_eq_card_kernel`
(see the block comment above). The proof is pure composition:
`#ker γ = sepDegree γ` (the residual) `= degree γ` (separability) and `#ker γ = pointCount`
(`ker γ = ⊤`). The dead L6_B3_tower / place↔point / `CoordHom` route is superseded.

This is the **sole** sharp sub-fact gating V.1.3. All three V.1.3 targets close from it
(plus axiom-clean shipped lemmas): `sepDegree_oneSub_eq_pointCount`, `ker_deg_skeleton`,
and `Sinf_sum_inertiaDeg_over_xIdeal_eq_pointCount_via_tower` (via the cardinality squeeze
of the fundamental ramification identity).

**[2026-05-28 ROUND-5 reduction.]** Per the block-comment above, this statement is
equivalent — via `l6_B3_tower` (axiom-clean), Mathlib's `Ideal.sum_ramification_inertia`,
the shipped bridge lemmas (`bridge_Biii_ord_eq_neg_two_v2`, `bridge_Biv_inertia_eq_one_v2`,
`Sinf_kernelToPrime_v2_injective`), and the axiom-clean squeeze composer
`Sinf_sum_inertiaDeg_over_xIdeal_eq_pointCount_of_finrank_witness` — to:

> Every prime `P` of `Sinf` over `(X)` is the kernel-prime of some `T ∈ ker(1 − π)` (i.e.
> is in the image of `bridge_Bi_kernelToPrime_v2`).

Mathematical content: function-field place ↔ closed-point dictionary over `K` (Silverman
II.2.4), specialised to the pole locus of `f = (1−π)*x`. Since `x` has its only pole at `O`,
a closed point of `E` where `f` has a pole satisfies `(1−π)(P) = O`, i.e. `P ∈ ker(1−π)`;
over `K`, these are the `K`-rational kernel points = `E(F_q)`.

**Casualties (round-5).** The WireUpPrep route (`degree_isogOneSub_negFrobenius_eq_pointCount`
+ `oneSubFrob_baseChange_coordHom`) is **dead** — relies on an impossible `CoordHom : R → R`
for `1 − π`. See the B2 annotation on `HasseWeil.RouteB.nReduced_R_div_D_sq`. 

Generalized form of `oneSubFrobeniusIsog_kernel_eq_top` for any witness
isogeny with the same point-map as `1 − π`. 

**Point count via a genuine `1 − π` witness** (Silverman V.1.1): if `β` is
any isogeny with `β.degree = pointCount`, then
`pointCount = q + 1 - isogTrace π β`.

Independent of any placeholder. The witness `β` is the genuine `1 − π`
(`isogOneSub_negFrobenius W hq`), whose `degree = pointCount` is the V.1.3
keystone (`ker_deg_skeleton` / `isogOneSub_negFrobenius_degree_eq_pointCount`). 

**Composed V.1 witness form**: if `β` has point-map `id − π` and
`#ker β = β.degree`, then `#E(F_q) = q + 1 − isogTrace π β`.