ExampleConstruction: AI-generatedVerification: AI-generatedPipeline-generated

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Compact boundaryless Gauss neutrality

Example

Fix periods $L_{1}, L_{2}, L_{3} > 0$ and use the smooth quotient geometry and global forms and vector fields supplied by The scaled three-torus as a smooth compact flat spatial manifold. In its coordinates set $M : = R_{x^{0}} \times T_{L}^{3}$ , with $g = - (d x^{0})^{2} + (d x^{1})^{2} + (d x^{2})^{2} + (d x^{3})^{2}$ , orientation $d x^{0} \land d x^{1} \land d x^{2} \land d x^{3}$ , and time orientation $N = \partial_{0}$ . Fix $c, μ_{0} > 0$ as real coefficients and put

$\tilde{f} (x) : = \cos (\frac{2 π x^{1}}{L_{1}}), \tilde{h} (x) : = \frac{L_{1}}{2 π} \sin (\frac{2 π x^{1}}{L_{1}}) .$

These lifts on $R^{3}$ are independent of $x^{2}, x^{3}$ and are $Λ$ -periodic. Let $f, h : T_{L}^{3} \to R$ be their unique smooth descents, so $f \circ q = \tilde{f}$ and $h \circ q = \tilde{h}$ . The descended global vector field $\partial_{1}$ satisfies $\partial_{1} h = f$ and $d h = f d x^{1}$ . On the lifts, ${\tilde{h}}^{'} = \tilde{f}$ and $\tilde{h} (L_{1}, x^{2}, x^{3}) = \tilde{h} (0, x^{2}, x^{3})$ . Define the smooth current and field

$j : = f \partial_{0}, F : = - μ_{0} h d x^{0} \land d x^{1} .$

Let $ι_{*} : T_{L}^{3} \to M$ be the slice inclusion $y \mapsto (x_{*}^{0}, y)$ , and let $T_{3} : = {s \in R^{3} : s_{i} \geq 0, s_{1} + s_{2} + s_{3} \leq 1} .$ Orient the slice by the restriction of the global form $d x^{1} \land d x^{2} \land d x^{3}$ . Let $θ : T_{3} \to Δ^{3}$ be the affine identification $θ (s) = (1 - s_{1} - s_{2} - s_{3}, s_{1}, s_{2}, s_{3})$ . Let $Σ$ be the oriented spatial slice $x^{0} = x_{*}^{0}$ , represented as a finite smooth singular chain as follows. Triangulate the fundamental cube $[0, L_{1}] \times [0, L_{2}] \times [0, L_{3}]$ by the six tetrahedra indexed by $σ \in S_{3}$ . The ordered vertices of tetrahedron $σ$ are $0$ , $L_{σ (1)} e_{σ (1)}$ , $L_{σ (1)} e_{σ (1)} + L_{σ (2)} e_{σ (2)}$ , and $(L_{1}, L_{2}, L_{3})$ . Let $ϕ_{σ} : T_{3} \to R^{3}$ be the affine map taking $0, e_{1}, e_{2}, e_{3}$ to these ordered vertices; it extends affinely to $R^{3}$ . Define the smooth singular simplex $ψ_{σ} : = ι_{*} \circ q \circ ϕ_{σ} \circ θ^{- 1} : Δ^{3} \to M$ ; in the standard $T_{3}$ parameter it satisfies $ψ_{σ} \circ θ = ι_{*} \circ q \circ ϕ_{σ}$ . It extends smoothly to a neighborhood of $Δ^{3}$ in its affine plane because $ϕ_{σ}$ extends affinely and $q, ι_{*}$ are smooth. Put $Σ : = \sum_{σ \in S_{3}} sgn (σ) ψ_{σ}$ . Thus each simplex maps into the slice of $M$ . The determinant of the ordered edge vectors is $L_{1} L_{2} L_{3} sgn (σ)$ , so this coefficient gives each simplex the cube orientation. The six regions are the orderings $0 \leq u_{σ (3)} \leq u_{σ (2)} \leq u_{σ (1)} \leq 1$ of $u_{i} : = x^{i} / L_{i}$ ; their interiors are disjoint and their union is the cube. Internal faces cancel in pairs, and opposite cube faces are identified by period translations with opposite boundary orientations, as verified below.

The perspective box depicts the fundamental cube, with opposite faces paired by the labels. Its dotted body diagonal is the shared edge of the six affine tetrahedra indexed by coordinate permutations. The drawing is schematic and is not used in the chain-boundary proof above.

Facts & Assumptions

Given: $L_{i}, c, μ_{0} > 0$ , the product Lorentzian geometry and the smooth fields in the Example.

[F1]

The scaled three-torus as a smooth compact flat spatial manifold proves the quotient is a smooth compact boundaryless torus, the global $d x^{i}, \partial_{i}$ descend, and on the product $M$ the metric components are constant $η = diag (- 1, 1, 1, 1)$ , the Christoffel symbols vanish, and ${v o l}_{g} = d x^{0} \land d x^{1} \land d x^{2} \land d x^{3}$ .

[F2]

The alternating current-flux form is $ι_{j} {v o l}_{g}$ and charge is $Q (Σ) = c^{- 1} \int_{Σ} ι_{j} {v o l}_{g}$ (The metric volume form, current flux through 3-faces and finite-chain charges, Gauss charge and finite-chain flux balance).

[F3]

For any finite smooth singular three-cycle on which a smooth sourced Maxwell field is defined, the Gauss lemma Gauss charge and finite-chain flux balance gives zero total charge.

[F4]

The smooth tangent-bundle conventions inherited from Oriented Lorentzian fields, observers and coordinate conventions and Gauss charge and finite-chain flux balance use ${A C}_{ω}$ ; the finite torus chain below is explicit and uses no additional choice (The Axiom of Countable Choice ( ${A C}_{ω}$ )).

[F5]

The boundary of an ordered smooth singular $3$ -simplex is the alternating sum of its four face maps, and the boundary of a finite chain is the finite sum of these boundaries (Smooth singular chain and cochain complexes).

[F6]

The power-series definitions and convergence, followed by repeated termwise differentiation, make $\sin$ and $\cos$ smooth. Their first derivatives are $\cos$ and $- \sin$ , and both have period $2 π$ (Sine and cosine defined by their real power series, The sine and cosine power series converge absolutely for every real argument, Inside its radius a real power series may be differentiated term by term, and the differentiated series has the same radius, The derivatives of sine and cosine are cosine and minus sine, The zero sets of sine and cosine and the least positive common period 2 pi).

[F7]

The chain rule gives ${\tilde{h}}^{'} = \tilde{f}$ on the lift; hence $\partial_{1} h = f$ for the descended functions. The continuous lift derivative is Riemann integrable, and its integral equals the endpoint difference of $\tilde{h}$ (The chain rule for total derivatives: $D (g \circ f) (a) = D g (f (a)) \circ D f (a)$ , A continuous function on $[a, b]$ is Riemann integrable, by Heine-Cantor and Riemann's criterion, The lower and upper Darboux integrals of a bounded $f$ on $[a, b]$ as $\sup_{P} L (f, P)$ and $\inf_{P} U (f, P)$ , Darboux integrability as their equality, and the notation $\int_{a}^{b} f$ , The second fundamental theorem: if $G$ is differentiable on $[a, b]$ with $G^{'} = f$ and $f$ is integrable, then $\int_{a}^{b} f = G (b) - G (a)$ ).

[F8]

The published definition Integral of a form over a smooth singular simplex defines the integral of a smooth $3$ -form over a smooth singular $3$ -simplex $σ$ as the Jordan-set Riemann integral of the coefficient of its pullback in the standard positive affine coordinates on $T_{3} = {(s_{1}, s_{2}, s_{3}) : s_{i} \geq 0, s_{1} + s_{2} + s_{3} \leq 1}$ ; it also establishes that $T_{3}$ is compact Jordan. The published, audited change-of-variables theorem Change of variables for an injective $C^{1}$ map on a compact Jordan set states: if $U \subseteq R^{3}$ is open, $ϕ : U \to R^{3}$ is injective and $C^{1}$ with $D ϕ$ invertible throughout $U$ , and $K \subseteq U$ is compact Jordan, then for bounded $u : ϕ (K) \to R$ the two integrability conditions are equivalent and, when they hold, $\int_{ϕ (K)} u (y) d y = \int_{K} u (ϕ (s)) ∣ \det D ϕ (s) ∣ d s .$ Its proof also establishes compact Jordan status of $ϕ (K)$ .

[F9]

The published boundary criterion says a Euclidean-metric-bounded set is Jordan measurable exactly when its boundary has content zero (A bounded set in $R^{m}$ is Jordan measurable iff its boundary is null, equivalently of content zero). The published graph theorem says the graph of a continuous function on a closed nondegenerate rectangle has content zero (The graph of a continuous function on a closed nondegenerate rectangle in $R^{m}$ has content zero in $R^{m + 1}$ ). The published compact-Jordan integrability theorem states that a continuous function on a compact Jordan set is integrable there (A continuous real function on a compact Jordan measurable set is Riemann integrable over that set), and closed bounded subsets of $R^{3}$ are compact (Heine-Borel in $R^{n}$ : with the Euclidean metric a subset of $R^{n}$ is compact if and only if it is closed and bounded, and the proof by bisection uses no choice principle; the same holds on the real line). Content zero passes to subsets and finite unions because a subset inherits a finite cube cover and finitely many such covers can be combined (Measure zero and content zero in $R^{m}$ by countable and finite cube covers). If bounded Jordan sets $A_{1}, \dots, A_{N}$ fill a bounded Jordan set $A$ up to a content-zero remainder, have pairwise content-zero intersections, and a bounded function is integrable on $A$ and every $A_{i}$ , then the published finite-additivity lemma Additivity of the integral over finitely many Jordan pieces that fill a Jordan set up to content zero gives $\int_{A} g = \sum_{i} \int_{A_{i}} g$ .

[F10]

The published theorem Every continuous function on a closed nondegenerate rectangle in $R^{m}$ is Riemann integrable says every continuous real function on a closed nondegenerate rectangle in $R^{m}$ is Riemann integrable. The published rectangular Fubini theorem Riemann--Fubini on product rectangles, with lower and upper section integrals and content-zero exceptional sections says that for an integrable function on a product of nondegenerate rectangles, the iterated section integrals exist when the sections in that order are integrable and equal the multiple integral. The published multidimensional Darboux definition The lower and upper Darboux integrals over a nondegenerate rectangle in $R^{m}$ gives the common lower/upper sum value when they agree, and rectangle volume is the product of side lengths by the published definition Axis-parallel rectangles in $R^{m}$ and their volume; in particular, a constant $a$ on a rectangle $R$ has integral $a vol (R)$ because each lower and upper Darboux sum has that value.

Verification

Given: [F1]–[F10], the geometry, fields and finite chain defined in the Example.

1.1givenF1constructalgebra

For a fixed permutation $σ$ , the barycentric coordinates of a point in the ordered region $0 \leq u_{σ (3)} \leq u_{σ (2)} \leq u_{σ (1)} \leq 1$ relative to its four listed vertices are $1 - u_{σ (1)}$ , $u_{σ (1)} - u_{σ (2)}$ , $u_{σ (2)} - u_{σ (3)}$ , and $u_{σ (3)}$ ; these are nonnegative, sum to one, and reconstruct the point. Thus the six tetrahedra cover the cube with disjoint interiors. Each $ϕ_{σ}$ extends affinely to $R^{3}$ , so $ψ_{σ} = ι_{*} \circ q \circ ϕ_{σ} \circ θ^{- 1}$ extends smoothly to the affine plane containing $Δ^{3}$ and is a smooth singular simplex into $M$ . The ordered edge determinant is $L_{1} L_{2} L_{3} sgn (σ)$ , so the weight $sgn (σ)$ orients each tetrahedron by $d x^{1} \land d x^{2} \land d x^{3}$ .

1.2givenF1F6F7algebra

The periodic lifts are smooth by [F6], and their descents are smooth by the torus lemma; [F6]–[F7] give $\partial_{1} h = f$ , so $F$ and $j$ are smooth global fields on the product. Since $d h = f d x^{1}$ , $d F = - μ_{0} f d x^{1} \land d x^{0} \land d x^{1} = 0$ , the homogeneous equation holds. Raising indices gives $F^{01} = μ_{0} h$ and $F^{10} = - μ_{0} h$ . Thus $\nabla_{a} F^{a 0} = \partial_{1} F^{10} = - μ_{0} f = - μ_{0} j^{0}$ , $\nabla_{a} F^{a 1} = \partial_{0} F^{01} = 0 = - μ_{0} j^{1}$ , and the $b = 2, 3$ equations have both sides zero. Thus both field equations are verified everywhere.

2.1givenF5step 1.1algebra

An internal facet arises by setting one adjacent-coordinate inequality to equality. The two permutations differ by swapping those adjacent entries; their omitted vertices occupy the same position in the ordered vertex lists, and the remaining three vertices have the same order. Thus the face maps in [F5] are identical, while the permutation signs are opposite. Their two coefficients in the signed face boundary therefore sum to zero. This covers both internal facet types (equal first and second coordinates, or equal second and third coordinates).

2.2givenF1F5step 1.1algebra

Fix a coordinate $i$ and order the other two indices as $(a, b)$ . The triangle on $x^{i} = L_{i}$ comes from permutation $(i, a, b)$ by omitting vertex $0$ ; its ordered vertices are $L_{i} e_{i}$ , $L_{i} e_{i} + L_{a} e_{a}$ , and $L_{i} e_{i} + L_{a} e_{a} + L_{b} e_{b}$ . The triangle on $x^{i} = 0$ comes from $(a, b, i)$ by omitting the final vertex; its ordered vertices are $0$ , $L_{a} e_{a}$ , and $L_{a} e_{a} + L_{b} e_{b}$ . Translation by $L_{i} e_{i}$ makes these vertex lists identical, so their quotient face maps are equal. Moving $i$ from first to last is two transpositions, so the permutation coefficients agree; the omitted-vertex boundary signs are $+ 1$ and $- 1$ . By [F5] the corresponding face terms cancel. This pairs every outer triangle, for all three coordinates and both orders $(a, b)$ .

2.3givenF1F2F8F9step 1.1algebraconstruct

Let $C = [0, L_{1}] \times [0, L_{2}] \times [0, L_{3}]$ and let $T_{σ} \subset C$ be the affine tetrahedron with the ordered vertices specified in the Example; each $T_{σ}$ is closed and bounded, hence compact by [F9], so the continuous lift $\tilde{f}$ is bounded there. The standard $T_{3}$ is compact Jordan by [F8]. Write $ϕ_{σ} : T_{3} \to T_{σ}$ for the affine parametrization already defined. The standard positive $T_{3}$ parameterization of $ψ_{σ}$ is $ψ_{σ} \circ θ = ι_{*} \circ q \circ ϕ_{σ}$ . Since $j = f \partial_{0}$ and ${v o l}_{g} = d x^{0} \land d x^{1} \land d x^{2} \land d x^{3}$ by [F1], the interior-product definition in [F2] gives $ι_{j} {v o l}_{g} = f d x^{1} \land d x^{2} \land d x^{3}$ . The pullback of $ι_{j} {v o l}_{g}$ by $ψ_{σ} \circ θ$ has coefficient $\tilde{f} (ϕ_{σ}^{1} (s)) \det D ϕ_{σ}$ in the standard positive affine coordinates, because $q$ pulls back the descended spatial coordinate forms to the Euclidean coordinate forms and $ι_{*}$ restricts them to the slice [F1]. By [F8] this is the coefficient whose integral defines $\int_{ψ_{σ}} ι_{j} {v o l}_{g}$ . This coefficient is continuous on compact Jordan $T_{3}$ , hence integrable by [F9]. The determinant of the three edge vectors is $\det D ϕ_{σ} = L_{1} L_{2} L_{3} sgn (σ)$ , so the chain coefficient gives $sgn (σ) \int_{ψ_{σ}} ι_{j} {v o l}_{g} = \int_{T_{3}} \tilde{f} (ϕ_{σ}^{1} (s)) ∣ \det D ϕ_{σ} ∣ d s = \int_{T_{σ}} \tilde{f} (x^{1}) d x^{1} d x^{2} d x^{3} .$ The last equality is [F8]'s change-of-variables formula: $T_{3}$ is compact Jordan, $ϕ_{σ}$ extends to an injective affine $C^{1}$ map on $R^{3}$ with nonsingular constant derivative, and $\tilde{f}$ is bounded and continuous on $T_{σ}$ . The cube $C$ and each $T_{σ}$ are closed and bounded, hence compact by Heine--Borel, and they are bounded Jordan sets. Indeed their boundaries are finite unions of bounded pieces of affine planes; each such piece is contained in the graph of an affine function over a containing closed nondegenerate rectangle after solving the plane equation for a coordinate with nonzero normal component. These graphs have content zero by [F9], so the boundary criterion in [F9] applies. By step 1.1 the six $T_{σ}$ cover $C$ and have disjoint interiors. Thus each pairwise intersection is contained in the union of their boundaries and has content zero by finite-union and subset closure in [F9], while the remainder $C ∖ ⋃_{σ \in S_{3}} T_{σ}$ is empty. The coefficient $\tilde{f}$ is continuous and bounded on the compact Jordan sets $C, T_{σ}$ , so all integrals in the finite additivity hypotheses are defined by [F9]. Applying the finite Jordan-set additivity result in [F9] and using the chain definition in [F2] gives $Q (Σ) = \frac{1}{c} \sum_{σ \in S_{3}} sgn (σ) \int_{ψ_{σ}} ι_{j} {v o l}_{g} = \frac{1}{c} \int_{C} \tilde{f} (x^{1}) d x^{1} d x^{2} d x^{3} .$

3.1givenF3F4F5step 2.1step 2.2algebra

The finite chain boundary is the alternating face sum in [F5]. Steps 2.1 and 2.2 cancel every internal and external face term, respectively. Hence $\partial Σ = 0$ , as required in [F3]. The explicit finite triangulation adds no choice, as [F4] records.

4.1givenF3step 3.1

Since $\partial Σ = 0$ by step 3.1, the finite-chain neutrality result [F3] applies and gives $Q (Σ) = 0$ .

5.1givenF7F10step 2.3algebra∎

Write $A = [0, L_{1}]$ and $B = [0, L_{2}] \times [0, L_{3}]$ , so $C = A \times B$ . The lift $\tilde{f} (x^{1})$ is continuous on $C$ and hence integrable there by [F10]. Rectangular Fubini [F10] applies, and its sections over $B$ are the constant function $\tilde{f} (x^{1})$ . The multidimensional Darboux sums and volume formula in [F10] therefore give $\int_{C} \tilde{f} (x^{1}) d x^{1} d x^{2} d x^{3} = L_{2} L_{3} \int_{0}^{L_{1}} \tilde{f} (x^{1}) d x^{1} .$ By [F7], ${\tilde{h}}^{'} = \tilde{f}$ and the one-dimensional FTC gives $\int_{0}^{L_{1}} \tilde{f} (x^{1}) d x^{1} = \tilde{h} (L_{1}) - \tilde{h} (0) = 0$ , since the sine values at $0$ and $2 π$ agree. Hence the direct integral computation also yields $Q (Σ) = 0$ , in agreement with step 4.1.

Remarks

This is a mathematical model with smooth fields. It illustrates the compact-cycle constraint without using a point source or a boundary at infinity; it does not report a measurement or assert that the model describes nature.

Compact boundaryless Gauss neutrality

Example

Facts & Assumptions

Verification

Remarks

Depends on

Dependency tree · 2 levels

Sources