Remark. Polynomial functions do not depend on a basis [fdip-002V]

For a finite-dimensional real vector space \(E\), the actual polynomial function algebra used in Proposition [fdip-002A] is independent of coordinates. It is the real unital subalgebra of functions \(E\to \mathbb R\) generated by linear functionals. In a chosen basis, every linear functional is a finite linear combination of coordinate evaluations. Conversely every coordinate evaluation is linear. Thus these generators give exactly the coordinate polynomial algebra of that note. Substituting linear combinations in a finite polynomial gives a finite polynomial, so changing basis preserves the algebra.

Its operations and identity involution are pointwise, and its functions are continuous, hence Borel for the finite-dimensional topology. For \(E=0\), the algebra consists of constants. These are actual functions; formal polynomial expressions and their polynomial rings are related algebraic vocabulary, not a second choice of observable functions here.

This coordinate-independence argument is a direct deduction from the generators. The algebra and star conventions are those already used in Proposition [fdip-002A]. For these conventions, see [stacks2017stacks, Section 22.2], Tag 09JF and [waldmann2004states, Definition 3.9, p. 11]. Neither citation asserts Gaussian integrability.