4.5. Descent and the three neighbour rows
Let L \subseteq K, let R \subseteq L^M be a subspace, and let
x_1, x_2, x_3 \in K be such that 1, x_1, x_2, x_3 are linearly independent
over L. If c, b_1, b_2, b_3 \in L^M satisfy
c + \sum_j x_j b_j \in R \otimes_L K, then c, b_1, b_2, b_3 \in R.
(Zheng, 2026, Lemma 2.4)
Lean code for Lemma4.5.1●1 theorem
Associated Lean declarations
-
theoremdefined in RB31EndToEnd/Algebra/AffineSpanDescent.leancomplete
theorem RB31E2E.AffineSpanDescent.affineCoefficients_mem_span.{u_1, u_2, u_3, u_4, u_5} {L : Type u_1} {K : Type u_2} {I : Type u_3} {C : Type u_4} {J : Type u_5} [Field L] [Field K] [Algebra L K] [Fintype I] [DecidableEq I] [Fintype C] (rows : J → I → L) (x : C → K) (hx : AlgebraicIndependent L x) (constant : I → L) (coefficient : C → I → L) (hmem : RB31E2E.FiniteFamilyBaseChange.mapVector constant + ∑ j, x j • RB31E2E.FiniteFamilyBaseChange.mapVector (coefficient j) ∈ Submodule.span K (Set.range fun r ↦ RB31E2E.FiniteFamilyBaseChange.mapVector (rows r))) : constant ∈ Submodule.span L (Set.range rows) ∧ ∀ (j : C), coefficient j ∈ Submodule.span L (Set.range rows)
theorem RB31E2E.AffineSpanDescent.affineCoefficients_mem_span.{u_1, u_2, u_3, u_4, u_5} {L : Type u_1} {K : Type u_2} {I : Type u_3} {C : Type u_4} {J : Type u_5} [Field L] [Field K] [Algebra L K] [Fintype I] [DecidableEq I] [Fintype C] (rows : J → I → L) (x : C → K) (hx : AlgebraicIndependent L x) (constant : I → L) (coefficient : C → I → L) (hmem : RB31E2E.FiniteFamilyBaseChange.mapVector constant + ∑ j, x j • RB31E2E.FiniteFamilyBaseChange.mapVector (coefficient j) ∈ Submodule.span K (Set.range fun r ↦ RB31E2E.FiniteFamilyBaseChange.mapVector (rows r))) : constant ∈ Submodule.span L (Set.range rows) ∧ ∀ (j : C), coefficient j ∈ Submodule.span L (Set.range rows)
Bundled form: the constant term and all variable coefficients descend simultaneously.
The Lean statement takes the coefficient family to be indexed by an arbitrary
finite type rather than by \{1,2,3\}, and takes as hypothesis that the family
is algebraically independent over L rather than that 1 together with it is
linearly independent. Algebraic independence is the stronger hypothesis, and
it is the one the exceptional case
provides: \delta_v = 3 says that the three coordinates of a_v are
algebraically independent over L.
The formal proof follows the paper's. A coefficient outside R is separated
by an L-linear functional; extending that functional coordinatewise to K
annihilates the extended row space and leaves an affine relation among 1
and the x_j, which independence forbids.
In the exceptional case, the three rigidity rows on pairs of neighbours belong
to \operatorname{row}_L D_H(a_H).
(Zheng, 2026, Lemma 2.5)
Lean code for Lemma4.5.2●1 theorem
Associated Lean declarations
-
theoremdefined in RB31EndToEnd/Linear/OutsideExceptionalFullResponse.leancomplete
theorem RB31E2E.DirectionStress.outsideExceptional_fullResponse.{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.edgeSetDegree F v = 3 ∧ RB31E2E.DirectionStress.outsideExtensionTrdeg a v = 3 ∧ RB31E2E.DirectionStress.outsideResponseKernelDim F a v = 1 ∧ RB31E2E.PinCollinearity.Collinear (a N.p) (a N.q) (a N.r) ∧ RB31E2E.DirectionStress.directionRow a (RB31E2E.simpleEdge N.p N.q ⋯) ∈ RB31E2E.DirectionStress.directionRowSpace (RB31E2E.deleteVertexEdges F v) a ∧ RB31E2E.DirectionStress.directionRow a (RB31E2E.simpleEdge N.p N.r ⋯) ∈ RB31E2E.DirectionStress.directionRowSpace (RB31E2E.deleteVertexEdges F v) a ∧ RB31E2E.DirectionStress.directionRow a (RB31E2E.simpleEdge N.q N.r ⋯) ∈ RB31E2E.DirectionStress.directionRowSpace (RB31E2E.deleteVertexEdges F v) a
theorem RB31E2E.DirectionStress.outsideExceptional_fullResponse.{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.edgeSetDegree F v = 3 ∧ RB31E2E.DirectionStress.outsideExtensionTrdeg a v = 3 ∧ RB31E2E.DirectionStress.outsideResponseKernelDim F a v = 1 ∧ RB31E2E.PinCollinearity.Collinear (a N.p) (a N.q) (a N.r) ∧ RB31E2E.DirectionStress.directionRow a (RB31E2E.simpleEdge N.p N.q ⋯) ∈ RB31E2E.DirectionStress.directionRowSpace (RB31E2E.deleteVertexEdges F v) a ∧ RB31E2E.DirectionStress.directionRow a (RB31E2E.simpleEdge N.p N.r ⋯) ∈ RB31E2E.DirectionStress.directionRowSpace (RB31E2E.deleteVertexEdges F v) a ∧ RB31E2E.DirectionStress.directionRow a (RB31E2E.simpleEdge N.q N.r ⋯) ∈ RB31E2E.DirectionStress.directionRowSpace (RB31E2E.deleteVertexEdges F v) a
**PF outside full response.** A genuinely exceptional degree-at-most three outside star forces all three virtual neighbour rows into the child row space. The returned packet is the packet produced by the literal exceptional classification.
The neighbour coordinates a_p, a_q, a_r lie in L^3 and are collinear over
K, hence over L, so there is a unique \tau \in L \setminus \{0,1\} with
a_r - a_p = \tau(a_q - a_p). Let the star weighting \mu take the values
1 - \tau, \tau, -1 on vp, vq, vr. Writing
C = (1-\tau) e_p \otimes a_p + \tau e_q \otimes a_q - e_r \otimes a_r and
\Lambda(z) = (1-\tau) e_p \otimes z + \tau e_q \otimes z - e_r \otimes z, a
calculation gives \mu \in \ker C_v = \ker \partial_v, so
C - \Lambda(a_v) \in R_H \otimes_L K where R_H = \operatorname{row}_L D_H(a_H).
By (2.8) the three coordinates of a_v are algebraically independent over
L, so descent of affine coefficients applies and gives
C, \Lambda(e_1), \Lambda(e_2), \Lambda(e_3) \in R_H, hence
\Lambda(z) \in R_H for every z \in L^3. Then
C - \Lambda(a_r) = \tau(1-\tau) r_{pq},
(1-\tau)(C - \Lambda(a_p)) = \tau r_{qr} and
\tau(C - \Lambda(a_q)) = (1-\tau) r_{pr}, and every scalar is nonzero.
The Lean statement combines the classification with this conclusion: one theorem asserts, of one triple of neighbours, the degree, the transcendence degree, the response dimension, the collinearity, and membership of all three neighbour rows in the row space of the deleted graph. The collinearity flag created at this point (the flags chapter) uses the same three vertices in every one of those roles, so the statement has to give one triple rather than several.
The paper works with a_H as an L-valued configuration throughout, and
its collinearity claims move between L and K without comment. The
formalization has a single K-valued placement, so it constructs the
L-valued configuration — v is sent to zero, every other vertex to its
own coordinates — and proves collinearity of the three neighbours over L
from collinearity over K
(collinear_restrictScalars_for_response)
before the descent lemma can be applied.