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.
Internal faces cancel for glued boxes
Example
Assume and . The boxes and glue to up to their common face. For their divergence identities sum to the identity on Q because the common fluxes cancel. The same calculation applies after replacing the coordinate intervals by arbitrary positive-length adjacent intervals.
Facts & Assumptions
Given: Assume , , the two explicit adjacent boxes and final box Q in the Example, and .
The specified finite-face theorem includes cancellation. (Divergence for finite piecewise C1 presentations).
Verification
For a box , its 2n faces are and , with remaining coordinates in their closed intervals. Each is a compact subset of an affine regular hypersurface, with area element the ordinary product measure and outward normal or . Put every face boundary (at least two endpoint coordinates) into E. On each face it is a finite union of parameter-coordinate hyperplanes and is null: a bounded hyperplane strip has arbitrarily small volume by giving the fixed coordinate an arbitrarily short interval. Off E exactly one coordinate is an endpoint and the domain is locally on one side of that plane. Thus all three boxes satisfy the specified finite-face conditions.
The common face has normal for and for . The same continuous F has the same trace on both sides, so the sum of its flux densities is pointwise off E. F1 applies to both restrictions of F. Their volume integrals add to the integral on Q because the omitted plane S is volume-null by the strip argument in step 1.1. Their exposed face integrals add to the faces of Q, while the two integrals over S cancel. This proves the asserted identity and all required gluing data.
For , the divergence is n and each small box has volume one. On the face contributes 1 and contributes 0; on the face contributes 1 and contributes 0. For each the face contributes 1 on each box and contributes 0. Each box therefore has flux , and Q has flux , equal to its volume integral. For the further constant field the shared fluxes are explicitly 1 and -1, exhibiting nonzero cancellation.
Source notes
Hunter §1.12, discussion following Theorem 1.46, printed p. 18 (PDF p. 24). The faces and field calculation below make the finite-gluing instance explicit.
Depends on
Used by
- A box is not a C1-boundary domain Counterexample
Dependency tree · two levels
10 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.
Sources
- Hunter, Notes on Partial Differential Equations (standard reference, not scraped)