Alphabeta Math
PropositionStatement: AI-adaptedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 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.

At interior base points, the graph faces of an adapted presentation induce the outward unit normal

Statement

Let (k,D,γ1,γ2) be a simple description of a solid E in the direction k and let Σ be a boundary presentation adapted to it. Let j∈Σ+∪Σ−, let c be an interior point of the parameter region Dj whose projection w0:=πk(φj(c)) lies in the interior of the base D, and put p:=φj(c).

Then p∈∂E, the tangent plane T:=span⁡{φj,u(c),φj,v(c)} is defined, and the induced unit normal of an upper or lower face is the outward unit normal: the vector

N:=φj,u(c)×φj,v(c)∥φj,u(c)×φj,v(c)∥2

is outward at p in the sense of The outward unit normal at a boundary point of a compact solid, while −N is not; so N is the outward unit normal to T at p.

The displayed interior condition makes explicit the part of the base on which the strict graph separation is used below.

Facts & Assumptions

Given: The simple description (k,D,γ1,γ2) of E, the adapted presentation Σ, the index j∈Σ+∪Σ−, the interior parameter point c∈Dj∘ with w0=πk(φj(c))∈D∘, and p=φj(c). Write ψj=πk∘φj, write γ for γ2 when j∈Σ+ and for γ1 when j∈Σ−, and write σk−1(w,t) for the point with πk-projection w and kth coordinate t.

[F1]

E={q∈R3:πk(q)∈D, γ1(πk(q))≤qk≤γ2(πk(q))}, with D compact Jordan of nonempty interior, γ1,γ2 continuous on D, γ1≤γ2 on D and γ1<γ2 on the interior of D (Simple solid regions in a coordinate direction and their cyclic coordinate projection).

[F2]

For j∈Σ+ the image of φj lies in the graph of γ2 and the kth coordinate of φj,u×φj,v is positive on the interior of Dj; for j∈Σ− the image lies in the graph of γ1 and that coordinate is negative on the interior of Dj (Boundary presentations adapted to a simple solid region in a coordinate direction).

[F3]

A regular patch has a compact Jordan parameter region that is the closure of its nonempty interior, its parametrization is C1 on an open neighbourhood of that region, and φu×φv≠0 on the interior (Regular parametrized surface patches on compact Jordan parameter regions).

[F4]

At an interior parameter point the tangent plane of a regular patch is span⁡{φu,φv}, a two-dimensional subspace of R3 (The tangent plane of a regular surface patch).

[F5]

The parametrization induces on the interior the unit normal Nφ=(φu×φv)/∥φu×φv∥2, which is orthogonal to the tangent plane (Unit normal fields, orientations, and flux through a regular surface patch).

[F6]

A unit vector ν is outward at p∈∂E when there is a real ε>0 with p+tν∉E and p−tν∈E for every t with 0<t<ε; when a two-dimensional subspace T is given and one of its two unit normals is outward at p, the other is not, and the outward one is called the outward unit normal to T at p (The outward unit normal at a boundary point of a compact solid).

[F7]

For x,y∈Rm, ⟨x,y⟩=∑i<mxiyi (The Euclidean inner product ⟨x,y⟩=∑k<nxkyk on Rn); the gradient of a scalar function is ∇f=(∂0f,…,∂m−1f) (The Jacobian matrix of partial derivatives and the gradient in the scalar-valued case); a map is Ck when each component is (Ck Euclidean maps and diffeomorphisms); and the Jacobian determinant of a square-dimensional C1 map is det⁡Dg (The Jacobian determinant of a square-dimensional C1 map is the determinant of its Jacobian matrix).

[L1]

If f:U→Rn is C1 on an open U and Df(a) is invertible, then there are open V′,W′ with a∈V′⊆U and f(a)∈W′ such that f∣V′:V′→W′ is bijective with C1 inverse (The Euclidean inverse function theorem).

[L2]

For a C1 map φ of two variables into R3, (φu×φv)k=det⁡D(πk∘φ) (Each coordinate of the oriented area vector is the Jacobian determinant of the matching cyclic projection).

[L3]

If f is totally differentiable at a then Dvf(a) exists for every v and equals Df(a)v, and the matrix of Df(a) is Jf(a) (A total derivative computes every directional derivative, and its matrix is the Jacobian).

[L4]

If f is totally differentiable at a and g at f(a), then D(g∘f)(a)=Dg(f(a))∘Df(a) (The chain rule for total derivatives: D(g∘f)(a)=Dg(f(a))∘Df(a)).

[L5]

If every partial derivative of f exists on a neighbourhood of a and is continuous at a, then f is totally differentiable at a with Df(a) the linear map of matrix Jf(a) (If all partial derivatives exist on a neighbourhood and are continuous at a point, then the map is totally differentiable there with Jacobian derivative).

[L6]

If lim⁡x→cf(x)=L>0 then there is δ>0 with f(x)>L/2>0 for every x in the domain with 0<∣x−c∣<δ; if L<0 then f(x)<L/2<0 there (If lim⁡x→cf(x)=L≠0 then ∣f∣>∣L∣/2 on a punctured neighbourhood of c; in particular if L>0 then f>L/2>0 there).

Proof

technique · direct
1.1givenF2F3F7L1L2

By [F3] the map φj is C1 on an open neighbourhood of Dj, so ψj=πk∘φj is C1 there by [F7], and by [F2] and [L2] its Jacobian determinant at c is nonzero, hence Dψj(c) is invertible. So [L1] supplies open sets P∋c and Q∋w0 with ψj∣P:P→Q bijective and with C1 inverse λ:Q→P; shrinking P and Q, which stays possible because Dj∘ and D∘ are open and contain c and w0, we may take P⊆Dj∘ and Q⊆D∘.

