4.2. Deleting one vertex🔗

The formalization represents L as an IntermediateField of K, generated by the family retainedCoordinates of the three coordinates of every vertex other than v, and \delta_v as a Cardinal. Neither definition mentions the coordinates of v: L uses only the coordinates that survive, and \delta_v is the transcendence degree of the whole of K over it. The bound \delta_v \le 3 is outsideExtensionTrdeg_le_three, and it is proved from the hypothesis that the coordinates of a generate K, not assumed. Finiteness is proved separately, because the ledger below adds \delta_v to a natural number and needs to know that the conversion loses nothing.

The formalization separates the linear algebra from the graph. For arbitrary linear maps A : X \to Y, B : Z \to Y and C : Z \to W, the block map (x, z) \mapsto (Ax + Bz, Cz) has a kernel that surjects onto the kernel of z \mapsto [Bz] with fibre \ker A, and this proves the dimension count finrank_blockKernel directly, rather than as a consequence of exactness. At the graph level, edge weights split along edgeDeletionEquiv, loads split along splitVertexLoads, and under these two identifications the direction equilibrium map is the block map.

Of the two declarations quoted here, connectingMap is the paper's \mu \mapsto [B_v\mu] in the abstract setting — apply B, take the class modulo the image of A — and deletedConnectingClass is its value at the deletion: the source is the kernel of the local equilibrium at v, the target is the space of loads on the retained vertices modulo the image of the retained equilibrium map, and its vanishing on a star weighting says that the load the weighting induces on the retained vertices lies in the retained row space.

The formalization does not state the exactness of (2.3) itself; it states the numerical consequence s = t + u, which is the only form the induction uses.

Both halves of (2.5) are theorems in the formalization: the stress half is directionStressDim_eq_delete_add_outsideResponseKernelDim, and the transcendence-degree half is stated together with the bound \delta_v \le 3 as trdeg_deletion_ledger. The paper's u is formalized as outsideResponseKernelDim, quoted here.

The defect \Delta itself has no Lean counterpart. The inequality \Delta \le 0 appears instead as the predicate SemismallBudget, in the form s + \operatorname{trdeg}_k K + 2|\Gamma| \le 3|V|, where \Gamma is the set of collinearity flags carried by the induction of the flags chapter and the flag-free case is \Gamma = \emptyset. Equation (2.6) therefore has no counterpart as an equation either; its arithmetic is carried out where the predicate is proved, using the local increment u + \delta_v.

If u + \delta_v \le 3, the defect does not increase and the induction hypothesis applies. The formalization defines this inequality as OutsideNonexceptional and the exceptional case as its literal negation, OutsideExceptional, so the two cases exhaust all possibilities by construction.