ExampleConstruction: Literature-sourcedVerification: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6-luna)

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.

A tensor NURBS patch exactly covers a quarter annulus

Statement

Assume Countable Choice. Fix $0 < r_{0} < 1$ . Use a linear radial coordinate $ρ (s) = r_{0} + (1 - r_{0}) s$ and a rational quadratic angular curve with control points $Q_{0} = (1, 0)$ , $Q_{1} = (1, 1)$ , $Q_{2} = (0, 1)$ and weights $(1, 1 / \sqrt{2}, 1)$ . Tensor their bases, use control points $P_{i j} = r_{i} Q_{j}$ for $r_{i} \in {r_{0}, 1}$ , and tensor weights $w_{i j} = w_{j}$ . The resulting patch maps $[0, 1]^{2}$ bijectively onto ${(x, y) : r_{0} \leq \sqrt{x^{2} + y^{2}} \leq 1, x, y \geq 0}$ with strictly positive Jacobian, and its exact map satisfies the norm-equivalence hypotheses of Bi-Lipschitz NURBS maps preserve H1 and energy norms.

Facts & Assumptions

Given: The radial degree-one basis, the rational quadratic angular basis and controls above, and the positive parameter $r_{0}$ .

[A1]

The Axiom of Countable Choice ( ${A C}_{ω}$ ) is used only for the pullback norm equivalence in [F3]; the explicit geometry calculations do not require choice.

[F1]

Tensor-product NURBS patch maps and rational spline spaces: tensor-product rational geometry uses the weighted denominator and positive-weight control points.

[F2]

Positive weights give a bounded partition-of-unity NURBS basis: positive weights and the tensor B-spline partition yield a positive denominator and a rational partition of unity.

[F3]

Bi-Lipschitz NURBS maps preserve H1 and energy norms under Countable Choice: a global bi-Lipschitz patch with positive bounded Jacobian and bounded derivative/inverse derivative has the stated H1 and energy norm equivalences.

Proof

1.1F1F2givenalgebra

Put $a = \sqrt{2}$ and $x_{0} (t) = (1 - t)^{2} + a t (1 - t), y_{0} (t) = t^{2} + a t (1 - t), D (t) = (1 - t)^{2} + a t (1 - t) + t^{2} .$ The weighted middle Bernstein coefficient is $2 (1 / \sqrt{2}) t (1 - t) = a t (1 - t)$ , so the angular map is $(X, Y) = (x_{0} / D, y_{0} / D)$ . Direct expansion gives $x_{0}^{2} + y_{0}^{2} - D^{2} = - 2 t^{2} (1 - t)^{2} + a^{2} t^{2} (1 - t)^{2} = 0,$ so $X^{2} + Y^{2} = 1$ ; also $X, Y \geq 0$ and $D > 0$ . The tensor-product weights and controls therefore give $F (s, t) = (ρ (s) X (t), ρ (s) Y (t))$ .

2.1step 1.1algebra

Expanding the numerator derivatives gives $x_{0} y_{0}^{'} - y_{0} x_{0}^{'} = a + 2 (1 - a) t (1 - t) = a D (t),$ because $D (t) = 1 + (a - 2) t (1 - t)$ and $a (a - 2) = 2 (1 - a)$ . Consequently $X Y^{'} - Y X^{'} = a / D (t) > 0$ . Since $X^{2} + Y^{2} = 1$ , the angular coordinate $θ (t) = \arctan (Y / X)$ has derivative $θ^{'} = X Y^{'} - Y X^{'} = a / D (t) > 0$ on the interior and extends monotonically from $0$ to $π / 2$ . Thus $t \mapsto (X, Y)$ traverses the first-quadrant unit-circle arc exactly once. Since $ρ$ increases bijectively from $r_{0}$ to $1$ , $F$ is injective and its image is exactly the stated quarter annulus.

3.1A1F1F3step 1.1step 2.1givenalgebra∎

The Jacobian is $\det D F (s, t) = ρ^{'} (s) ρ (s) (X Y^{'} - Y X^{'}) = (1 - r_{0}) ρ (s) \frac{\sqrt{2}}{D (t)} > 0.$ On the closed square, $ρ \geq r_{0} > 0$ and $D$ is continuous and positive, so this determinant has positive minimum and finite maximum; $D F$ is continuous and bounded, and the inverse matrix is bounded by its cofactor formula divided by the positive determinant. The physical inverse first recovers $ρ = \sqrt{x^{2} + y^{2}}$ and the angle $θ = atan2 (y, x)$ . This angle is Lipschitz on the annular sector because $ρ \geq r_{0}$ , and the inverse parameter $t (θ)$ is Lipschitz because $θ^{'} (t) = \sqrt{2} / D (t)$ has a positive minimum. Together with the linear inverse for $s$ , this makes $F^{- 1}$ Lipschitz; bounded $D F$ makes $F$ Lipschitz. The quarter annulus has a finite piecewise smooth Lipschitz boundary, so all admissibility hypotheses in [F1] hold. Applying [F3] gives the announced pullback norm equivalence.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

21 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

Stefan Takacs, Numerical Analysis of Isogeometric Methods, complete JKU lecture notes, 2018/19 (standard reference, not scraped)
Annalisa Buffa, Gregor Gantner, Carlotta Giannelli, Dirk Praetorius, Rafael Vázquez, Mathematical Foundations of Adaptive Isogeometric Analysis, Archives of Computational Methods in Engineering 29 (2022) (standard reference, not scraped)