2.1step 1.1F2F7L3L4L5

Let w∈Q. By [F2] the point φj(λ(w)) lies in the graph of γ over D, and its πk-projection is ψj(λ(w))=w, so φj(λ(w))=σk−1(w,γ(w)). Reading the kth coordinate, γ(w)=(φj(λ(w)))k on Q, a composite of C1 maps and therefore C1 on Q by [F7] and [L4]; by [L5] it is totally differentiable at w0, and by [L3] and [F7] its total derivative there acts by v↦⟨g,v⟩ with g:=∇γ(w0).

3.1step 1.1step 2.1F4L3L4

The map Φ(w):=σk−1(w,γ(w)) on Q equals φj∘λ by step 2.1, and its two parameter derivatives at w0 are τi=σk−1(ei,∂iγ(w0)) for i=0,1. By [L4] the derivative DΦ(w0)=Dφj(c)∘Dλ(w0) with Dλ(w0) invertible, so span⁡{τ0,τ1} and span⁡{φj,u(c),φj,v(c)} are the same subspace, namely the tangent plane T of [F4].

4.1step 3.1F2F3F5F7L2

By [F3] and [F5] the vector N is defined at c, has norm 1 and is orthogonal to T. Write N=σk−1(a,b) with a∈R2 and b=Nk; since σk−1 merely permutes coordinates, [F7] gives ⟨σk−1(a,b),σk−1(a′,b′)⟩=⟨a,a′⟩+bb′. Orthogonality to τi of step 3.1 therefore reads ai+b ∂iγ(w0)=0 for i=0,1, that is a=−b g. If b were 0 then a=0 and N=0, contradicting ∥N∥2=1; so b≠0, and by [F2] and [L2] the number b has the sign of det⁡Dψj(c), hence b>0 for j∈Σ+ and b<0 for j∈Σ−.

5.1step 2.1step 4.1F8L3L6

For real t near 0 the projection πk(p+tN)=w0+ta lies in the open Q, so u(t):=(p+tN)k−γ(πk(p+tN))=γ(w0)+tb−γ(w0+ta) is defined there, using pk=γ(w0) from step 2.1. Then u(0)=0, and by step 2.1 and [L3] the function u is differentiable at 0 with u′(0)=b−⟨g,a⟩=b+b∥g∥22=b(1+∥g∥22), using a=−bg from step 4.1. Since u(0)=0, the difference quotient at 0 is u(t)/t, so [F8] and [L6] give ε0>0 such that u(t)/t has the sign of b for every t with 0<∣t∣<ε0; hence u(t) has the sign of tb there.

6.1step 5.1F1F6

Suppose j∈Σ+, so γ=γ2 and b>0 by step 4.1. Shrink ε0 so that πk(p±tN)∈Q⊆D for 0<t<ε0 and so that, γ1 and γ2 being continuous with γ1(w0)<γ2(w0) by [F1], one also has γ1(πk(p−tN))<γ2(w0)−tb there. For 0<t<ε0, step 5.1 gives u(t)>0, that is (p+tN)k>γ2(πk(p+tN)), so p+tN∉E by [F1]; and u(−t)<0, that is (p−tN)k<γ2(πk(p−tN)), while (p−tN)k=γ2(w0)−tb>γ1(πk(p−tN)) by the choice of ε0, so p−tN∈E by [F1]. Hence N is outward at p by [F6].

6.2step 5.1F1F6

Suppose instead j∈Σ−, so γ=γ1 and b<0 by step 4.1. Shrink ε0 so that πk(p±tN)∈Q⊆D for 0<t<ε0 and so that γ2(πk(p−tN))>γ1(w0)−tb there, which is possible since γ1(w0)<γ2(w0) by [F1] and −tb>0 tends to 0. For 0<t<ε0, step 5.1 gives u(t)<0, that is (p+tN)k<γ1(πk(p+tN)), so p+tN∉E by [F1]; and u(−t)>0, that is (p−tN)k>γ1(πk(p−tN)), while (p−tN)k=γ1(w0)−tb<γ2(πk(p−tN)) by the choice of ε0, so p−tN∈E by [F1]. Hence N is outward at p by [F6].

7.1step 6.1step 6.2F6F8∎

In both cases p∈E while p+tN∉E for arbitrarily small t>0, so p is not interior to E and therefore p∈∂E by [F8]. Replacing N by −N exchanges the two conditions of [F6], which then fail, so −N is not outward at p; since ±N are the only unit vectors orthogonal to the two-dimensional T, the vector N is the outward unit normal to T at p.

Remarks

  • Why the projection is interior here. The nonzero projected Jacobian at the interior parameter point makes ψj a local diffeomorphism. Its local image is open and, because the patch image lies in the graph over D, is contained in D; hence w0 is automatically an interior point of D. The Statement records the condition explicitly because steps 6.1 and 6.2 use the strict inequality γ1(w0)<γ2(w0) attached to it.

  • The excluded points are the seams and the edges. Nothing is claimed at a parameter-boundary point of a patch, nor at a point whose projection lies on ∂D. Those points form a set of content zero in every parameter region, which is why no integral identity on this page is affected by them; but a pointwise claim about the normal there would be false in general and is not made.

Depends on

Used by

Dependency tree · two levels

82 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