addBase
plain-language theorem explainer
Componentwise sum of two vectors in ℝ⁴ (indexed by Fin 4). Gravity analysts cite it when shifting a hinge base by a star-member offset in the Path B position-resolved local-incidence construction. The body is a one-line pointwise addition; no proof content.
Claim. For $x,\delta\in\mathbb{R}^4$, the shifted base is the vector with components $(x+\delta)_i=x_i+\delta_i$ for each coordinate $i\in\{0,1,2,3\}$.
background
The module develops Path B local-incidence kernels in a 4D continuum setting. Layer 1 is mean-local and vacuous by linearity; layer 2 is position-resolved and non-vacuous: expand the star as a sum of assembled star-members evaluated at cube-translate bases of the form hinge base plus a permuted member offset, then weight by $1/r_\tau$.
Coordinates live on $\mathrm{Fin},4\to\mathbb{R}$, i.e. ordinary $\mathbb{R}^4$ vectors. Shifting a base point by an offset is the elementary operation this definition names. Upstream kernel families (BIT and ILG) appear in the broader gravity stack as weighting factors, not inside this arithmetic helper.
proof idea
Pure definition: the body is the lambda $i\mapsto x_i+\delta_i$. No lemmas, no tactics, no axioms.
why it matters
Feeds phasedT11PositionResolved, the position-resolved deficit phased class-dot for type $(1,1)$: sum of local kernels at bases of the form base plus perm(offset). That construction is the non-vacuous half of Path B (missing-factor blocker). Measured receipts report t11 agreement with distinct-hinge on tested TT rays; t12 still fails symbolDir plus/cross and does not hit the EH $-1/4$ target. The helper itself is only the coordinate shift that makes those cube-translate bases well-typed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.