TheoremStatement: Literature-sourcedProof: 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.

Complete finite-slab production and outward-flux balance

Statement

Assume the ${A C}_{ω}$ background of Finite spacelike slab and normal flux charge. Let $K$ , $Σ_{t}$ , the $C^{1}$ current $J$ , its slice charge $Q_{J} (t)$ and its net outward side flux $Φ_{J} (B)$ be as in Finite spacelike slab and normal flux charge. Use the oriented metric volume form of The metric volume form, current flux through 3-faces and finite-chain charges clause (a). Put $Π : = \nabla_{a} J^{a}$ , using the $C^{1}$ divergence of Metric divergence density identity for a C¹ current. Then the exact finite-slab balance is $Q_{J} (t_{1}) - Q_{J} (t_{0}) + Φ_{J} (B) = \int_{K} Π {v o l}_{g} .$ Here the four-volume integral is the Riemann integral on the bounded Jordan slab $K$ , whose compact closure is the supplied coordinate box. If $Π \geq 0$ everywhere on $K$ , then $Q_{J} (t_{1}) + Φ_{J} (B) \geq Q_{J} (t_{0})$ . In particular, nonnegative local production implies $Q_{J} (t_{1}) \geq Q_{J} (t_{0})$ when the net outward side flux is zero. If $Π = 0$ , the identity instead reads $Q_{J} (t_{1}) - Q_{J} (t_{0}) = - Φ_{J} (B)$ , so zero production alone does not imply constant slice charge.

Facts & Assumptions

Given: The ${A C}_{ω}$ convention, a positively oriented Lorentzian coordinate slab $K = [t_{0}, t_{1}] \times Ω$ with nondegenerate rectangular factors and compact closure $\overline{K}$ , spacelike slices, its future unit normal and induced volume, and a $C^{1}$ current on a neighborhood of $\overline{K}$ .

[A1]

The Countable Choice assumption is the tangent-bundle background recorded in The Axiom of Countable Choice ( ${A C}_{ω}$ ) and Smooth time-oriented Lorentzian four-manifolds: the geometric objects of the model; no additional choice is used.

[F1]

The definition gives the coordinate slice charge $Q_{J} (t) = \int_{Ω} - g (J, n) \sqrt{\det h} d^{3} x$ and net side flux as the sum of upper-minus-lower $w J^{i}$ face integrals (Finite spacelike slab and normal flux charge).

[F2]

On each slice, the normal charge equals its coordinate density integral $Q_{J} (t) = \int_{Ω} w J^{0} d^{3} x$ (Normal slice charge equals its coordinate density integral).

[F3]

For a $C^{1}$ current, $\partial_{a} (w J^{a}) = w \nabla_{a} J^{a}$ (Metric divergence density identity for a C¹ current).

[F4]

The sets $K$ , $Ω$ and each $Ω_{i}$ are bounded Jordan products, and every continuous density on their compact coordinate closures is Riemann integrable on them. In particular, the two endpoints of each closed coordinate interval have content zero, by the one-dimensional case of Finite coordinate boxes and their faces are compact Jordan sets.

[F5]

For an integrable function on a bounded Jordan set whose coordinate sections are integrable outside a content-zero set, its integral equals the iterated section integral; in particular this applies to continuous functions on a product rectangle (Fubini over a bounded Jordan set when all but a content-zero family of sections are integrable).

[F6]

