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

The closed unit box, with its six faces, is an elementary solid region

Example

Let B:=[0,1]3 and let S:=[0,1]2 with parameters (u,v). Then the six faces of the closed unit box, each parametrized on the unit square so that its oriented area vector points out of the box, form one presentation adapted in all three coordinate directions, so B is an elementary solid region (Elementary solid regions: one boundary presentation adapted in all three coordinate directions) with that presentation. The six parametrizations are

φz+(u,v)=(u,v,1),φz(u,v)=(v,u,0),φx+(u,v)=(1,u,v), φx(u,v)=(0,v,u),φy+(u,v)=(v,1,u),φy(u,v)=(u,0,v),

all on S, and their oriented area vectors are the constants ez, ez, ex, ex, ey and ey respectively.

Facts & Assumptions

Given: The box B=[0,1]3, the square S=[0,1]2, and the six parametrizations displayed above.

[F1]

For u=(ux,uy,uz) and v=(vx,vy,vz) in R3, u×v=(uyvzuzvy,uzvxuxvz,uxvyuyvx) (The cross product in R3), and ek has kth coordinate 1 and the others 0 (The standard list e:nFn with ei(i)=1F and ei(j)=0F for ji is an ordered basis of Fn; hence dimFFn=n, and F0 is the zero space with basis and dimension 0, The Euclidean inner product x,y=k<nxkyk on Rn).

[F2]

A regular parametrized surface patch has a compact Jordan parameter region that is the closure of its nonempty connected interior, a parametrization C1 on an open neighbourhood of it, nonvanishing parameter cross product on the interior, and no interior parameter point sharing its image with a distinct point of the region (Regular parametrized surface patches on compact Jordan parameter regions).

[F3]

A compatible finite patch presentation is a finite list of regular patches whose images cover a set, such that for two distinct patches the preimage of their overlap has content zero in each parameter region, and whose induced normals agree at every point of the overlap that is the image of an interior parameter point of both (Finitely patched regular surfaces, their area, scalar integrals, and flux).

[F4]

A simple description of a solid in the direction k is (k,D,γ1,γ2) with DR2 compact Jordan of nonempty interior and γ1γ2 continuous on D, strict on its interior, describing E={p:πk(p)D, γ1(πk(p))pkγ2(πk(p))}; the cyclic projections are πx(p)=(py,pz), πy(p)=(pz,px) and πz(p)=(px,py) (Simple solid regions in a coordinate direction and their cyclic coordinate projection).

[F5]

Given a compatible finite patch presentation whose images cover and lie in the boundary, it is adapted to a description in the direction k when its index set splits into an upper, a lower and a lateral sublist, with the image of an upper patch in the graph of γ2 and the kth coordinate of its oriented area vector positive on the parameter interior, the mirror conditions for a lower patch, that coordinate vanishing on the parameter interior for a lateral patch, the projected images of each graph sublist pairwise disjoint and filling D up to content zero, and both graph sublists nonempty (Boundary presentations adapted to a simple solid region in a coordinate direction).

[F6]

An elementary solid region is a compact set with a simple description in each of the three coordinate directions and one compatible finite patch presentation of its boundary adapted to a simple description in each of them (Elementary solid regions: one boundary presentation adapted in all three coordinate directions).

[F7]

The oriented area vector of a patch is φu×φv and the flux integrand is taken against it (Unit normal fields, orientations, and flux through a regular surface patch); integration over a bounded Jordan set is that of The Riemann integral of a bounded function over a bounded Jordan measurable set; boundaries and interiors are those of Interior, closure, boundary, limit point, isolated point and dense subset of a metric space.

[F8]

A set has content zero when it admits finite cube covers of arbitrarily small total volume, and content zero passes to subsets (Measure zero and content zero in Rm by countable and finite cube covers); a bounded set is Jordan measurable exactly when its boundary has content zero (A bounded set in Rm is Jordan measurable iff its boundary is null, equivalently of content zero).

[L1]

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

Verification

technique · constructive
1.1

Each of the six maps is affine, so its two parameter derivatives are the constant standard basis vectors φz+,u=ex, φz+,v=ey; φz,u=ey, φz,v=ex; φx+,u=ey, φx+,v=ez; φx,u=ez, φx,v=ey; φy+,u=ez, φy+,v=ex; φy,u=ex, φy,v=ez. Computing each cross product from [F1] gives ex×ey=(0,0,1)=ez, ey×ex=ez, ey×ez=(1,0,0)=ex, ez×ey=ex, ez×ex=(0,1,0)=ey and ex×ez=ey, so the six oriented area vectors are the constants ez,ez,ex,ex,ey,ey as displayed.

givenF1F7construct
1.2

