Alphabeta Math
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.

Degree elevation and simple-knot insertion preserve the identity patch

Statement

Start with the degree-one identity map F(ξ,η)=(ξ,η) on [0,1]2, represented by its four tensor control points and unit weights. Elevate both coordinate degrees to two using control net Pij=(i/2,j/2) for i,j∈{0,1,2} and retain unit weights. Inserting a simple knot at 1/2 in both coordinate directions leaves the geometry exactly the identity and gives degree-two analysis splines with C1 continuity at the new interior knots.

Facts & Assumptions

Given: The initial identity patch, the degree-two tensor Bernstein basis, and midpoint-knot insertion in each coordinate.

[F1]

Conforming isogeometric Galerkin spaces and h/p/k refinement: h-refinement inserts knots at fixed degree; k-refinement combines degree elevation and knot insertion, and exact geometry is claimed only after verifying the homogeneous representation.

[F2]

B-spline basis properties and polynomial reproduction: degree-two splines with an interior knot of multiplicity one are C2−1=C1 there.

[F3]

Homogeneous knot insertion preserves an admissible NURBS patch: insertion of a new knot strictly inside a nonempty span, with homogeneous control updates, leaves the NURBS patch map unchanged and all weights positive.

Proof

1.1givenalgebra

The degree-two Bernstein functions are B02(t)=(1−t)2, B12(t)=2t(1−t), and B22(t)=t2. Thus ∑i=02Bi2(t)=1 and ∑i=02(i/2)Bi2(t)=t. For Pij=(i/2,j/2), unit weights make the tensor denominator one; summing the first and second control coordinates yields ξ and η. Hence the elevated representation is still exactly the identity map, with positive weights.

2.1F1F2F3step 1.1given∎

The midpoint 1/2 is new and lies strictly inside the single nonempty span of the clamped degree-two Bernstein knot vector. Apply [F3] to each fixed-coordinate control-net slice first in ξ, then in η. Each insertion preserves the entire homogeneous geometry and positive weights, so the final patch is exactly F(ξ,η)=(ξ,η). The resulting degree-two univariate knot vectors have a simple interior knot; [F2] gives C1 continuity in both coordinate directions. This is the stated k-refinement, and no general p/k geometry-preservation claim is needed.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

13 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