Alphabeta Math
ExampleConstruction: Literature-sourcedVerification: AI-adaptedSession-authored (Fable 5 assisted)precheck 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]

(sint)=cost and (cost)=sint (The derivatives of sine and cosine are cosine and minus sine).

[L2]
[L5]

Sine is positive on (0,π), cosine is strictly decreasing on [0,π], cos0=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(cost,sint) 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.1

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ϕ.

F1F2F4L1L2L5F5given
2.1

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

step 1.1L1L3L4L5F3
3.1

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.

step 2.1F6F5

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

66 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