The three quadruples (z,[0,1]2,0,1), (x,[0,1]2,0,1) and (y,[0,1]2,0,1), with constant graph functions, are simple descriptions of B in the three directions in the sense of [F4]: the base [0,1]2 is compact, Jordan measurable and has nonempty interior; the constants 0<1 satisfy the weak and the strict inequality; and in each case {p:πk(p)[0,1]2, 0pk1} is exactly [0,1]3, because πk lists the two coordinates other than the kth.

givenF4F8construct
2.1

Each of the six pairs (S,φ) is a regular patch in the sense of [F2]: the square S is compact and Jordan measurable, being a rectangle, and is the closure of its nonempty convex, hence connected, interior (0,1)2; each φ is affine and therefore C1 on all of R2; each oriented area vector is a nonzero constant by step 1.1; and each φ is injective on R2, since its two direction vectors are distinct standard basis vectors and reading the two matching coordinates of the image recovers (u,v), so in particular no interior parameter point shares its image with a distinct point of S.

step 1.1F2F8
2.2

Take Σz+=(φz+), Σz=(φz) and Σz0=(φx+,φx,φy+,φy). The image of φz+ is the face pz=1, the graph of γ2=1, and by step 1.1 the z coordinate of its oriented area vector is 1>0; the image of φz is the graph of γ1=0 with z coordinate 1<0; and the four lateral vectors ±ex,±ey have z coordinate 0, so that coordinate vanishes on the whole parameter square. The projected image πz[φz+[(0,1)2]] is (0,1)2, whose complement in [0,1]2 is ([0,1]2) of content zero by [F8], and likewise for φz, where πz(v,u,0)=(v,u); each graph sublist is a single patch, so pairwise disjointness is vacuous, and both are nonempty. So the presentation is adapted to the z description of step 1.2, in the sense of [F5].

step 1.1step 1.2F5F8L1
2.3

Take Σx+=(φx+), Σx=(φx) and Σx0=(φz+,φz,φy+,φy). By step 1.1 the x coordinates of the oriented area vectors are 1 for φx+, 1 for φx and 0 for the other four. The image of φx+ is the face px=1 and πx(1,u,v)=(u,v), so its projected image is (0,1)2; the image of φx is px=0 and πx(0,v,u)=(v,u), again with projected image (0,1)2. Both complements in the base are ([0,1]2), of content zero. So the same presentation is adapted to the x description.

step 1.1step 1.2F5F8L1
2.4

Take Σy+=(φy+), Σy=(φy) and Σy0=(φz+,φz,φx+,φx). By step 1.1 the y coordinates of the oriented area vectors are 1 for φy+, 1 for φy and 0 for the other four. The image of φy+ is the face py=1 and πy(v,1,u)=(u,v), so its projected image is (0,1)2; the image of φy is py=0 and πy(u,0,v)=(v,u), with projected image (0,1)2. So the same presentation is adapted to the y description.

step 1.1step 1.2F5F8L1
3.1

The six images are the six closed faces of B, each contained in B, and their union is B by [F7], since a point of B fails to be interior exactly when one of its coordinates is 0 or 1. Two distinct faces meet in a closed edge, a vertex or the empty set; the preimage of such an intersection in either parameter square is contained in S, which has content zero by [F8], so the overlap condition of [F3] holds. Interior parameter points map into the six open faces, which are pairwise disjoint, so no point of an overlap is the image of an interior parameter point of two distinct patches and the normal-agreement condition of [F3] holds with nothing to check. Hence the six patches form a compatible finite patch presentation of B.

step 2.1F3F7F8
4.1

Steps 2.1 and 3.1 make the six patches a compatible finite patch presentation of B, step 1.2 supplies the three simple descriptions, and steps 2.2, 2.3 and 2.4 make that one presentation adapted in all three directions. By [F6] the box B, with these data, is an elementary solid region.

step 2.1step 3.1step 2.2step 2.3step 2.4F6discharge-construct: the six displayed patches

Remarks

  • The parameter order on each face is chosen, and the choice is what fixes the sign. Exchanging u and v on any one face reverses its oriented area vector and would make that face fail the adaptation condition in the direction where it is a graph face. The six orders above are the ones for which the oriented area vector is the outward standard basis vector, which is also what makes the presentation the outward one in the sense of Every patch of an elementary solid region's presentation is a graph face in some direction, and at interior base points its normal is outward.

  • Each face is lateral in two directions and a graph face in one. That is visible in step 1.1: the oriented area vector of each face is ± one standard basis vector, so exactly one of its three coordinates is nonzero. It is the concrete case of the general fact that no patch can be lateral in all three directions.

Depends on

Used by

Dependency tree · two levels

69 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