Alphabeta Math
ExampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passaudited 2026-08-26
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.

The outward flux of the inverse-square field through a sphere centred at the origin is 4π

Example

Let F(x,y,z)=(x,y,z)(x2+y2+z2)3/2 on R3∖{0}, and let SR={(x,y,z):x2+y2+z2=R2} with R>0. Then the outward flux of F through SR is 4π, independent of R.

Facts & Assumptions

Given: A radius R>0, the spherical parametrization φ(ϕ,θ)=R(sin⁡ϕcos⁡θ,sin⁡ϕsin⁡θ,cos⁡ϕ) on [0,π]×[0,2π], and the inverse-square field F on R3∖{0}.

[F1]

For a regular parametrized surface patch, the flux in the orientation induced by φ is ∫D(F∘φ)⋅(φu×φv) (Unit normal fields, orientations, and flux through a regular surface patch).

[F2]

A regular patch may degenerate on its parameter boundary, but on the parameter interior its cross product is nonzero and no interior parameter point shares its image with a distinct parameter point (Regular parametrized surface patches on compact Jordan parameter regions).

[F3]

For a finite patch presentation, the total flux is the sum of the patch fluxes (Finitely patched regular surfaces, their area, scalar integrals, and flux).

[F4]

The cross product is that of The cross product in R3.

[L1]

(sin⁡t)′=cos⁡t and (cos⁡t)′=−sin⁡t (The derivatives of sine and cosine are cosine and minus sine).

[L2]
[L5]

Sine is positive on (0,π), cosine is strictly decreasing on [0,π], cos⁡0=1, cos⁡π=−1, and θ↦(cos⁡θ,sin⁡θ) is injective on [0,2π) (Signs, monotonicity intervals, and ranges of sine and cosine, Quarter-turn values and shifts by pi/2 and pi, t↦(cos⁡t,sin⁡t) is a bijection from [0,2π) onto the real unit circle).

[L3]

Jordan Fubini computes a multiple integral by iterated section integrals (Fubini over a bounded Jordan set when all but a content-zero family of sections are integrable).

[L4]

If a<b, G is differentiable on [a,b], and G′=f is integrable there, then ∫abf=G(b)−G(a) (The second fundamental theorem: if G is differentiable on [a,b] with G′=f and f is integrable, then ∫abf=G(b)−G(a)).

[F6]

The divergence theorem for an elementary solid region assumes a C1 field on an open set containing the solid (The divergence theorem on an elementary solid region).

Verification

technique · direct
1.1F1F2F4L1L2L5F5given

On the parameter interior 0<ϕ<π and 0<θ<2π, equality of two spherical images first forces equality of ϕ because cosine is strictly decreasing on [0,π], and then equality of θ by the injectivity of the unit-circle parametrization in [L5]. The cross product is nonzero there because sin⁡ϕ>0 by [L5]; any degeneracy or repeated image occurs only on the parameter boundary. Thus [F2] makes it a regular patch. Differentiating φ and using [F4], [L1], [L2], and [F5] gives φϕ×φθ=Rsin⁡ϕ φ(ϕ,θ), while F(φ(ϕ,θ))=φ(ϕ,θ)/R3, so the flux integrand is (F∘φ)⋅(φϕ×φθ)=sin⁡ϕ.

2.1step 1.1L1L3L4L5F3

By [L3], [L4], [L5], and the identity (cos⁡ϕ)′=−sin⁡ϕ from [L1], the flux is ∫02π∫0πsin⁡ϕ dϕ dθ=∫02π2 dθ=4π, independent of R.

3.1step 2.1F6F5∎

The divergence theorem is not being applied here: the field is undefined at the origin, so it is not C1 on any open set containing the closed ball bounded by SR, and [F6] names exactly that missing hypothesis.

Remarks

  • The independence of R is the point-source phenomenon behind the later false statement: moving the sphere without enclosing the origin changes the answer to 0, but changing only the radius does not.

Depends on

Used by

Dependency tree · two levels

68 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