If $G$ is differentiable on a closed interval and $G^{'}$ is integrable, then its integral is $G (b) - G (a)$ , including the one-sided endpoint values (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)$ ).

[F7]

The integral over a Jordan set is the Riemann integral of its zero extension, and on a rectangle an integrable function's integral is the supremum of lower Darboux sums; lower sums use the cell infima times nonnegative rectangle volumes (The Riemann integral of a bounded function over a bounded Jordan measurable set, The lower and upper Darboux integrals over a nondegenerate rectangle in $R^{m}$ , Lower and upper Darboux sums over a grid partition in $R^{m}$ ).

[F8]

In a positively oriented chart, ${v o l}_{g} = w d x^{0} \land d x^{1} \land d x^{2} \land d x^{3}$ (The metric volume form, current flux through 3-faces and finite-chain charges clause (a)).

Proof

technique · direct; apply one-dimensional FTC on each coordinate and sum the six oriented side-face terms

1.1A1F3F4

By [F3], $w Π = \partial_{0} (w J^{0}) + \sum_{i = 1}^{3} \partial_{i} (w J^{i})$ on the coordinate box. Since $g$ and $w$ are smooth and $J$ is $C^{1}$ , this integrand and all face integrands are continuous; [F4] makes their compact-box integrals finite.

1.2F2F5F6

By [F2], $Q_{J} (t) = \int_{Ω} w J^{0} d^{3} x$ . Fix $(x^{1}, x^{2}, x^{3}) \in Ω$ . Apply [F6] to the function $x^{0} \mapsto w J^{0} (x^{0}, x^{1}, x^{2}, x^{3})$ on $[t_{0}, t_{1}]$ , then integrate over $Ω$ using [F5]. This gives $\int_{K} \partial_{0} (w J^{0}) d^{4} x = \int_{Ω} (w J^{0} (t_{1}, x) - w J^{0} (t_{0}, x)) d^{3} x = Q_{J} (t_{1}) - Q_{J} (t_{0}) .$

1.3F1F4F5F6F7

For each fixed $i \in {1, 2, 3}$ and the other three coordinates, the section of $K$ in the $x^{i}$ coordinate is $(a_{i}, b_{i})$ . By [F7], its integral is defined using the zero extension to $[a_{i}, b_{i}]$ . This extension differs from the continuous derivative $x^{i} \mapsto \partial_{i} (w J^{i})$ only at the two endpoints, which have content zero by [F4]; since the functions are bounded, covers of those points by intervals of arbitrarily small total length show from the Darboux definition that the two integrals agree. Apply [F6] on $[a_{i}, b_{i}]$ , then integrate the endpoint difference over the remaining face coordinates by [F5]. This gives $\int_{K} \partial_{i} (w J^{i}) d^{4} x = \int_{Ω_{i}} {w J^{i} ∣}_{x^{i} = b_{i}} - {w J^{i} ∣}_{x^{i} = a_{i}} d^{3} x_{\hat{i}} .$ By [F1], summing these three terms gives exactly $Φ_{J} (B)$ , with outward orientation and no choice of a unit normal on any side face.

1.4A1F1F2F3F5F6constructalgebra

To verify the nonimplication by a current independent of any consuming counterexample, use $M = R^{4}$ with $g = diag (- 1, 1, 1, 1)$ , future direction $\partial_{0}$ , the standard positive coordinate orientation, and $K = [0, 1] \times (0, 1)^{3}$ . Then $w = 1$ , $n = \partial_{0}$ and $d V_{h} = d^{3} x$ , so these are the slab data of [F1]. For real constants $a, b \in [- 1 / 4, 1 / 4]$ , set $J = (2 + a x^{0}) \partial_{0} + b x^{1} \partial_{1}$ . This is smooth on all of $R^{4}$ ; on the compact slab closure, $J^{0} \geq 7 / 4 > ∣ J^{1} ∣$ and $J^{0} > 0$ , so it is even future timelike there and on a neighborhood of the closure. Directly from [F1]–[F3] and the elementary rectangular integrals [F5]–[F6], $Π = a + b, Q_{J} (t) = 2 + a t, Q_{J} (1) - Q_{J} (0) = a, Φ_{J} (B) = b, \int_{K} Π {v o l}_{g} = a + b .$ Indeed only the $x^{1}$ side pair contributes, and its upper-minus-lower density is $b$ on a face parameter rectangle of volume one. These evaluations do not use the balance conclusion or any later example.

2.1step 1.1step 1.2step 1.3F5F8algebra

Add the temporal identity of step 1.2 and the three spatial identities of step 1.3. Additivity of the finite Riemann integral and [F5] give $\int_{K} \sum_{a = 0}^{3} \partial_{a} (w J^{a}) d^{4} x = Q_{J} (t_{1}) - Q_{J} (t_{0}) + Φ_{J} (B) .$ By step 1.1 and the coordinate expression ${v o l}_{g} = w d x^{0} \land d x^{1} \land d x^{2} \land d x^{3}$ in [F8], the left side is $\int_{K} Π {v o l}_{g}$ , proving the equality.

2.2step 1.4algebra

In the family of step 1.4 take $a = - 1 / 4$ and $b = 1 / 4$ . Then $Π = 0$ , $Φ_{J} (B) = 1 / 4$ and $Q_{J} (1) - Q_{J} (0) = - 1 / 4$ . This admissible smooth current has zero production and strictly decreasing slice charge, proving that zero production alone does not imply charge constancy.

3.1step 2.1F7algebra

If $Π \geq 0$ , then $Π w \geq 0$ because $w > 0$ . The zero extension of $Π w$ from $K$ to a containing rectangle is nonnegative; each of its lower Darboux sums is nonnegative by [F7], so $\int_{K} Π {v o l}_{g} \geq 0$ . The equality in step 2.1 yields $Q_{J} (t_{1}) + Φ_{J} (B) \geq Q_{J} (t_{0})$ ; setting the net side flux to zero gives the stated slice-charge inequality. If $Π = 0$ , step 2.1 gives $Q_{J} (t_{1}) - Q_{J} (t_{0}) = - Φ_{J} (B)$ .

4.1step 1.4algebra∎

Taking instead $a = b = 1 / 4$ gives positive production $Π = 1 / 2$ whose integral $1 / 2$ exceeds the positive outward flux $1 / 4$ , with positive charge change $1 / 4$ . Thus zero side flux is sufficient under nonnegative production but is not necessary for nondecreasing charge. The choice $a = 1 / 4$ , $b = - 1 / 4$ also gives zero production, negative net side flux and positive charge change. These explicit cases establish both possibilities without treating a later consuming counterexample as a premise.

Remarks

This is an equality on the stated finite rectangular coordinate slab. It asserts no arbitrary-domain Stokes theorem, infinite exhaustion, boundary at infinity, or convergence result.
For nonnegative production, zero net outward side flux is sufficient for endpoint charge monotonicity. The exact criterion is that integrated production is at least the net outward side flux, as illustrated in proof steps 1.4, 2.2 and 4.1. The theorem places no causal-character restriction on the side faces; their flux is defined by the three-form/coordinate face integral, so null side faces need no unit normal.
This is a pure mathematical identity. A physical entropy interpretation, units, and a local second-law premise must be supplied separately.

Complete finite-slab production and outward-flux balance

Statement

Facts & Assumptions

Proof

Remarks

Depends on

Dependency tree · 2 levels

Sources