The horizon functions are the source's concrete pair, ρ⁻(k, q) = 9^((k+q+1)q) and ρ⁺(k, q) = 9^((k+q)(q+1)), rather than an arbitrary pair satisfying the source's inequalities (1). The statements on this surface are then about a definite logic with definite radii and can be read without carrying a parameter through every one of them. The proofs behind those statements use nothing about the pair beyond the two inequalities of (1), and are written against an abstract bundle of them; that bundle is an implementation detail and is not part of the concept surface.

The distance rank is a predicate on formulas, not a second type index. Its rank argument is independent of the type index: $DRank k' q φ$ may be asserted of a $φ : DistFO L k$ for any $k'$ — the source's "at most k free variables" is $k ≤ k'$, and demanding equality would force a reindexing of the syntax at every step of every proof, for no gain. The source's Observations 4 and 6, which say that rank is preserved along the schedule, become monotonicity lemmas of this predicate.

Deviation, deliberate: the local guard radius is bounded, not pinned. The source's grammar admits the local quantifier only at the exact radius ρ⁺(k+1, q−1); here $DRank$ requires $r ≤ ρ⁺(k'+1, q)$ at rank ($k'$, $q$+1). The source's own Observation 4 — every formula of distance rank (k+1, q−1) with at most k free variables also has distance rank (k, q) — is false for the exact reading as stated: a local quantifier of a (k+1, q−1)-formula guards at ρ⁺(k+2, q−2), which is not the radius ρ⁺(k+1, q−1) that a (k, q)-formula is allowed. The source absorbs the mismatch silently, by reading a guarded quantifier as an unrestricted quantifier over a conjunction with binary distance atoms — a rewriting, not an identity of formulas. With the bound in place the observation is a plain monotonicity lemma about $DRank$, proved where it is used and not here. The relaxation only adds sound inputs: a smaller guard radius means the quantifier ranges over fewer vertices, so every syntactic bound the locality proof draws from a guard still holds.

Satisfaction is total, environments are $Fin k → Fin n$, and binders extend the environment at the last position; see $Lax3.FirstOrder$ for that discussion, which applies verbatim.

The guard of a local quantifier carries its variable set in the syntax: $exL r g φ$ ranges over the vertices within distance r of the variables in the finite set $g$. This is the source's guard dist(x̄, y) ≤ r = ⋁_{x ∈ x̄} dist(x, y) ≤ r read as the source writes it: the set x̄ is chosen when the formula is formed ("we write φ(x̄) to indicate that x̄ contains the free variables of φ") and does not change when the formula later occurs inside a larger one. Recording the set is what makes that stability true here as well — placing a one-variable formula at a bound variable of a wider formula, as the locality theorem's proof and the normal form's written-out scatter sentences both do, keeps its guards reading that one variable, and renaming is sound with no side conditions because the guard set travels along. A guard over everything in scope is the special case $g = univ$; the earlier revision of this file had only that case, which widens a formula's guards whenever the context grows, and under which the placement just described is unsound. With $g = ∅$ the guard is an empty disjunction, so the quantifier is vacuously false — in particular a local quantifier over a sentence's empty context has no vertex to be local to, and the locality theorem's sentence case produces scatter sentences precisely because local quantification cannot help there.

The unary distance atom is strict, dist(x, Y) < r, as in the source; the binary one is not. The asymmetry is the source's and is kept — a translation that quietly aligned them would make the statements here no longer the statements of the source note. Unary distance atoms are carried at all only for faithfulness: the algorithm never manufactures one, and its formulas stay in the fragment without them.

$SatWithin$ is the source's relativization A[N_r(ā)] ⊨ φ(ā), written with the carrier kept: the induced substructure lives on the same vertex type $Fin n$, and the restriction to $D$ is imposed by the definition instead of by a subtype. That matches the uniform vertex numbering every structure of this submission carries, and matches Lax12's $deleteVerts$, which also isolates rather than removes. Inside $D$ the atoms are the induced ones: an edge survives only if both its endpoints do, a color class is intersected with $D$, and a distance atom measures along walks that stay in $D$. Satisfaction and relativization to the full vertex set agree, but $SatWithin univ$ is not how $Sat$ is defined — the agreement is a lemma, proved where the two are compared, so that each definition can be read and audited on its own.

$rename$ is here because the sentences of $Lax3.Locality$ need to place a one-variable formula at each of several bound variables. It is a definition only; the lemmas relating it to satisfaction belong with the proofs that use them.