4.4. The local classification
If \deg_F(v) \le 3, then either u + \delta_v \le 3, or v has exactly
three neighbours p, q, r with
\delta_v = 3, u = 1, \operatorname{rank} C_v = 2,
\dim_K \ker C_v = 1 and \ker \partial_v = \ker C_v, and in that case
a_p, a_q, a_r are distinct and collinear.
(Zheng, 2026, Lemma 2.3)
Lean code for Lemma4.4.1●2 theorems
Associated Lean declarations
-
theoremdefined in RB31EndToEnd/Linear/OutsideLocalClassification.leancomplete
theorem RB31E2E.DirectionStress.outsideExceptional_linear_dichotomy.{u, v, w} {k : Type u} {K : Type v} {V : Type w} [Field k] [Field K] [Algebra k K] [Fintype V] [DecidableEq V] (F : RB31E2E.SimpleEdgeSet V) (a : V → Fin 3 → K) (v : V) (ha : Function.Injective a) (hDegree : RB31E2E.edgeSetDegree F v ≤ 3) (hgen : IntermediateField.adjoin k (Set.range fun c ↦ a c.1 c.2) = ⊤) (hExceptional : RB31E2E.DirectionStress.OutsideExceptional F a v) : Cardinal.toNat (RB31E2E.DirectionStress.outsideExtensionTrdeg a v) = 3 ∧ 1 ≤ RB31E2E.DirectionStress.outsideResponseKernelDim F a v ∨ Cardinal.toNat (RB31E2E.DirectionStress.outsideExtensionTrdeg a v) = 2 ∧ RB31E2E.DirectionStress.outsideResponseKernelDim F a v = 2 ∧ RB31E2E.DirectionStress.outsideLocalKernelDim F a v = 2 ∧ RB31E2E.DirectionStress.outsideLocalRank F a v = 1 ∧ RB31E2E.edgeSetDegree F v = 3
theorem RB31E2E.DirectionStress.outsideExceptional_linear_dichotomy.{u, v, w} {k : Type u} {K : Type v} {V : Type w} [Field k] [Field K] [Algebra k K] [Fintype V] [DecidableEq V] (F : RB31E2E.SimpleEdgeSet V) (a : V → Fin 3 → K) (v : V) (ha : Function.Injective a) (hDegree : RB31E2E.edgeSetDegree F v ≤ 3) (hgen : IntermediateField.adjoin k (Set.range fun c ↦ a c.1 c.2) = ⊤) (hExceptional : RB31E2E.DirectionStress.OutsideExceptional F a v) : Cardinal.toNat (RB31E2E.DirectionStress.outsideExtensionTrdeg a v) = 3 ∧ 1 ≤ RB31E2E.DirectionStress.outsideResponseKernelDim F a v ∨ Cardinal.toNat (RB31E2E.DirectionStress.outsideExtensionTrdeg a v) = 2 ∧ RB31E2E.DirectionStress.outsideResponseKernelDim F a v = 2 ∧ RB31E2E.DirectionStress.outsideLocalKernelDim F a v = 2 ∧ RB31E2E.DirectionStress.outsideLocalRank F a v = 1 ∧ RB31E2E.edgeSetDegree F v = 3
The preceding dichotomy instantiated with the actual coordinate-field extension. Thus an actual exceptional outside deletion is already reduced to the maximal-cost branch or the one explicit rank-one branch.
-
theoremdefined in RB31EndToEnd/Linear/OutsideLocalGeometry.leancomplete
theorem RB31E2E.DirectionStress.outsideExceptional_classification.{u, v, w} {k : Type u} {K : Type v} {V : Type w} [Field k] [Field K] [Algebra k K] [Fintype V] [DecidableEq V] (F : RB31E2E.SimpleEdgeSet V) (a : V → Fin 3 → K) (v : V) (ha : Function.Injective a) (hDegree : RB31E2E.edgeSetDegree F v ≤ 3) (hgen : IntermediateField.adjoin k (Set.range fun c ↦ a c.1 c.2) = ⊤) (hExceptional : RB31E2E.DirectionStress.OutsideExceptional F a v) : ∃ N, RB31E2E.PinCollinearity.Collinear (a N.p) (a N.q) (a N.r) ∧ a N.p ≠ a N.q ∧ a N.p ≠ a N.r ∧ a N.q ≠ a N.r ∧ RB31E2E.DirectionStress.outsideExtensionTrdeg a v = 3 ∧ RB31E2E.DirectionStress.outsideResponseKernelDim F a v = 1 ∧ RB31E2E.DirectionStress.outsideLocalKernelDim F a v = 1 ∧ RB31E2E.DirectionStress.outsideLocalRank F a v = 2 ∧ RB31E2E.DirectionStress.deletedConnectingClass F a v = 0
theorem RB31E2E.DirectionStress.outsideExceptional_classification.{u, v, w} {k : Type u} {K : Type v} {V : Type w} [Field k] [Field K] [Algebra k K] [Fintype V] [DecidableEq V] (F : RB31E2E.SimpleEdgeSet V) (a : V → Fin 3 → K) (v : V) (ha : Function.Injective a) (hDegree : RB31E2E.edgeSetDegree F v ≤ 3) (hgen : IntermediateField.adjoin k (Set.range fun c ↦ a c.1 c.2) = ⊤) (hExceptional : RB31E2E.DirectionStress.OutsideExceptional F a v) : ∃ N, RB31E2E.PinCollinearity.Collinear (a N.p) (a N.q) (a N.r) ∧ a N.p ≠ a N.q ∧ a N.p ≠ a N.r ∧ a N.q ≠ a N.r ∧ RB31E2E.DirectionStress.outsideExtensionTrdeg a v = 3 ∧ RB31E2E.DirectionStress.outsideResponseKernelDim F a v = 1 ∧ RB31E2E.DirectionStress.outsideLocalKernelDim F a v = 1 ∧ RB31E2E.DirectionStress.outsideLocalRank F a v = 2 ∧ RB31E2E.DirectionStress.deletedConnectingClass F a v = 0
**Outside-local classification.** If a degree-at-most-three deletion fails the three-coordinate payment at an injective, coordinate-generating function-field point, then every part of the unique bad shape is forced by the actual maps and fields: * the degree is three; * the three retained neighbours are pairwise distinct and collinear; * the extension transcendence degree is exactly three; * both `ker C_v` and the connecting kernel have dimension one; * consequently the entire one-dimensional local relation space descends through the child row-space quotient.
Since K is generated by L and the three coordinates of a_v, we have
\delta_v \le 3. If \deg_F(v) \le 1 then C_v is injective. If
\deg_F(v) = 2 and \ker C_v \ne 0, then v and its two neighbours are
collinear; the line through the two L-points is defined over L, so
\delta_v \le 1, and u \le 1 gives u + \delta_v \le 2.
Let \deg_F(v) = 3. If \operatorname{rank} C_v = 3 then u = 0. If
\operatorname{rank} C_v \le 1 the three star directions are collinear, so
a_v and all its neighbours lie on a line defined over L, whence
\delta_v \le 1 while u \le \dim \ker C_v \le 2. In the remaining case
\operatorname{rank} C_v = 2 and u \le 1, so a failure of (2.7) forces
u = 1 and \delta_v = 3. Noncollinear neighbours would put a_v in the
affine plane they span, giving \delta_v \le 2. Finally
\ker \partial_v \subseteq \ker C_v and both are one-dimensional.
The formalization splits this proof along the same lines, into a numerical and
a geometric module. The numerical module, OutsideLocalClassification.lean,
proves rank–nullity for C_v, proves that the kernel of \partial_v is a
subspace of \ker C_v, and deduces that a failure of u + \delta_v \le 3 at
degree three forces the values in (2.8). The geometric module,
OutsideLocalGeometry.lean, proves the two field-generation statements of the
proof above: if \operatorname{rank} C_v \le 1, then a_v lies on a line
defined over L, so \delta_v \le 1; if \operatorname{rank} C_v = 2 and
the three neighbours are not collinear, then a_v lies in their affine
plane, so \delta_v \le 2.
outsideExceptional_classification
is the two halves combined, and its conclusion is (2.8) together with
distinctness and collinearity of the three neighbour coordinates, and with
\partial_v = 0 rather than \ker \partial_v = \ker C_v. Those two
statements agree here because both kernels are one-dimensional and one contains
the other.
The paper's hypothesis is a bound on the degree of v in F; the Lean
hypothesis is the same bound plus injectivity of the placement, which the
paper assumes from the start of the section and the formalization takes as
an explicit hypothesis.