Definition. Finite incidence data and real fields [fdip-0002]

Specialize the field modules to \(R=\mathbb R\). The finite sets \(V,E\) and endpoint maps \(s,h:E\to V\) form a finite incidence presentation; its real specialization adds the scalar order needed for positive pairings and weights. A real vertex field is a function \(f:V\to \mathbb R\), written \(f\in \mathbb R^V\) with \(\mathbb R^V=\mathcal F_{\mathbb R}(V)\) and \(\mathbb R^E=\mathcal F_{\mathbb R}(E)\).

Their counting inner products are \[\langle f,g\rangle _V=\sum _{v\in V}f(v)g(v),\qquad \langle a,b\rangle _E=\sum _{e\in E}a(e)b(e).\] These finite sums are bilinear and symmetric. A sum of squares vanishes exactly when all its entries vanish, so they are positive definite, including on the zero space when an indexing set is empty. The real field values remain continuous even though the carrier is finite.

The real incidence map is the specialization \[D=d_{\mathbb R}:\mathbb R^V\longrightarrow \mathbb R^E,\qquad (Df)(e)=f(h(e))-f(s(e)).\] Its linearity is the specialization of the ring-valued incidence map. Loops have zero incidence, and parallel edges remain distinct. For an oriented loopless graph this is the sign convention of [spielman2009effective, Section 2.1, p. 4]; the endpoint formula extends it to loops. Connectedness and positive weights are not needed to define \(D\).

A positive edge-weight function \(w:E\to \mathbb R_{>0}\) is additional data. It acts on edge fields by \((Wa)(e)=w(e)a(e)\). Different weights change the supplied data. No retained subset belongs to this definition. The alternating four-cycle of Example [fdip-0003] is one weighted instance.

For the counting inner product, Mathlib's EuclideanSpace is the corresponding finite function space and PiLp.inner_apply gives the sum of coordinate inner products. These declarations concern the pairing, rather than the incidence presentation as a whole.