ExampleConstruction: AI-generatedVerification: AI-adaptedPipeline-generatedprecheck pass

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.

Explicit hypothesis and convention check for the moving-patch flux

Example

Throughout this Example and Verification, the spatial labels are local one-based names: $x_{i} : = x (i - 1)$ for $i = 1, 2, 3$ , $e_{1} = (1, 0, 0)$ , $e_{2} = (0, 1, 0)$ , $e_{3} = (0, 0, 1)$ , and $\partial_{i}$ denotes the canonical coordinate derivative $\partial_{i - 1}$ under this relabeling. Thus the locally named $e_{i}$ has canonical coordinate $1$ at $i - 1$ and $0$ at the other coordinates; the tuples, inner product, cross product, divergence and curl retain the canonical meanings of The Euclidean inner product $⟨ x, y ⟩ = \sum_{k < n} x_{k} y_{k}$ on $R^{n}$ , The cross product in $R^{3}$ and Divergence and curl of a $C^{1}$ vector field. This local notation does not change the zero-based indices of Localization: vanishing integrals or fluxes force a continuous function to vanish.

Take the unit square $D = [0, 1]^{2}$ as parameter region, an open interval $I \subseteq R$ , a function $a \in C^{2} (I)$ with $a > 0$ everywhere, and

$r (u, v, t) : = (a (t) u, a (t) v, 0), B : = e_{3}, v (x, t) : = \frac{a^{'} (t)}{a (t)} (x_{1}, x_{2}, 0) .$

Then $r$ is of class $C^{2}$ on the open set $R^{2} \times I$ , the tangent vectors are $r_{u} = (a, 0, 0)$ and $r_{v} = (0, a, 0)$ with $r_{u} \times r_{v} = (0, 0, a^{2}) \neq 0$ on $D^{\circ} \times I^{\circ} = D^{\circ} \times I$ , the field $B$ is constant with $div B = 0$ , and $v$ is $C^{1}$ on $R^{3} \times I$ with $v (r (u, v, t), t) = (a^{'} (t) u, a^{'} (t) v, 0) = r_{t} (u, v, t)$ ; so the data satisfy the standing hypotheses of Moving parametrized surface patches and their flux. For every $t \in I$ the parametrized flux is $Φ (t) = a (t)^{2}$ , hence $Φ^{'} (t) = 2 a (t) a^{'} (t)$ ; the fixed-time surface integral of $\partial_{t} B$ is $0$ ; and $curl (v \times B) = - 2 (a^{'} (t) / a (t)) e_{3}$ , so patch Stokes gives $\oint_{\partial S (t)} (v \times B) \cdot d r = - 2 a (t) a^{'} (t)$ , exactly the sign in the formula of Transport of flux through a moving patch. Dropping the term $- \oint (v \times B) \cdot d r$ — that is, treating the moving patch as fixed — would leave $Φ^{'} = 0$ , which the direct derivative contradicts whenever $a^{'} (t) \neq 0$ . All maps are of the stated regularity and no singular support is involved; the example verifies the sign convention and the necessity of the motion term, and asserts no physical law.

Facts & Assumptions

Given: The unit square $D = [0, 1]^{2}$ ; an open interval $I \subseteq R$ ; a function $a \in C^{2} (I)$ with $a > 0$ ; the maps $r$ , $B$ , $v$ displayed in the Example; and a fixed time $t \in I$ .

[L1]

Moving patch and transport identity: in the setting of Moving parametrized surface patches and their flux under the declared ${A C}_{ω}$ , with $div B = 0$ on its domain, the flux $Φ (τ) = \int_{D} ⟨ B (r (p, τ), τ), r_{u} (p, τ) \times r_{v} (p, τ) ⟩ d p$ is differentiable on $I$ and, at every $τ \in I$ at which $r_{u} \times r_{v}$ is nonvanishing on $D^{\circ}$ , satisfies $Φ^{'} (τ) = \int_{S (τ)} \partial_{τ} B \cdot n d S - \oint_{\partial S (τ)} (v \times B) \cdot d r$ , with the induced orientation and boundary chain (Transport of flux through a moving patch).

[L2]

The unit square is an elementary Green region: with $a_{0} = 0$ , $b_{0} = 1$ , $α \equiv 0$ , $β \equiv 1$ on $[0, 1]$ , the set $D$ has both the Type I description ${(x, y) : 0 \leq x \leq 1, 0 \leq y \leq 1}$ and the analogous Type II description, so it is a compact elementary Green region, hence a finite elementary Green region, and it is compact and Jordan measurable; its volume is $vol (D) = (1 - 0) (1 - 0) = 1$ (Type I, Type II, and elementary regions for Green's theorem, Axis-parallel rectangles in $R^{m}$ and their volume).

[L3]

Integrals of constants over $D$ : for every constant $c$ , the Riemann integral over the Jordan set $D$ is $\int_{D} c d u d v = c$ . Indeed $D$ is its own nondegenerate bounding rectangle, so by The Riemann integral of a bounded function over a bounded Jordan measurable set $\int_{D} c$ is the Darboux integral of $c$ over $D$ ; on every cell of every grid partition both the infimum and the supremum of $c$ equal $c$ , so every lower and upper Darboux sum equals $c \sum_{i} vol (Q_{i}) = c vol (D) = c$ by Lower and upper Darboux sums over a grid partition in $R^{m}$ , The lower and upper Darboux integrals over a nondegenerate rectangle in $R^{m}$ and Grid partitions of a rectangle in $R^{m}$ , their cells, refinements and mesh, whence the common value is $c$ (Axis-parallel rectangles in $R^{m}$ and their volume).

[L4]

Calculus and vector analysis rules: $a > 0$ makes $a^{'} / a$ of class $C^{1}$ on $I$ and $v$ of class $C^{1}$ jointly in $(x, t)$ ( $C^{k}$ Euclidean maps and diffeomorphisms, Sums, scalar multiples, products and quotients: $(f + g)^{'} (c) = f^{'} (c) + g^{'} (c)$ , $(α f)^{'} (c) = α f^{'} (c)$ , $(f g)^{'} (c) = f^{'} (c) g (c) + f (c) g^{'} (c)$ , and $(f / g)^{'} (c) = (f^{'} (c) g (c) - f (c) g^{'} (c)) / g (c)^{2}$ when $g (c) \neq 0$ ); the product rule gives $(a^{2})^{'} = 2 a a^{'}$ , and the time derivative of the constant field $B$ satisfies $\partial_{t} B \equiv 0$ ; with the Example's local $\partial_{i} = \partial_{i - 1}$ coordinate relabeling, the partial derivatives, divergence, curl, cross product and Euclidean inner product are those of Divergence and curl of a $C^{1}$ vector field, The cross product in $R^{3}$ and The Euclidean inner product $⟨ x, y ⟩ = \sum_{k < n} x_{k} y_{k}$ on $R^{n}$ (The chain rule for total derivatives: $D (g \circ f) (a) = D g (f (a)) \circ D f (a)$ ).

[L5]

Patch Stokes: for a $C^{2}$ patch over a finite elementary Green region and a $C^{1}$ field $G$ on a neighbourhood of its image, $\oint_{φ (\partial D)} G \cdot d r = \int_{D} ⟨ (curl G) \circ φ, φ_{u} \times φ_{v} ⟩$ , with the induced boundary chain, the positive boundary orientation and the line integrals as cited (The classical Stokes theorem for a $C^{2}$ patch over a finite elementary Green region, The induced boundary chain and circulation of a $C^{2}$ patch over a finite elementary Green region, Positive orientation of elementary-region boundaries, Scalar line integrals with respect to arc length and vector-field line integrals, Unit normal fields, orientations, and flux through a regular surface patch).

Verification

technique · direct; evaluate the parametrized flux and its derivative, evaluate the two terms of the transport identity by explicit vector calculus and Stokes, and compare

1.1givenL1L2L4algebra

Setting and regularity. The map $r (u, v, t) = (a (t) u, a (t) v, 0)$ is of class $C^{2}$ on the open set $R^{2} \times I$ , since it is polynomial in $(u, v)$ with $C^{2}$ coefficients, with $r_{u} = (a, 0, 0)$ , $r_{v} = (0, a, 0)$ and $r_{u} \times r_{v} = (0, 0, a^{2}) \neq 0$ on $D^{\circ} \times I$ because $a > 0$ ; further $v (x, t) = \frac{a^{'} (t)}{a (t)} (x_{1}, x_{2}, 0)$ is $C^{1}$ jointly, and $v (r (u, v, t), t) = \frac{a^{'}}{a} (a u, a v, 0) = (a^{'} u, a^{'} v, 0) = r_{t} (u, v, t)$ , while $div B = 0$ for the constant field $B = e_{3}$ . Thus the geometric and analytic hypotheses of [L1] hold, and $D$ is the elementary Green region of [L2]. At each time $D$ has connected interior and $r (\cdot, t)$ is injective since $a (t) > 0$ , so it is a regular patch for the Stokes application [L5].

2.1step 1.1L3L4algebra

The flux and its derivative. At each $τ$ , $⟨ B (r), r_{u} \times r_{v} ⟩ = ⟨ e_{3}, (0, 0, a (τ)^{2}) ⟩ = a (τ)^{2}$ , a constant in $(u, v)$ ; hence by [L3] $Φ (τ) = \int_{D} a (τ)^{2} d u d v = a (τ)^{2}$ . Therefore $Φ^{'} (t) = 2 a (t) a^{'} (t)$ for every $t \in I$ by the product rule of [L4].

2.2step 1.1L3L4L5algebra

The two terms on the right-hand side. Since $B$ is constant, $\partial_{t} B \equiv 0$ and the surface integral $\int_{S (t)} \partial_{t} B \cdot n d S$ vanishes. For the boundary term, [L4] gives $v \times B = \frac{a^{'}}{a} (x_{1}, x_{2}, 0) \times (0, 0, 1) = \frac{a^{'}}{a} (x_{2}, - x_{1}, 0)$ and then $curl (v \times B) = (0, 0, \partial_{1} (- \frac{a^{'}}{a} x_{1}) - \partial_{2} (\frac{a^{'}}{a} x_{2})) = (0, 0, - 2 \frac{a^{'}}{a}) = - 2 \frac{a^{'}}{a} e_{3}$ at time $t$ ; consequently $(curl (v \times B)) \circ r = - 2 \frac{a^{'}}{a} e_{3}$ is constant on $D$ , and patch Stokes [L5] together with the constant-integral fact [L3] gives $\oint_{\partial S (t)} (v \times B) \cdot d r = \int_{D} ⟨ - 2 \frac{a^{'}}{a} e_{3}, (0, 0, a^{2}) ⟩ d u d v = - 2 \frac{a^{'}}{a} a^{2} \int_{D} d u d v = - 2 a (t) a^{'} (t)$ .

3.1step 2.1step 2.2L1algebra∎

Comparison. The direct computations of steps 2.1 and 2.2 give $2 a (t) a^{'} (t) = 0 - (- 2 a (t) a^{'} (t))$ , so the transport formula holds here by direct computation without Choice; under the declared ${A C}_{ω}$ it also instantiates Transport of flux through a moving patch, with the boundary term contributing $+ 2 a (t) a^{'} (t)$ to $Φ^{'}$ ; if that boundary term is dropped, the identity would read $Φ^{'} (t) = 0$ , contradicting step 2.1 whenever $a^{'} (t) \neq 0$ . The example therefore checks the sign convention and the necessity of the motion term at the stated $C^{2}$ / $C^{1}$ regularity without singular support, and it asserts no physical law.

Remarks

When $a$ is constant, $Φ (t) = a^{2}$ is constant, both terms of the identity vanish, and the contrast with the fixed-patch reading disappears; the example's discriminating case is therefore any $t$ with $a^{'} (t) \neq 0$ .
The computation uses no choice principle; it is finite algebra and one application of the published Stokes theorem for a patch over the unit square.

Explicit hypothesis and convention check for the moving-patch flux

Example

Facts & Assumptions

Verification

Remarks

Depends on

Dependency tree · 2 levels

Sources