5.6. Function-field branches and the semismallness budget🔗

The paper states Theorem 3.9 for a configuration over a finitely generated extension K/k and reads it, equivalently, as a codimension bound on subvarieties of X^\circ_{\mathcal{T}}. The formalization keeps only the first reading. Its object is a function-field branch: a placement \mathrm{pos} : V \to K^3 of the live vertices, together with proofs that the coordinates generate K over k, that the placement is injective, and that every terminal triple is collinear. The branch dimension is the transcendence degree \trdeg_k K, and no codimension, stress bound, or height conclusion is a field of the structure.

The last definition is the inequality the whole induction proves. As noted in the deletion chapter, the paper's defect \Delta(G, \Gamma, a) = s + \trdeg_k K + 2|\Gamma| - 3|V| has no Lean counterpart as a quantity; the statement \Delta \le 0 appears instead as this predicate, in the subtraction-free form

s + \trdeg_k K + 2|\Gamma| \le 3|V|,

where s is stressDim, the self-stress dimension of the live graph at the branch's placement. The paper's bookkeeping identities (3.16) and (3.18) below likewise have no counterparts as equations: each induction step proves the parent's budget from the child's budget and a local payment, and the arithmetic of the defect is carried out inside those proofs.

The formal theorem is provenanceFlag_semismallness: for every state whose completion is sparse and every function-field branch on it, the semismallness budget holds. The strong induction is on the size Fintype.card of the live vertex type, which strictly decreases at every recursive call because each move constructs its child on the subtype of remaining vertices. The base case is the empty live type, where the state's own fields force \Gamma to be empty and coordinate generation forces \trdeg_k K = 0. Each of the four cases of the induction is proved in its own module: the two nonexceptional deletions rest on the local payments proved in the deletion ledger; in the outside exceptional case an edge is inserted or the neighbour triple is registered, with the stress and flag terms changing by exactly two each in the registered alternative; and in the private exceptional case the branch is transported across the pivot before the deletion. We describe those transitions one by one in the closing section.

One hypothesis differs in form. The paper redefines the retained data after each move and reuses the ambient field K; the formalization measures each child by the intermediate field generated by the child's own coordinates inside K, proves that direction-stress rank is unchanged under that restriction of scalars, and descends collinearity of the retained triples to the child field. The equivalence between the two measurements is the intrinsic-placement interface of the deletion ledger, and it is why the induction can pass to a subtype without rebuilding the function field at every step.

The paper proves this by applying Theorem 3.9 with G = F and \Gamma = \emptyset, so that \widehat{G} = F and (3.14) is (1.5). The formalization makes the same specialization: emptyFlagState puts the empty flag type on F, and its completion is F itself. It never states (1.5) as a standalone theorem, however. The assembly of the main theorem uses a grounded form instead: the placement sends a root vertex to zero, the base field is \mathbb{Q}, and the right-hand side is 3(|V| - 1), the number of spatial variables left after grounding. groundedPF_of_provenanceFlag_semismallness derives that form from flag semismallness. It adjoins three independent translation variables to K and translates the placement by them; translatedPlacement leaves every direction row, hence the stress space, unchanged, while the transcendence degree grows by exactly three. Applying the empty-flag budget over the enlarged field and cancelling those three dimensions against the grounding gives the grounded inequality, which then enters endToEndBodyPinStatement_of_groundedPF as its sole hypothesis, and endToEndBodyPinStatement_of_provenanceFlag_semismallness is the composite, from the flag theorem to the body–pin statement. The grounded model itself is the subject of the strata chapter.