Pipeline-generated

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.

✓ 13 results · all verified · 6 also independently AI-judged

Every result on this page is machine-checked by a proof checker and read in full and owner-audited; the judge is an additional, independent cross-model AI review of the proofs. The 7 not AI-judged were verified by owner audit (typically over a confirmed judge false positive), not failures.

Curved geometry, mesh generation and conservative transfer

1 · Prerequisites

2 · Summary

This page defines admissible isoparametric maps and geometry-approximation errors, proves pullback and interpolation estimates, and bounds the Laplace tensor defect used in a local Strang estimate. It defines exact overlap-volume remapping as an orthogonal projection, proves conservation and positivity, and gives a conditional error bound that separates source approximation, target approximation, and geometry displacement.

For a reference facet chart $\hat{f} : \hat{F} \to \hat{K}$ , its physical facet is $F_{K} (\hat{f} (\hat{F})) \subset K$ , where $K = F_{K} (\hat{K})$ ; $ι_{K}$ denotes inclusion into $K$ . The square below commutes because both paths send $z \in \hat{F}$ to $F_{K} (\hat{f} (z))$ . It records the restriction of the cell map and the physical-facet inclusion; it is schematic, and the proofs use the explicit map, Jacobian, and matching hypotheses rather than the drawing.

\begin{tikzcd}[column sep=large,row sep=large]
\widehat F \arrow[r,"\widehat f"] \arrow[d,"F_K\circ\widehat f"'] &
\widehat K \arrow[d,"F_K"] \\
F_K(\widehat f(\widehat F)) \arrow[r,"\iota_K"'] & K
\end{tikzcd}

The mesh-generation result is deliberately restricted to a square mapped by an explicit area-preserving shear. It consumes the exact Delaunay and certified-predicate interfaces and a compatible two-dimensional NVB family. Its angle and termination results do not establish a general Delaunay quality theorem or adaptive complexity. Exact polygon clipping is limited to rational convex cells; unsupported or uncertified cases return unresolved.

The page uses adaptive-finite-element-methods and delaunay-triangulations-and-voronoi-computation as its declared current-plan prerequisites. It also cites the already published affine interpolation, measure, geometry-lift, and Strang items stated in the individual contracts.

3 · Logical flowchart

4 · Definitions, theorems and proofs

DefinitionDefinition: Literature-sourcedProof: Not applicableOpen item page →

Intersection-volume conservative remapping

Definition

Assume Countable Choice. Let $Ω \subset R^{d}$ be a bounded Lebesgue-measurable domain of finite positive measure. Let $S = (S_{i})_{i = 1}^{m}$ and $T = (T_{j})_{j = 1}^{n}$ be finite measurable partitions of $Ω$ up to null sets, with disjoint interiors modulo null sets and positive cell volumes. Define exact overlap weights $w_{j i} = ∣ T_{j} \cap S_{i} ∣$ . For source constants $v_{i}$ , the intersection-volume remap is the target piecewise-constant field $R v$ whose value on $T_{j}$ is $(R v)_{j} = ∣ T_{j} ∣^{- 1} \sum_{i} w_{j i} v_{i}$ . All weights are exact measures; an approximate clipping weight is not silently substituted.

Notes

The measurable sets and restricted set function are defined in Lebesgue measurable sets, the family $L (R^{n})$ , and the restricted set function $λ_{n}$ . Under Countable Choice (The Axiom of Countable Choice ( ${A C}_{ω}$ )), Assuming countable choice, $L (R^{n})$ is a sigma-algebra containing every elementary set and $λ_{n}$ is a complete measure extending elementary volume makes that family a sigma-algebra and the set function a measure. Thus every $T_{j} \cap S_{i}$ is measurable, and its measure is finite because it lies in $Ω$ ; every target denominator is finite and positive. Stable cell identifiers fix the finite summation order but do not affect the real-valued result. A target cell with zero volume is excluded because its average is undefined. The remap is a finite-volume $L^{2}$ projection once the conservation and orthogonality theorem below is proved.

DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (gpt-6-luna)Open item page →

Admissible isoparametric curved cells

Definition

Fix a reference matching affine simplicial mesh as in Matching affine simplicial meshes and shape regularity. An admissible curved cell is the image of a closed reference simplex $\hat{K}$ under a map $F_{K} \in C^{2} (\hat{K}; R^{d})$ that extends to a diffeomorphism on a neighborhood, is orientation preserving, and satisfies $0 < j_{0} \leq J_{K} : = \det D F_{K} \leq j_{1}$ and $∥ D F_{K} ∥ + ∥ (D F_{K})^{- 1} ∥ + ∥ D^{2} F_{K} ∥ \leq C_{F}$ . The physical cells have disjoint interiors, cover the domain up to their shared facets, and maps agree on each common reference facet under the prescribed affine facet identification. Define the volume metric $G_{K} = D F_{K}^{T} D F_{K}$ , volume factor $J_{K} = \sqrt{\det G_{K}}$ , and for a reference facet parametrization $\hat{f}$ the surface metric $G_{K, \hat{f}} = D (F_{K} \circ \hat{f})^{T} D (F_{K} \circ \hat{f})$ and surface factor $\sqrt{\det G_{K, \hat{f}}}$ . The positive-Jacobian lower bound is the admissibility certificate; it is not inferred from a drawing or from Delaunay quality.

Shape regularity and normals

Use the map and metric conventions in the Statement. A family is uniformly isoparametric shape regular if the reference affine family is shape regular and the displayed derivative, inverse-derivative, second-derivative, and positive-Jacobian bounds have constants independent of the cell. For an oriented reference facet normal $\hat{n}$ , the physical oriented normal is the normalization of $cof (D F_{K}) \hat{n} = J_{K} D F_{K}^{- T} \hat{n}$ . A map without a certified positive lower Jacobian is not an admissible cell map.

LemmaStatement: AI-adaptedProof: AI-adaptedprecheck passjudge pass (gpt-6-luna)Open item page →

The nodal P1 interpolant preserves homogeneous boundary values

Statement

Assume the Axiom of Choice and Countable Choice. Let $Ω = (- 1, 1)^{2}$ have a finite matching affine triangular mesh, and let $u \in H^{2} (Ω; R) \cap H_{0}^{1} (Ω; R)$ . On each triangle take the unique continuous representative of the restriction of $u$ . These representatives give one well-defined value at every mesh vertex. The global nodal P1 interpolant $I_{h} u$ , affine on each triangle and equal to these values at its vertices, is continuous, has zero trace on every boundary edge, and belongs to $H_{0}^{1} (Ω)$ .

Facts & Assumptions

Given: The Axiom of Choice and Countable Choice; the open square with its finite matching triangular mesh; and a real Sobolev class $u \in H^{2} (Ω) \cap H_{0}^{1} (Ω)$ .

[F1]

Affine pullback and pushforward preserve $W^{2, 2}$ , with weak derivatives given by the constant-matrix chain rule. (Affine pullback of weak derivatives and Sobolev seminorms)

[F2]

The reference triangle is a $W^{2, 2}$ extension domain; since $2 \cdot 2 > 2$ , higher-order Sobolev embedding gives a unique continuous representative on its closure. The same embedding applies on every ball whose closure is contained in $Ω$ , since a ball is a bounded smooth domain and therefore an extension domain. (A reference simplex is an integer-order Sobolev extension domain, Higher-order Sobolev embedding, Bounded C^k domains admit integer-order Sobolev extension)

[F3]

Zero extension sends $H_{0}^{1} (Ω)$ into $H^{1} (R^{2})$ and has the zero extended weak gradient. (Zero extension of W_0^{1,p} has no boundary derivative)

[F4]

The half-space trace is a bounded linear map on $H^{1}$ and agrees with classical restriction for compactly supported functions continuous on the closed half-space. Smooth compactly supported functions are dense in $H^{1} (R^{2})$ . (The half-space trace estimate and the half-space trace operator, Compactly supported smooth functions are dense in W^{k,p}(R^n))

[F5]

Translation and orthogonal coordinate changes preserve $H^{1} (R^{2})$ and its norm; weak derivatives transform by the corresponding constant matrix. This follows by changing variables in the weak-derivative identity and using the smooth chain rule. (A C^1 diffeomorphism satisfies the change-of-variables formula for nonnegative Lebesgue measurable functions, The chain rule for differentials of smooth maps)

[F6]

A nonempty open subset of $R^{2}$ contains a nondegenerate box, which has positive Lebesgue measure; hence continuous functions agreeing almost everywhere on an open set agree there everywhere. (A box in $R^{n}$ with parameters $a_{i} \leq b_{i}$ is Lebesgue measurable of measure $\prod_{i < n} (b_{i} - a_{i})$ , whichever of its faces are included)

[F7]

A smooth multiplier preserves $H^{1}$ and obeys the weak product rule. (Weak Leibniz rule with a smooth factor)

[F8]

On a finite matching mesh of a bounded polyhedral domain, a continuous piecewise polynomial with zero polynomial trace on every boundary facet belongs to $H_{0}^{1}$ . (Zero-boundary conforming polynomials lie in W0 1p and satisfy Poincare)

[F9]

Given concentric balls with the smaller closure inside the larger ball, there is a smooth cutoff supported in the larger ball and equal to one on the smaller ball. (A smooth bump between concentric Euclidean balls)

[F10]

A finite matching affine triangular mesh of the square consists of nondegenerate triangles with disjoint interiors, whose intersections are whole common edges or vertices; its boundary edges cover $\partial Ω$ . (Matching affine simplicial meshes and shape regularity)

[A1]

The Axiom of Choice is inherited through the simplex and higher-order Sobolev embedding and the half-space trace interfaces. (The Axiom of Choice)

[A2]

Countable Choice is inherited through affine changes of variables, zero extension, half-space trace and density, the weak multiplier rule, and the zero-boundary finite-element interface. (The Axiom of Countable Choice ( ${A C}_{ω}$ ))

Proof

1.1A1A2F1F2F6F10given

For each mesh triangle $K$ , apply [F1] to pull $u ∣_{K}$ back to the reference triangle, and then apply [F2]. This gives a continuous representative on $\overline{K}$ . It is unique: if two continuous representatives differed at one point, continuity would make them differ on a nonempty open subset of $K$ , contradicting [F6]. Thus each cellwise nodal value is individually well-defined.

1.2A1A2F3F4F5given

Put $z = E_{0} u$ , the zero extension from [F3]. On either side of any straight line, the half-space trace is obtained from the positive-half-space trace in [F4] by a translation and, when needed, a reflection; [F5] verifies that these changes preserve the Sobolev class and norm. The two traces of a global $H^{1} (R^{2})$ class across such a line agree: choose $z_{m} \in C_{c}^{\infty} (R^{2})$ converging to $z$ by [F4]; the two traces of each $z_{m}$ are its same classical restriction, and boundedness of the two trace maps passes this equality to the limit. On the exterior half-space of each side of $Ω$ , $z = 0$ , so both its exterior trace and its interior trace are zero.

2.1A1F2F6F10givenstep 1.1

If $K_{+}$ and $K_{-}$ share an interior edge, every point $x$ in the relative interior of that edge has a ball $B \subset Ω$ meeting only those two cells. By [F2], $u ∣_{B}$ has a continuous representative. On each of the two open half-balls $B \cap K_{\pm}$ , this representative and the corresponding representative from step 1.1 agree almost everywhere, hence everywhere by [F6]. Taking limits to $x$ shows the two cell values agree at $x$ ; continuity along the closed edge gives agreement at its endpoints as well. For an interior mesh vertex, take a ball about the vertex contained in $Ω$ and repeat this argument for every incident cell.

2.2A1A2F4F5F7F9F10step 1.1step 1.2

Let $x$ lie in the relative interior of a boundary mesh edge $E$ . Choose a ball $B$ centered at $x$ small enough that its interior half-ball lies in the unique incident triangle $K$ and its other boundary is disjoint from all mesh edges. By [F9] choose $χ \in C_{c}^{\infty} (B)$ equal to one near $x$ . On the interior half-space define $v = χ u_{K}$ inside $B$ and zero outside, where $u_{K}$ is the continuous cell representative from step 1.1. The cutoff vanishes near the circular part of $\partial B$ , so the weak test identity shows $v \in H^{1}$ of that half-space; it is compactly supported and continuous on the closed half-space. Its class is $χ z$ there. By linearity and boundedness of the trace, and by approximation with the smooth functions in step 1.2, $T (χ z) = χ T z = 0$ on the side. The classical-restriction clause of [F4] gives $T v = χ u_{K} ∣_{E}$ , so $u_{K} = 0$ almost everywhere near $x$ on $E$ . Continuity from step 1.1 makes this value zero at every point of that edge, including its endpoints.

3.1A2F8F10givenstep 2.1step 2.2∎

Interior edge values agree by step 2.1. At a boundary vertex, the incident triangles form a connected fan because the square is convex; the fan is a chain under adjacency across edges containing that vertex, and at least one end cell has a boundary edge. Step 2.2 gives zero at the vertex in that end cell, and step 2.1 propagates that value through the fan. Thus all cell values at every shared vertex agree and boundary vertex values are zero. The affine traces of adjacent P1 interpolants agree because they agree at both edge endpoints, so $I_{h} u$ is continuous; on each boundary edge it is affine with both endpoint values zero, hence its trace is zero. Apply [F8] to conclude $I_{h} u \in H_{0}^{1} (Ω)$ .

DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (gpt-6-luna)Open item page →

Curved-domain geometry approximation errors

Definition

Let $\hat{Ω} \subset R^{d}$ be a bounded reference domain and let $Φ, Φ_{h} : \overline{\hat{Ω}} \to R^{d}$ be cellwise $C^{2}$ admissible maps with matching traces, positive Jacobians, and common image topology. The exact and approximate domains are $Ω = Φ (\hat{Ω})$ and $Ω_{h} = Φ_{h} (\hat{Ω})$ . Define $e_{0} = ∥ Φ - Φ_{h} ∥_{L^{\infty} (\hat{Ω})}$ and $e_{1} = ∥ D Φ - D Φ_{h} ∥_{L^{\infty} (\hat{Ω}; o p)}$ . A geometry approximation claim must separately state bounds on $e_{0}, e_{1}$ , both Jacobian lower bounds, and boundary-trace compatibility; none follows from the word “isoparametric.”

Tensor convention

The transformed Laplace tensors associated with these maps are $B = J_{Φ} D Φ^{- 1} D Φ^{- T}$ and $B_{h} = J_{Φ_{h}} D Φ_{h}^{- 1} D Φ_{h}^{- T}$ wherever the maps are differentiable. Boundary lifting error and data error are separate quantities and are not included in $e_{0}$ or $e_{1}$ .

LemmaStatement: AI-adaptedProof: AI-adaptedprecheck passOpen item page →

P1 interpolation scaling on uniformly curved cells

Statement

Assume AC and Countable Choice. In dimension two let $K = Ψ (\tilde{K})$ , where $\tilde{K}$ is a shape-regular affine triangle of diameter comparable to $h_{K}$ , and $Ψ$ extends to a $C^{2}$ diffeomorphism on a neighborhood of $\overline{\tilde{K}}$ . Assume $∥ D Ψ ∥_{\infty} + ∥ D Ψ^{- 1} ∥_{\infty} + ∥ D^{2} Ψ ∥_{\infty} + ∥ J_{Ψ}^{- 1} ∥_{\infty}$ are uniformly bounded. Let $v$ denote its continuous representative and set $I_{K} v = (I_{\tilde{K}} (v \circ Ψ)) \circ Ψ^{- 1}$ , the mapped nodal P1 interpolant. For $v \in H^{2} (K)$ , $∥ v - I_{K} v ∥_{L^{2} (K)} \leq C h_{K}^{2} ∥ v ∥_{H^{2} (K)}$ and $∣ v - I_{K} v ∣_{H^{1} (K)} \leq C h_{K} ∥ v ∥_{H^{2} (K)}$ , with $C$ uniform over the family.

Facts & Assumptions

Given: AC and Countable Choice; a uniformly shape-regular affine triangle family; uniformly bi-Lipschitz $C^{2}$ cell maps with bounded second derivatives and Jacobian inverse; and $v \in H^{2} (K)$ .

[F1]

Local interpolation estimates on shape-regular affine meshes: under Countable Choice and, for automatic nodal boundedness, AC, on a shape-regular affine mesh, the nodal P1 interpolant of an $H^{2}$ function has $L^{2}$ error at most $C h_{K}^{2} ∣ v ∣_{H^{2}}$ and $H^{1}$ seminorm error at most $C h_{K} ∣ v ∣_{H^{2}}$ .

[F2]

Admissible isoparametric curved cells: admissible maps are diffeomorphisms with positive Jacobian and uniform derivative and inverse bounds.

[F3]

AC is used for continuous-representative nodal evaluation in [F5] and its automatic nodal-boundedness application in [F1]; Countable Choice is used through [F1] and [F4] (The Axiom of Choice, The Axiom of Countable Choice ( ${A C}_{ω}$ )).

[F4]

C^k boundary flattening preserves local W^{k,p}: under Countable Choice, composition with a $C^{2}$ diffeomorphism and its inverse having bounded derivatives through order two is bounded on local $W^{2, 2}$ spaces, with the weak derivatives given by the chain-rule polynomials.

[F5]

Sobolev threshold for Lagrange point evaluations on a reference simplex: under AC, in dimension $d = 2$ , point evaluation is bounded on $W^{2, 2}$ because $2 > d / p = 1$ , so the nodal values are defined for the continuous representative.

Proof

1.1F2F4F5givenalgebra

First apply [F4] to $w = v \circ Ψ$ on the interiors of the reference and curved cells. The maps extend to a $C^{2}$ diffeomorphism on neighborhoods of the compact cell closures, and the stated derivative, inverse-derivative, and Jacobian bounds give $w \in H^{2} (\tilde{K})$ with $∥ w ∥_{H^{2} (\tilde{K})} \leq C ∥ v ∥_{H^{2} (K)}$ . Now [F5] supplies the unique continuous representative $\tilde{v}$ of $w$ on $\overline{\tilde{K}}$ , so its three reference-vertex values are defined. The function $\tilde{v} \circ Ψ^{- 1}$ is continuous on $\overline{K}$ and represents $v$ , by the inverse-composition part of [F4]. If $g$ is any other continuous representative of $v$ on $\overline{K}$ , then $g \circ Ψ$ is a continuous representative of $w$ and equals $\tilde{v}$ by [F5]; hence the representative on $K$ is unique. Its values at the curved-cell vertices are exactly the pulled-back nodal values. Applying [F4] to the inverse map also gives the uniform $L^{2}$ and $H^{1}$ norm bounds needed when the interpolation error is pushed back to $K$ .

2.1F1F5step 1.1given

Apply [F1] to $w$ on the affine triangle $\tilde{K}$ . The mapped interpolant is exactly $(I_{\tilde{K}} w) \circ Ψ^{- 1}$ because its three nodal values are those of $v$ at the three image vertices. The affine estimates give $∥ w - I_{\tilde{K}} w ∥_{L^{2} (\tilde{K})} \leq C h_{K}^{2} ∥ w ∥_{H^{2} (\tilde{K})}$ and $∣ w - I_{\tilde{K}} w ∣_{H^{1} (\tilde{K})} \leq C h_{K} ∥ w ∥_{H^{2} (\tilde{K})}$ , using the assumed diameter comparability.

3.1F1F2F3F4F5step 1.1step 2.1∎

Push the error through $Ψ^{- 1}$ using step 1.1. The resulting uniform norm bounds are the two claimed estimates. AC is used in [F5] for the continuous representative and nodal evaluations, including the automatic nodal-boundedness application in [F1]; Countable Choice is used through [F1] and [F4].

LemmaStatement: AI-adaptedProof: AI-adaptedprecheck passjudge pass (gpt-6-luna)Open item page →

Pullback gradients and induced surface metrics

Statement

Assume Countable Choice. Let $F : \hat{K} \to K$ be an admissible $C^{1}$ orientation-preserving cell diffeomorphism and let $u$ be $C^{1}$ on $K$ . With $\hat{u} = u \circ F$ , one has $\nabla_{x} u \circ F = D F^{- T} \nabla_{ξ} \hat{u}$ and $\int_{K} ∣ \nabla u ∣^{2} d x = \int_{\hat{K}} J_{F} \nabla {\hat{u}}^{T} (D F^{- 1} D F^{- T}) \nabla \hat{u} d ξ$ . For a regular $k$ -dimensional parametrized face $f : U \subset R^{k} \to R^{d}$ with metric $G_{f} = D f^{T} D f$ , the induced area factor is $\sqrt{\det G_{f}}$ and the tangential gradient of $u \circ f$ is $D f G_{f}^{- 1} \nabla (u \circ f)$ ; its squared norm is $\nabla (u \circ f)^{T} G_{f}^{- 1} \nabla (u \circ f)$ .

Facts & Assumptions

Given: Countable Choice, an admissible orientation-preserving $C^{1}$ cell map, and a $C^{1}$ scalar field.

[F1]

Admissible isoparametric curved cells: $J_{F} = \det D F > 0$ , $G_{F} = D F^{T} D F$ , and the induced facet metric is the Gram matrix of the facet differential.

[F2]

The chain rule for total derivatives: $D (g \circ f) (a) = D g (f (a)) \circ D f (a)$ : $D (u \circ F) = D u (F) D F$ .

[F3]

A C^1 diffeomorphism satisfies the change-of-variables formula for nonnegative Lebesgue measurable functions: under Countable Choice a $C^{1}$ diffeomorphism changes variables with factor $∣ \det D F ∣$ .

[A1]

Countable Choice is assumed exactly for [F3] (The Axiom of Countable Choice ( ${A C}_{ω}$ )).

Proof

1.1F1F2givenalgebra

The chain rule [F2] gives $\nabla_{ξ} \hat{u} = D F^{T} (\nabla_{x} u \circ F)$ . Since $D F$ is invertible by admissibility, multiplication by $D F^{- T}$ yields $\nabla_{x} u \circ F = D F^{- T} \nabla_{ξ} \hat{u}$ .

1.2F1F2algebra

For a regular face parametrization, the differential maps a coordinate vector $z$ to $D f z$ and its squared Euclidean length is $z^{T} G_{f} z$ . The vector $G_{f}^{- 1} \nabla (u \circ f)$ is therefore the coordinate vector whose image under $D f$ has the defining inner products with every tangent vector; its image is the tangential gradient. Taking its squared norm gives $\nabla (u \circ f)^{T} G_{f}^{- 1} \nabla (u \circ f)$ . The Gram determinant gives the $k$ -volume scaling factor.

2.1F1F3A1givenstep 1.1∎

The energy identity follows by substituting step 1.1 into $∣ \nabla u ∣^{2}$ and applying [F3] to the nonnegative measurable energy density. Since $J_{F} > 0$ , the absolute determinant in [F3] equals $J_{F}$ .

TheoremStatement: AI-adaptedProof: AI-adaptedprecheck passOpen item page →

Overlap remapping is an L2 projection, conservative and positive

Statement

Assume Countable Choice. Under the finite partition hypotheses of Intersection-volume conservative remapping, let $P_{0} (T)$ be the target cellwise-constant subspace of $L^{2} (Ω)$ . For every source piecewise-constant $v$ , $R v$ is the $L^{2}$ orthogonal projection of $v$ onto $P_{0} (T)$ , hence $∥ R v ∥_{2} \leq ∥ v ∥_{2}$ . It preserves total mass, $\int_{Ω} R v = \int_{Ω} v$ , and if all $v_{i} \geq 0$ then every target value $(R v)_{j} \geq 0$ .

Facts & Assumptions

Given: Countable Choice; a finite-measure domain, finite source and target partitions up to null sets, positive target volumes, and source cell values $v_{i}$ .

[F1]

Intersection-volume conservative remapping: $w_{j i} = ∣ T_{j} \cap S_{i} ∣$ and $(R v)_{j} = ∣ T_{j} ∣^{- 1} \sum_{i} w_{j i} v_{i}$ .

[F2]

Holder's inequality for integrals, including the endpoint cases: Cauchy–Schwarz makes products of $L^{2}$ functions integrable and gives the $L^{2}$ inner-product inequality.

[F3]

The Lebesgue integral is linear on $L^{1} (μ)$ : the integral is linear on integrable functions.

[F4]

Assuming countable choice, $L (R^{n})$ is a sigma-algebra containing every elementary set and $λ_{n}$ is a complete measure extending elementary volume: under Countable Choice, Lebesgue measure is a countably additive measure.

[A1]

Countable Choice is assumed for [F4] (The Axiom of Countable Choice ( ${A C}_{ω}$ )).

Proof

1.1F1F4A1given

By [F4], Lebesgue measure is countably additive and hence finitely additive. The partition hypotheses therefore give $\sum_{i} w_{j i} = ∣ T_{j} ∣$ for every target cell and $\sum_{j} w_{j i} = ∣ S_{i} ∣$ for every source cell; omitted partition boundaries are null and do not change these measures. The same finite additivity gives $\int_{T_{j}} v = \sum_{i} w_{j i} v_{i}$ .

2.1F1F3F4A1step 1.1algebra

For any target cellwise-constant $z$ , sum over target cells: $\int_{Ω} (v - R v) z = \sum_{j} z_{j} (\sum_{i} w_{j i} v_{i} - ∣ T_{j} ∣ (R v)_{j}) = 0$ by [F1] and step 1.1. Thus $v - R v$ is orthogonal to the target subspace.

3.1F2step 2.1algebra

Orthogonality with $z = R v$ gives $∥ v ∥_{2}^{2} = ∥ R v ∥_{2}^{2} + ∥ v - R v ∥_{2}^{2}$ , so $∥ R v ∥_{2} \leq ∥ v ∥_{2}$ . All terms are finite because the partitions are finite, cells have finite volume, and $v$ is piecewise constant.

4.1F1F3F4A1step 1.1algebra∎

By the column-sum identity in step 1.1, $\int R v = \sum_{j} ∣ T_{j} ∣ (R v)_{j} = \sum_{i} ∣ S_{i} ∣ v_{i} = \int v$ . If each $v_{i} \geq 0$ , every overlap weight is nonnegative, so the defining finite weighted average is nonnegative.

LemmaStatement: AI-adaptedProof: AI-adaptedprecheck passOpen item page →

Geometry error bounds a pulled-back boundary-lift residual

Statement

Assume Countable Choice. Let $\hat{Ω} = (- 1, 1)^{2}$ carry a finite matching affine triangular mesh $T$ as in Matching affine simplicial meshes and shape regularity. Let $Φ, Φ_{h} : \overline{\hat{Ω}} \to R^{2}$ be continuous and $C^{1}$ on each closed triangle, with matching traces on shared edges, and suppose $∥ D Φ ∥_{\infty} + ∥ D Φ_{h} ∥_{\infty} \leq M$ , $e_{0} = ∥ Φ - Φ_{h} ∥_{\infty}$ , and $e_{1} = ∥ D Φ - D Φ_{h} ∥_{L^{\infty}; o p}$ . Let $G$ be a scalar physical boundary lift on an open convex neighborhood containing both images and every segment joining corresponding image points, with $∥ D G ∥_{\infty} \leq L_{1}$ and $∥ D^{2} G ∥_{\infty} \leq L_{2}$ . Define the piecewise pullback gradients by $\nabla_{p w} (G \circ Φ) = D Φ^{T} \nabla G (Φ)$ and $\nabla_{p w} (G \circ Φ_{h}) = D Φ_{h}^{T} \nabla G (Φ_{h})$ , and set $ℓ_{\partial, h} (w) = \int_{\hat{Ω}} (\nabla_{p w} (G \circ Φ) - \nabla_{p w} (G \circ Φ_{h})) \cdot \nabla w, w \in H_{0}^{1} (\hat{Ω}) .$ With the $H^{1}$ dual norm, $∥ ℓ_{\partial, h} ∥_{(H_{0}^{1})^{*}} \leq 2 (L_{1} e_{1} + M L_{2} e_{0})$ . Thus the geometry-induced boundary-lift contribution to the Strang load defect is $O (e_{0} + e_{1})$ .

Facts & Assumptions

Given: Countable Choice; the reference square; continuous, cellwise $C^{1}$ maps with the stated derivative gap and upper bound; a $C^{2}$ lift $G$ on a convex neighborhood of both images; and $w \in H_{0}^{1} (\hat{Ω})$ .

[F1]

Curved-domain geometry approximation errors: $e_{0}$ and $e_{1}$ are the uniform value and derivative gaps between exact and approximate geometry maps.

[F2]

The chain rule for total derivatives: $D (g \circ f) (a) = D g (f (a)) \circ D f (a)$ : $D (G \circ Φ) = D Φ^{T} (D G \circ Φ)$ wherever the cell maps are differentiable.

[F3]

Holder's inequality for integrals, including the endpoint cases: $∣ \int f \cdot g ∣ \leq ∥ f ∥_{L^{2}} ∥ g ∥_{L^{2}}$ .

[F4]

Under Countable Choice, the Lebesgue measurable sets form a sigma-algebra containing every elementary set, and Lebesgue measure agrees there with elementary volume. For the half-open box $B = (- 1, 1]^{2}$ , its elementary volume is $4$ . (Assuming countable choice, $L (R^{n})$ is a sigma-algebra containing every elementary set and $λ_{n}$ is a complete measure extending elementary volume, The sum of the volumes of a disjoint box decomposition of an elementary set does not depend on the decomposition, Half-open boxes in $R^{n}$ and their volume, Elementary sets: the finite unions of half-open boxes in $R^{n}$ )

[F5]

A measure is nonnegative and finitely additive on disjoint measurable sets; consequently it is monotone on measurable sets, since $E \subseteq B$ gives $B = E \cup (B ∖ E)$ . (Measures on sigma-algebras)

[F6]

Under Countable Choice, on each affine triangle, the Gauss--Green formula applies to a $C^{1}$ vector field on its closure, and the induced orientations on the two copies of a shared edge are opposite in a matching mesh. (Gauss–Green formula on an affine simplex, Interior facet orientations cancel in a matching mesh)

[A1]

Countable Choice is used through [F4] and the Gauss--Green supplier in [F6] (The Axiom of Countable Choice ( ${A C}_{ω}$ )).

Proof

1.1F1F2F6givenalgebra

Because each geometry map and its traces are continuous across every interior edge, $G \circ Φ$ and $G \circ Φ_{h}$ have matching traces there. Apply [F6] on each triangle to the product of the pulled-back lift with a compactly supported smooth test function; the interior-edge fluxes cancel, and the outer boundary term vanishes. Thus the displayed piecewise gradients are the weak gradients of the pulled-back lifts. On each triangle, [F2] and the triangle inequality give $∣ \nabla_{p w} (G \circ Φ) - \nabla_{p w} (G \circ Φ_{h}) ∣ \leq L_{1} e_{1} + M L_{2} e_{0},$ using the bound on $D^{2} G$ along the joining segment.

2.1F4F5A1step 1.1givenalgebra

For $n \geq 2$ put $B_{n} = (- 1 + 1 / n, 1 - 1 / n]^{2}$ . Each $B_{n}$ is an elementary half-open box in the convention $(a, b]$ , and $(- 1, 1)^{2} = ⋃_{n \geq 2} B_{n}$ : one inclusion is immediate, and for any $x \in (- 1, 1)^{2}$ choose $n$ with $1 / n < \min_{i} {1 + x_{i}, 1 - x_{i}}$ for both coordinates. Thus [F4] makes $\hat{Ω}$ measurable. Since $\hat{Ω} \subset B = (- 1, 1]^{2}$ , [F5] and [F4] give $∣ \hat{Ω} ∣ \leq λ_{2} (B) = 4$ . Step 1.1 therefore yields $∥ \nabla_{p w} (G \circ Φ) - \nabla_{p w} (G \circ Φ_{h}) ∥_{L^{2} (\hat{Ω})} \leq 2 (L_{1} e_{1} + M L_{2} e_{0}) .$

3.1F1F3step 2.1algebra∎

Apply [F3] to the defining integral for $ℓ_{\partial, h} (w)$ and use $∥ \nabla w ∥_{L^{2}} \leq ∥ w ∥_{H^{1}}$ . Taking the supremum over unit $H_{0}^{1}$ tests proves the dual bound.

LemmaStatement: AI-adaptedProof: AI-adaptedprecheck passOpen item page →

Cofactor, surface-Jacobian, and normal perturbation bounds

Statement

Let $A = D Φ$ and $A_{h} = D Φ_{h}$ be orientation-preserving cell-map derivatives with $\det A, \det A_{h} \geq j_{*} > 0$ , $∥ A ∥_{o p}, ∥ A_{h} ∥_{o p} \leq M$ , and $∥ A - A_{h} ∥_{o p} \leq e_{1}$ . For every unit reference-facet normal $\hat{n}$ , define the surface Jacobians $J_{Γ} (A) = ∥ cof (A) \hat{n} ∥$ , $J_{Γ} (A_{h}) = ∥ cof (A_{h}) \hat{n} ∥$ , and mapped unit normals $n_{Γ} (A) = cof (A) \hat{n} / J_{Γ} (A)$ and $n_{Γ} (A_{h}) = cof (A_{h}) \hat{n} / J_{Γ} (A_{h})$ . Then $∥ cof (A) - cof (A_{h}) ∥_{o p} + ∣ J_{Γ} (A) - J_{Γ} (A_{h}) ∣ + ∣ n_{Γ} (A) - n_{Γ} (A_{h}) ∣ \leq C (d, M, j_{*}) e_{1} .$ For any regular reference-facet parametrization $\hat{f}$ , the chart Gram-metric factor of Admissible isoparametric curved cells is $\sqrt{\det (D {\hat{f}}^{T} A^{T} A D \hat{f})} = J_{Γ} (A) \sqrt{\det (D {\hat{f}}^{T} D \hat{f})}$ , pointwise with $A = D Φ (\hat{f})$ . Thus $J_{Γ} (A)$ is the surface-area factor relative to reference-facet area; it equals the chart factor when the reference chart has unit area factor. The same relation holds for $A_{h}$ .

Facts & Assumptions

Given: Orientation-preserving invertible matrices $A, A_{h} \in R^{d \times d}$ with determinant lower bound $j_{*}$ , operator norm upper bound $M$ , derivative gap $e_{1}$ , and a unit reference normal $\hat{n}$ .

[F1]

Admissible isoparametric curved cells: for a reference facet chart $\hat{f}$ , the physical surface factor is the square root of the Gram determinant of $D (Φ \circ \hat{f})$ .

[F2]

Curved-domain geometry approximation errors: $e_{1} = ∥ D Φ - D Φ_{h} ∥_{L^{\infty}; o p}$ .

Proof

1.1F1F2givenalgebra

Each entry of $cof (A)$ is a signed $(d - 1)$ -minor, hence a polynomial of degree $d - 1$ in the entries of $A$ . On the bounded matrix ball $∥ A ∥_{o p}, ∥ A_{h} ∥_{o p} \leq M$ , its derivative is bounded by a constant depending only on $d, M$ . The mean-value inequality therefore gives $∥ cof (A) - cof (A_{h}) ∥_{o p} \leq C (d, M) ∥ A - A_{h} ∥_{o p} = C (d, M) e_{1}$ .

1.2F1givenalgebra

Let $T$ have orthonormal columns spanning the reference facet tangent space, so $Q = [T, \hat{n}]$ is orthogonal. The squared Gram-metric surface factor is $\det (T^{T} A^{T} A T)$ . The identity $cof (A)^{T} cof (A) = cof (A^{T} A)$ and orthogonal covariance of cofactors show ${\hat{n}}^{T} cof (A^{T} A) \hat{n}$ is the bottom-right cofactor of $Q^{T} A^{T} A Q$ , which is exactly $\det (T^{T} A^{T} A T)$ . Therefore $∥ cof (A) \hat{n} ∥^{2} = \det (T^{T} A^{T} A T)$ . For a regular chart write $D \hat{f} = T R$ , where $R$ is an invertible $(d - 1) \times (d - 1)$ matrix. Then $\det (D {\hat{f}}^{T} A^{T} A D \hat{f}) = \det (R)^{2} \det (T^{T} A^{T} A T)$ and $\det (D {\hat{f}}^{T} D \hat{f}) = \det (R)^{2}$ . Taking positive square roots gives the stated chart-factor relation, also for $A_{h}$ .

2.1F1givenstep 1.1algebra

If $σ_{1} (A) \geq \dots \geq σ_{d} (A) > 0$ are the singular values, the smallest singular value of $cof (A)$ is $\prod_{i = 2}^{d} σ_{i} (A) = \det (A) / σ_{1} (A) \geq j_{*} / M$ . Thus $J_{Γ} (A) \geq j_{*} / M$ , and the same bound holds for $A_{h}$ . The reverse triangle inequality and step 1.1 give $∣ J_{Γ} (A) - J_{Γ} (A_{h}) ∣ \leq C (d, M) e_{1}$ .

3.1step 1.1step 2.1algebra∎

Put $a = cof (A) \hat{n}$ and $b = cof (A_{h}) \hat{n}$ . For nonzero vectors, $∣ a / ∣ a ∣ - b / ∣ b ∣ ∣ \leq 2 ∣ a - b ∣ / \min (∣ a ∣, ∣ b ∣)$ . The lower bounds from step 2.1 and the cofactor gap from step 1.1 therefore imply $∣ n_{Γ} (A) - n_{Γ} (A_{h}) ∣ \leq C (d, M, j_{*}) e_{1}$ . Combining the three estimates proves the result.

LemmaStatement: AI-adaptedProof: AI-adaptedprecheck passjudge pass (gpt-6-luna)Open item page →

Derivative geometry error controls the Laplace tensor defect

Statement

Let $Φ, Φ_{h}$ be the orientation-preserving maps of Curved-domain geometry approximation errors, with $J, J_{h} \geq j_{*} > 0$ and $∥ D Φ ∥_{\infty} + ∥ D Φ_{h} ∥_{\infty} \leq M$ . Set $B = J D Φ^{- 1} D Φ^{- T}$ and $B_{h} = J_{h} D Φ_{h}^{- 1} D Φ_{h}^{- T}$ . Then $∥ B - B_{h} ∥_{\infty} \leq C e_{1}$ , where $C$ depends only on $d, j_{*}, M$ . Consequently $∣ \int_{\hat{Ω}} \nabla v^{T} (B - B_{h}) \nabla w ∣ \leq C e_{1} ∥ \nabla v ∥_{2} ∥ \nabla w ∥_{2}$ for $v, w \in H^{1} (\hat{Ω})$ .

Facts & Assumptions

Given: Two orientation-preserving $C^{1}$ diffeomorphisms with the stated determinant lower bounds and uniform derivative upper bounds.

[F1]

Curved-domain geometry approximation errors: $e_{1} = ∥ D Φ - D Φ_{h} ∥_{\infty}$ and $J, J_{h}$ are the positive determinants.

[F2]

Pullback gradients and induced surface metrics: the pulled-back Laplace tensor is $J D Φ^{- 1} D Φ^{- T}$ .

[F3]

Holder's inequality for integrals, including the endpoint cases: integral Cauchy–Schwarz bounds the product of the two gradient magnitudes.

Proof

1.1F1givenalgebra

On the bounded matrix set $∥ A ∥, ∥ C ∥ \leq M$ , the determinant is a polynomial in the entries, so its derivative is bounded on that set and $∣ \det A - \det C ∣ \leq C_{d} M^{d - 1} ∥ A - C ∥$ . Apply this with $A = D Φ$ and $C = D Φ_{h}$ to obtain $∣ J - J_{h} ∣ \leq C e_{1}$ .

2.1F1F2step 1.1algebra

The inverse identity $A^{- 1} - C^{- 1} = A^{- 1} (C - A) C^{- 1}$ and $J, J_{h} \geq j_{*}$ show $∥ D Φ^{- 1} - D Φ_{h}^{- 1} ∥ \leq C (d, M, j_{*}) e_{1}$ ; indeed every singular value is at most $M$ and their product is at least $j_{*}$ , so the smallest is at least $j_{*} / M^{d - 1}$ and each inverse norm is at most $M^{d - 1} / j_{*}$ . Expanding $J A^{- 1} A^{- T} - J_{h} C^{- 1} C^{- T}$ into the determinant difference and the two inverse-factor differences gives $∥ B - B_{h} ∥_{\infty} \leq C e_{1}$ .

3.1F3step 2.1given∎

Pointwise, $∣ \nabla v^{T} (B - B_{h}) \nabla w ∣ \leq C e_{1} ∣ \nabla v ∣ ∣ \nabla w ∣$ . Integrating and applying [F3] proves the stated bilinear-form defect bound; the right side is finite because both gradients are in $L^{2}$ .

LemmaStatement: AI-adaptedProof: AI-adaptedprecheck passjudge pass (gpt-6-luna)Open item page →

P1 approximation of a parabolic shear map

Statement

Assume Countable Choice. Let $\hat{Ω} = [- 1, 1]^{2}$ , let $T_{h}$ be a matching shape-regular affine triangulation, and put $Φ (x, y) = (x, y + x^{2} / 4)$ . Let $I_{h}$ be the vertexwise P1 interpolant and $Φ_{h} (x, y) = (x, y + I_{h} (x^{2} / 4))$ . In the notation of Curved-domain geometry approximation errors, there is a constant $C$ depending only on the shape-regularity bound such that $e_{0} \leq C h^{2}$ and $e_{1} \leq C h$ . For sufficiently small $h$ , $\det D Φ_{h} \geq 1 / 2$ , and $Φ_{h}$ is globally one-to-one on the square. The exact map has $\det D Φ = 1$ and a global inverse $(X, Y) \mapsto (X, Y - X^{2} / 4)$ .

Facts & Assumptions

Given: Countable Choice; the square and a matching shape-regular affine triangulation with maximal diameter $h$ .

[F1]

Matching affine simplicial meshes and shape regularity: triangle interiors are disjoint and shared boundaries are complete matching facets.

[F2]

Shape regularity controls affine simplex geometry: barycentric gradients on a shape-regular triangle satisfy $∣ \nabla λ_{i} ∣ \leq C h_{K}^{- 1}$ .

[F3]

Curved-domain geometry approximation errors: $e_{0}$ and $e_{1}$ are the uniform value and derivative differences of exact and approximate geometry maps.

[A1]

Countable Choice is the explicit hypothesis of [F2] (The Axiom of Countable Choice ( ${A C}_{ω}$ )).

Proof

1.1givenalgebra

Direct differentiation gives $D Φ = (\begin{array}{cc} 1 & 0 \\ x / 2 & 1 \end{array})$ and determinant $1$ ; the stated inverse is verified by substitution. On a triangle with barycentric coordinates $λ_{i}$ and vertex first-coordinates $x_{i}$ , exact quadratic expansion gives $I_{h} (x^{2} / 4) - x^{2} / 4 = \frac{1}{4} \sum_{i < j} λ_{i} λ_{j} (x_{i} - x_{j})^{2}$ . Since $∣ x_{i} - x_{j} ∣ \leq h_{K}$ and $0 \leq λ_{i} \leq 1$ , this is bounded by $C h_{K}^{2}$ .

2.1F2F3A1step 1.1algebra

Differentiating the barycentric expression in step 1.1, only the factors $λ_{i} λ_{j}$ vary; their derivatives are bounded by $C h_{K}^{- 1}$ using [F2], while $∣ x_{i} - x_{j} ∣^{2} \leq h_{K}^{2}$ . The product rule therefore gives a derivative bound $C h_{K}$ . Thus $∥ D (I_{h} (x^{2} / 4) - x^{2} / 4) ∥_{L^{\infty} (K)} \leq C h_{K}$ , yielding the global $C h$ derivative estimate and the $C h^{2}$ value estimate. By [F3] these are the geometry errors $e_{1}$ and $e_{0}$ .

3.1F1step 2.1algebra∎

The first coordinate of $Φ_{h}$ is $x$ , and on each vertical segment its second coordinate is the continuous piecewise-affine function $y + I_{h} (x^{2} / 4) (x, y)$ . Its slope on every subsegment is $1 + \partial_{y} I_{h} (x^{2} / 4) \geq 1 - C h$ . Choose $h$ with $C h \leq 1 / 2$ . Integration over the finitely many subsegments makes this coordinate strictly increasing with increment at least half the vertical increment. Equal images must therefore have equal first coordinates and then equal second-coordinate inputs; hence $Φ_{h}$ is injective. The same derivative estimate gives $\det D Φ_{h} = 1 + \partial_{y} I_{h} (x^{2} / 4) \geq 1 / 2$ .

TheoremStatement: AI-adaptedProof: AI-adaptedprecheck passOpen item page →

Remap error separates source, target and geometry approximation

Statement

Assume Countable Choice. Let $\hat{Ω}$ be bounded, let $Φ, Φ_{h}$ be the geometry maps of Curved-domain geometry approximation errors and assume each is a global orientation-preserving $C^{1}$ diffeomorphism from $\hat{Ω}$ onto its image, with $J_{h} \leq J^{*}$ and $u$ is $L_{u}$ -Lipschitz on the union of their images. On $Ω_{h} = Φ_{h} (\hat{Ω})$ let $S = (S_{i})_{i = 1}^{m}$ and $T = (T_{j})_{j = 1}^{n}$ be finite families of Lebesgue-measurable sets of positive measure satisfying $∣ Ω_{h} ∖ ⋃_{i} S_{i} ∣ = ∣ Ω_{h} ∖ ⋃_{j} T_{j} ∣ = 0, ∣ S_{i} \cap S_{i^{'}} ∣ = 0 (i \neq i^{'}), ∣ T_{j} \cap T_{j^{'}} ∣ = 0 (j \neq j^{'}) .$ Thus each family is a finite measurable partition up to null sets as required by Intersection-volume conservative remapping. Let $v_{S}$ be source-piecewise-constant data with finite $L^{2}$ error. Assume the exact target projection error below is finite. Define $P_{T} q$ on each target cell by its exact cell average, $η_{S} = ∥ u - v_{S} ∥_{L^{2} (Ω_{h})}$ , and $η_{T} = ∥ u - P_{T} u ∥_{L^{2} (Ω_{h})}$ . If $R$ is the exact overlap remap, then $∥ u \circ Φ - (R v_{S}) \circ Φ_{h} ∥_{L^{2} (\hat{Ω}, J_{h})} \leq L_{u} e_{0} \sqrt{J^{*} ∣ \hat{Ω} ∣} + η_{S} + η_{T},$ where $e_{0} = ∥ Φ - Φ_{h} ∥_{\infty}$ and $∥ z ∥_{L^{2} (\hat{Ω}, J_{h})}^{2} = \int_{\hat{Ω}} ∣ z ∣^{2} J_{h}$ .

Facts & Assumptions

Given: Countable Choice; the exact and approximate maps; a bounded approximate Jacobian; a Lipschitz field on both images; two finite measurable families satisfying the displayed coverage and pairwise-null-overlap conditions; and source values constant on source cells.

[F1]

Curved-domain geometry approximation errors: $e_{0} = ∥ Φ - Φ_{h} ∥_{\infty}$ and $J_{h}$ is the positive approximate Jacobian.

[F2]

Intersection-volume conservative remapping and Overlap remapping is an L2 projection, conservative and positive: exact overlap remapping of source constants is the target-cell average projection.

[F3]

Holder's inequality for integrals, including the endpoint cases: $∣ \int_{T} q ∣^{2} \leq ∣ T ∣ \int_{T} ∣ q ∣^{2}$ on every finite-volume target cell.

[F4]

A C^1 diffeomorphism satisfies the change-of-variables formula for nonnegative Lebesgue measurable functions: under Countable Choice, a $C^{1}$ diffeomorphism transforms nonnegative integrals by its positive Jacobian.

[A1]

Countable Choice is assumed for the measure/projection interfaces in [F2] and change of variables in [F4] (The Axiom of Countable Choice ( ${A C}_{ω}$ )).

Proof

1.1F1given

The Lipschitz condition gives $∣ u (Φ (X)) - u (Φ_{h} (X)) ∣ \leq L_{u} e_{0}$ for every $X$ . Integrating its square against $J_{h} \leq J^{*}$ gives the geometry term $L_{u} e_{0} \sqrt{J^{*} ∣ \hat{Ω} ∣}$ .

1.2F3givenalgebra

For any $q \in L^{2} (Ω_{h})$ and target cell $T$ , [F3] gives $∣ T ∣ ∣ P_{T} q ∣_{T}^{2} = ∣ \int_{T} q ∣^{2} / ∣ T ∣ \leq \int_{T} ∣ q ∣^{2}$ . Summing over the disjoint target cells shows $P_{T}$ is contractive. The same averaging identity gives $q - P_{T} q$ orthogonal to every target-cellwise constant, so $P_{T}$ is the orthogonal projection.

2.1F2step 1.2algebra

By [F2], $R v_{S} = P_{T} v_{S}$ . Thus $u - R v_{S} = (u - P_{T} u) + P_{T} (u - v_{S})$ ; the two terms are orthogonal and $P_{T}$ is contractive by step 1.2. The first term has norm $η_{T}$ and the second is at most $η_{S}$ , whence $∥ u - R v_{S} ∥_{L^{2} (Ω_{h})} \leq η_{T} + η_{S}$ .

3.1F4A1step 1.1step 2.1∎

Apply [F4] separately on the finitely many mesh cells to identify the physical $L^{2} (Ω_{h})$ norm in step 2.1 with the weighted pullback norm of $(u - R v_{S}) \circ Φ_{h}$ . The triangle inequality with step 1.1 proves the claimed bound.

LemmaStatement: AI-adaptedProof: AI-adaptedprecheck passjudge pass (gpt-6-luna)Open item page →

Conforming NVB closure preserves curved shared traces

Statement

Let a compatible labeled reference triangulation be refined by recursive reference-edge closure as in Dorfler marking and conforming newest-vertex refinement. The closure terminates in a matching conforming affine descendant. If every cell is mapped through one common injective geometry map whose traces agree on common reference facets, the resulting curved cells also have matching interfaces.

Facts & Assumptions

Given: A compatible labeled 2D triangulation, a finite refinement request, recursive reference-edge closure, and a common injective geometry map with matching facet traces.

[F1]

Termination and cumulative complexity of NVB conformity closure: recursive reference-edge closure of any finite marked set terminates and produces a matching conforming NVB descendant.

[F2]

Admissible isoparametric curved cells: neighboring cell maps agree under the prescribed common-facet identification.

Proof

1.1F1given

Apply [F1] to the finite request. Its output is a conforming affine triangulation, so each interior edge is represented by the same complete reference segment from both incident cells; no hanging edge subdivision remains.

2.1F2givenstep 1.1∎

On a common edge, the assumed geometry map has one trace from the shared reference segment. By [F2] the two incident curved-cell parametrizations use that same trace, and injectivity prevents distinct reference interfaces from being identified as overlapping physical interiors. Thus the physical curved interface matches.

TheoremStatement: AI-adaptedProof: AI-adaptedprecheck passjudge pass (gpt-6-luna)Open item page →

Strang error bound for a parabolic isoparametric P1 family

Statement

Assume the Axiom of Choice and Countable Choice. Let $\hat{Ω} = (- 1, 1)^{2}$ , let $Φ (x, y) = (x, y + x^{2} / 4)$ , and let $Φ_{h}$ be its continuous piecewise-affine nodal interpolant on a shape-regular matching triangular mesh with maximum diameter $h \leq 1$ , small enough that $J_{h} = \det D Φ_{h} \geq 1 / 2$ as in P1 approximation of a parabolic shear map. Put $J = \det D Φ$ and define the pulled-back Laplace tensors $B = J D Φ^{- 1} D Φ^{- T}, B_{h} = J_{h} D Φ_{h}^{- 1} D Φ_{h}^{- T} .$ On $V = H_{0}^{1} (\hat{Ω})$ set $a (v, w) = \int_{\hat{Ω}} \nabla v^{T} B \nabla w, a_{h} (v, w) = \int_{\hat{Ω}} \nabla v^{T} B_{h} \nabla w .$ Let $V_{h}$ be the finite-dimensional space of continuous functions on $\overline{\hat{Ω}}$ that are affine on each triangle and vanish on $\partial \hat{Ω}$ , viewed as a subspace of $V$ . Suppose $a$ and $a_{h}$ are uniformly bounded and coercive on $V$ and $V_{h}$ , respectively, with constants independent of $h$ , $F \in V^{*}$ and $F_{h} \in V_{h}^{*}$ are bounded, $u \in H^{2} (\hat{Ω}) \cap V$ is real-valued and satisfies $a (u, w) = F (w)$ for every $w \in V$ , and $u_{h} \in V_{h}$ satisfies $a_{h} (u_{h}, w_{h}) = F_{h} (w_{h})$ for every $w_{h} \in V_{h}$ .

If a common physical boundary lift $G \in C^{2}$ with bounded first and second derivatives on a convex neighborhood of the two geometry images is used, let $ℓ_{\partial, h}$ be its pulled-back residual from Geometry error bounds a pulled-back boundary-lift residual and set $ϵ_{\partial, h} = ∥ ℓ_{\partial, h} ∥_{V^{*}}$ . Assume the load difference on $V_{h}$ splits as $(F - F_{h}) ∣_{V_{h}} = L_{b u l k, h} + ℓ_{\partial, h} ∣_{V_{h}}, ∥ L_{b u l k, h} ∥_{V_{h}^{*}} \leq ϵ_{F, h}^{b u l k}, ϵ_{F, h}^{b u l k} \geq 0.$ Here the $V^{*}$ and $V_{h}^{*}$ norms are induced by the $H^{1}$ norm. If no lift is used, set $ℓ_{\partial, h} = 0$ and take the same bound for the full load difference. Then $∥ u - u_{h} ∥_{H^{1} (\hat{Ω})} \leq C (h ∥ u ∥_{H^{2} (\hat{Ω})} + ϵ_{F, h}^{b u l k} + ϵ_{\partial, h}) .$ where $C$ is independent of $h$ . For the parabolic geometry family, $ϵ_{\partial, h} \leq C_{G} (e_{0} + e_{1}) \leq C_{G} h$ .

Facts & Assumptions

Given: The Axiom of Choice and Countable Choice; the parabolic exact and approximate geometry maps on the reference square; a shape-regular matching mesh with $h \leq 1$ and $J_{h} \geq 1 / 2$ ; bounded, uniformly coercive forms and bounded exact and discrete loads; the stated exact and discrete variational solutions; and, when a lift is present, the stated decomposition of the load difference.

[L1]

$H^{k} = W^{k, 2}$ with the derivative-sum Sobolev norm, and $H_{0}^{1} = W_{0}^{1, 2}$ is the norm closure of $C_{c}^{\infty}$ in $H^{1}$ . (The notation $H^{k}$ and the reserved zero-boundary symbol, Integer-order Sobolev spaces and their norms, Zero-boundary Sobolev space as a norm closure)

[L2]

A matching affine mesh is a finite face-to-face triangulation by nondegenerate cells; shape regularity gives the cellwise scaling hypotheses used by the P1 interpolation estimate. (Matching affine simplicial meshes and shape regularity, Shape regularity controls affine simplex geometry)

[L3]

$e_{0}$ and $e_{1}$ denote the uniform value and derivative geometry gaps. (Curved-domain geometry approximation errors)

[F1]

For the parabolic geometry family, $e_{0} \leq C h^{2}$ , $e_{1} \leq C h$ , and $J_{h} \geq 1 / 2$ for sufficiently small $h$ . (P1 approximation of a parabolic shear map)

[F2]

The pullback of the physical Laplace form has tensor $J D Φ^{- 1} D Φ^{- T}$ , and the tensor difference obeys $∥ B - B_{h} ∥_{L^{\infty}} \leq C e_{1}$ . (Pullback gradients and induced surface metrics, Derivative geometry error controls the Laplace tensor defect)

[F3]

On each affine triangle, the identity-map P1 interpolant of an $H^{2}$ function has $H^{1}$ error at most $C h_{K} ∥ u ∥_{H^{2} (K)}$ ; the constants are uniform over the shape-regular mesh family. (P1 interpolation scaling on uniformly curved cells)

[F4]

The nodal P1 interpolant of $u \in H^{2} \cap H_{0}^{1}$ is well-defined, continuous across the mesh, zero on boundary edges, and belongs to $V_{h}$ . (The nodal P1 interpolant preserves homogeneous boundary values)

[F5]

The first Strang estimate bounds the error by best approximation, the form defect, and the load defect divided by the uniform discrete coercivity constant. (First Strang estimate for conforming perturbed Galerkin problems)

[F6]

The variational-crime framework defines $δ_{a, h} (v_{h}) = \sup_{w_{h} \neq 0} ∣ a (v_{h}, w_{h}) - a_{h} (v_{h}, w_{h}) ∣ / ∥ w_{h} ∥_{H^{1}}$ and $δ_{F, h} = \sup_{w_{h} \neq 0} ∣ F (w_{h}) - F_{h} (w_{h}) ∣ / ∥ w_{h} ∥_{H^{1}}$ . (Variational-crime settings and consistency defects)

[F7]

For the common $C^{2}$ physical lift, the pulled-back residual satisfies $∥ ℓ_{\partial, h} ∥_{V^{*}} \leq C_{G} (e_{0} + e_{1})$ . (Geometry error bounds a pulled-back boundary-lift residual)

[F8]

With the standard $H^{1}$ inner product, $H_{0}^{1} (\hat{Ω})$ is a closed Hilbert subspace of $H^{1} (\hat{Ω})$ . (The Sobolev space $H^{1}$ is a Hilbert space)

[A1]

Countable Choice is assumed through the first-Strang, geometry and interpolation interfaces. (The Axiom of Countable Choice ( ${A C}_{ω}$ ))

[A2]

The Axiom of Choice is assumed for the automatic nodal-boundedness clause of the interpolation supplier and the local conformity result. (The Axiom of Choice)

Proof

1.1A1F1F5F8L1given

The exact shear has positive determinant, and [F1] gives $J_{h} \geq 1 / 2$ ; thus both tensor formulas are defined almost everywhere. By [L1] and [F8], $V = H_{0}^{1} (\hat{Ω})$ is Hilbert in the stated $H^{1}$ norm. The boundedness and coercivity assumptions, bounded loads, finite-dimensional conforming subspace $V_{h} \subset V$ , and the given variational equations supply the remaining hypotheses of [F5].

1.2A1F1F2F6F7L3givenalgebra

For $v_{h}, w_{h} \in V_{h}$ , [F2] and integral Cauchy--Schwarz give $∣ a (v_{h}, w_{h}) - a_{h} (v_{h}, w_{h}) ∣ \leq C e_{1} ∥ v_{h} ∥_{H^{1}} ∥ w_{h} ∥_{H^{1}} .$ Taking the supremum in [F6] yields $δ_{a, h} (v_{h}) \leq C h ∥ v_{h} ∥_{H^{1}}$ by [F1]. The assumed load decomposition and the triangle inequality give $δ_{F, h} \leq ϵ_{F, h}^{b u l k} + ϵ_{\partial, h}$ , because restriction of the $V^{*}$ residual norm to $V_{h} \subset V$ cannot increase it.

1.3F3F4A1A2L1L2givenalgebra

By [L2], the shape-regular matching mesh satisfies the affine scaling hypotheses in [F3]. Apply [F3] on each triangle with the identity geometry map. The finite element interpolants assemble into the global nodal interpolant $I_{h} u$ , and [F4] gives $I_{h} u \in V_{h}$ . Squaring each local estimate, summing over cells, and using $h_{K} \leq h$ gives $∥ u - I_{h} u ∥_{H^{1}} \leq C h ∥ u ∥_{H^{2}}$ . Since $h \leq 1$ , [L1] gives $∥ I_{h} u ∥_{H^{1}} \leq ∥ u ∥_{H^{1}} + C h ∥ u ∥_{H^{2}} \leq C ∥ u ∥_{H^{2}}$ .

2.1A1F5step 1.2step 1.3algebra

Use $I_{h} u$ as the comparison function in [F5]. Step 1.3 bounds the best-approximation term by $C h ∥ u ∥_{H^{2}}$ ; steps 1.2 and 1.3 bound its form defect by $C h ∥ I_{h} u ∥_{H^{1}} \leq C h ∥ u ∥_{H^{2}}$ ; and step 1.2 bounds the load defect by the two stated load tolerances. Uniform positive discrete coercivity in [F5] proves the displayed Strang estimate.

3.1A1F1F7L3step 2.1algebra∎

By [F1] and [F7], $ϵ_{\partial, h} \leq C_{G} (e_{0} + e_{1}) \leq C_{G} (h^{2} + h) \leq C_{G}^{'} h$ for $h \leq 1$ . The residual remains an explicit term of the error bound, including when its $O (h)$ rate dominates higher-order geometric terms.

AlgorithmAlgorithm: Literature-sourcedProof: Not applicableOpen item page →

Exact certified clipping of convex rational polygons

Definition

Input two cyclic vertex lists for positive-area convex polygons in $R^{2}$ , with rational coordinates. The closing edge is implicit; if the last listed vertex repeats the first, delete that final copy. Delete consecutive duplicate vertices, including across the cyclic endpoint, then return unresolved if a list has fewer than three vertices, any remaining repeated vertex, a zero-length edge, or zero signed shoelace area. Reverse a negatively oriented list so both polygons are counterclockwise. For each list, certify convexity as follows: for every directed edge, evaluate the orientation of that edge with every listed vertex and require every sign to be nonnegative; if three consecutive vertices are collinear, require the middle one to lie between the other two; and for every pair of nonadjacent closed edges, certify that they do not intersect. Test the latter exactly using the four orientation signs: two segments $A B, C D$ intersect if the signs for $C, D$ against $A B$ are strictly opposite and the signs for $A, B$ against $C D$ are strictly opposite, or if one of these signs is zero and its point lies in the closed coordinatewise bounding rectangle of the corresponding segment. Return unresolved if any certificate check fails. These finite checks certify that each normalized list is the simple counterclockwise boundary of its convex hull, allowing redundant collinear vertices.

For every rational orientation test, clear one common positive denominator from the coordinates of its three points and call Certified predicate for exact dyadic geometric inputs on the resulting integer (hence dyadic) points. Propagate any result other than an exact positive, zero, or negative sign as unresolved. For each directed edge of $Q$ , clip the current cyclic list of $P$ to that edge's closed left half-plane, treating a point $X$ as inside exactly when $s (X) \geq 0$ , where $s (X)$ is its signed edge determinant. Traverse cyclically by setting $S$ to the last current vertex and then taking each current vertex in list order as $E$ . Apply exactly one of these branches:

If $s (S) \geq 0$ and $s (E) \geq 0$ , append $E$ .
If $s (S) \geq 0 > s (E)$ , append $S + t (E - S)$ .
If $s (S) < 0 \leq s (E)$ , append $S + t (E - S)$ and then $E$ .
If $s (S) < 0$ and $s (E) < 0$ , append nothing.

In either crossing branch set $t = s (S) / (s (S) - s (E))$ . The strict sign inequalities make this denominator nonzero and give $t \in [0, 1]$ ; when an endpoint sign is zero the intersection is that endpoint. No division is performed in either noncrossing branch. Remove consecutive duplicate output vertices after each pass, including a duplicate across the cyclic endpoint, and continue with the next edge of $Q$ . If the current list is empty, it remains empty. Return the final rational cyclic list and area zero when it has fewer than three noncollinear vertices; otherwise return its exact shoelace area. No floating tolerance is used.

Failure behavior

The input polygons represent convex cells in the intersection-volume remap of Intersection-volume conservative remapping. A failed convexity check or uncertified predicate sign returns unresolved; it is never guessed. A negative crossing denominator is valid and is used as written. All constructions after the exact dyadic predicate calls use exact rational arithmetic.

TheoremStatement: AI-adaptedProof: AI-adaptedprecheck passOpen item page →

Certified clipping returns the exact convex polygon overlap

Statement

Assume Countable Choice. For positive-area convex polygons $P, Q \subset R^{2}$ with rational vertices, Exact certified clipping of convex rational polygons terminates and returns exactly $P \cap Q$ as a cyclic list of rational vertices, with its exact Lebesgue area. Empty intersections and intersections consisting only of a point or segment return area zero. The result can be used as the exact weight $∣ P \cap Q ∣$ in Intersection-volume conservative remapping.

Facts & Assumptions

Given: Countable Choice; two finite convex rational polygons with cyclic vertices, exact rational arithmetic, and certified orientation calls.

[F1]

Exact certified clipping of convex rational polygons: the finite exact certificate checks verify the normalized input cycles; each clipping pass traverses the current cyclic list, applies the four inside/outside sign branches, inserts exact crossing points only on strict crossings or crossings with one boundary endpoint, removes consecutive duplicates, and uses the exact shoelace formula.

[F2]

Certified predicate for exact dyadic geometric inputs: on dyadic inputs it returns the exact orientation sign, including zero, and terminates.

[F3]

Intersection-volume conservative remapping: a remap weight is the measure of the exact cell intersection.

[F4]

Every affine hyperplane of $R^{n}$ , and hence every proper linear subspace, is Lebesgue null: under Countable Choice every affine hyperplane in $R^{2}$ and every subset of it is Lebesgue null.

[A1]

Countable Choice is assumed for the measure interfaces in [F3] and [F4] (The Axiom of Countable Choice ( ${A C}_{ω}$ )).

Proof

1.1F1F2givenalgebra

Clearing one common positive denominator from the three rational points in an orientation test multiplies the determinant by a positive square, so its sign is unchanged and all scaled coordinates are integers. Therefore [F2] returns the exact side classification, including boundary zero, for every clipping pass.

2.1F1step 1.1algebra

The algorithm's finite certificate accepts only a simple counterclockwise cycle whose vertices lie in the closed left half-plane of every directed edge, with any collinear consecutive triple ordered monotonically. Each edge is therefore a supporting boundary segment of the convex hull of the listed vertices; the simple closed cycle with positive area traverses that hull boundary once, so the certified input is the stated convex polygon. Now fix one directed edge of $Q$ and write $s (X)$ for its signed edge determinant. If $s (S), s (E) \geq 0$ , the whole segment remains and the traversal appends $E$ . If $s (S) \geq 0 > s (E)$ , it appends the crossing point; if $s (S) < 0 \leq s (E)$ , it appends the crossing point and $E$ ; and if both signs are negative, it appends nothing. In either crossing case, $s (S) - s (E)$ has the strict sign of the crossing and is nonzero, and $t = s (S) / (s (S) - s (E))$ lies in $[0, 1]$ . If an endpoint lies on the clipping line, the formula gives that endpoint exactly. Thus each pass returns the cyclic boundary of the preceding convex intersection with this closed half-plane, preserving isolated boundary vertices and degenerate point or segment outputs.

3.1step 2.1given

Induction over the finite edge list of $Q$ shows the final polygon is $P$ intersected with every defining half-plane of $Q$ , hence is exactly $P \cap Q$ . Each pass processes a finite list and adds at most two crossings per clip edge, so the finitely many passes terminate.

4.1F1F3F4A1step 3.1algebra∎

The final vertices are rational because every crossing uses rational operations with a nonzero exact denominator. For a nondegenerate simple polygon the shoelace sum equals its signed area; the output is counterclockwise, so this is its nonnegative Lebesgue area. A convex intersection with fewer than three noncollinear vertices is empty or lies in an affine line. By [F4], the line and all its subsets are Lebesgue null, so the returned area is zero in these degenerate cases.

TheoremStatement: AI-adaptedProof: AI-adaptedprecheck passOpen item page →

Quality and finite termination for the curved square NVB family

Statement

For every tolerance $0 < τ \leq σ / 4 = 1 / 4$ , the algorithm Delaunay-seeded curved uniform NVB refinement with square boundary angle $α = π / 2$ and nonincident-feature separation $σ = 1$ terminates after finitely many three-generation cycles. Its reference triangles remain right isosceles with minimum angle $π / 4$ , all interfaces match, and every curved cell map is orientation preserving. Pointwise on each cell, if $a_{K}$ is an affine parametrization of its reference triangle, then the induced metric $G_{Φ, K} = (D (Φ \circ a_{K}))^{T} D (Φ \circ a_{K})$ has spectral condition number $κ_{2} (G_{Φ, K}) \leq (81 / 16) κ_{2} (G_{r e f, K})$ , where $G_{r e f, K} = (D a_{K})^{T} D a_{K}$ . The returned maximum curved-cell diameter is at most $τ$ . This is a guarantee for this square/shear family; it asserts no general Delaunay minimum-angle theorem, adaptive complexity bound, or 3D shape bound.

Facts & Assumptions

Given: The four square-corner sites, a successful exact Delaunay triangulation, compatible initial labels, the shear $Φ (x, y) = (x, y + x^{2} / 4)$ , tolerance $0 < τ \leq 1 / 4$ , boundary angle $π / 2$ , and feature separation $σ = 1$ .

[F1]

Exact planar insertion terminates with a weak empty-circle triangulation: the exact planar algorithm returns a triangulation of the convex hull with a coherent tie convention.

[F2]

Compatible 2D newest-vertex-bisection meshes: a bisection splits its reference edge at the midpoint and retains the prescribed generation labels.

[F3]

Shape regularity and local reduction under 2D newest-vertex bisection: three complete generations give shape-regular descendants and child diameters at most half the parent diameter.

[F4]

Conforming NVB closure preserves curved shared traces: recursive closure yields matching affine edges, and a common admissible map sends them to matching curved interfaces.

[F6]

Dorfler marking and conforming newest-vertex refinement: a budget-exhausted call discards the tentative forest and returns the original mesh.

[A1]

The algorithm input certifies that the four square corners have interior angles $π / 2$ and that the minimum distance between nonincident boundary features is at least $1$ (Delaunay-seeded curved uniform NVB refinement).

[F5]

Admissible isoparametric curved cells and Curved-domain geometry approximation errors: positive Jacobian and derivative/inverse bounds define admissible curved-cell geometry.

Proof

1.1F1A1givenalgebra

Directly from the square coordinates, each interior angle is $π / 2$ , opposite edges and nonincident vertices/edges are separated by distance $2$ , so $σ = 1$ is a valid lower certificate [A1]. The four corners are distinct dyadic sites in convex position. By [F1] the returned Delaunay triangulation covers the square; with four extreme vertices it has exactly two triangles sharing one diagonal. Each is right isosceles. Labeling the shared diagonal as reference on both sides gives compatible initial labels. The two seed triangles have different vertex-site sets, hence distinct sorted site-index triples; their lexicographic ranks initialize two distinct operational roots without changing those edge labels.

1.2F2F4F6givenconstruct

In each call the squared estimator array is constantly one and the oscillation array is zero. With $θ_{E} = 1$ , the shortest initial segment whose sum reaches the total contains every cell, so every current cell is requested for three generations. The persistent root-and-binary-path identifiers in [F2] assign a unique order to every generated pending leaf; child identifiers are determined by the stored parent vertex list before it is replaced. At every stage the pending set is finite, so its least identifier exists. The recursive closure theorem [F4] says this finite request terminates, so some finite number $N$ of bisections suffices. By [F6], failed budget calls discard tentative splits and their identifiers, leaving the same ordered input mesh for retry; repeated doubling eventually reaches $B \geq N$ and a complete call.

1.3F4F5givenalgebra

The shear extends to the global $C^{2}$ diffeomorphism $Φ (x, y) = (x, y + x^{2} / 4)$ of $R^{2}$ , with explicit inverse $Φ^{- 1} (X, Y) = (X, Y - X^{2} / 4)$ and determinant $\det D Φ = 1$ . On the square, $D Φ = (\begin{array}{cc} 1 & 0 \\ x / 2 & 1 \end{array})$ and both $∥ D Φ ∥_{o p}$ and $∥ D Φ^{- 1} ∥_{o p}$ are at most $3 / 2$ by the Frobenius bound. The second derivatives of the map and its inverse have operator norm $1 / 2$ . Thus the shear satisfies the positive-Jacobian, derivative, inverse-derivative and $C^{2}$ bounds of [F5]; its cell traces agree because every cell uses the same global map, and its injectivity verifies the common-map hypothesis of [F4].

2.1F2F3step 1.1algebra

Each right-isosceles triangle has its hypotenuse as reference edge. Bisection at the hypotenuse midpoint joins that point to the right-angle vertex; the two resulting triangles have equal legs of half the parent hypotenuse and hence are right isosceles, with their inherited leg as hypotenuse/reference. Thus every bisection in the closure process preserves the $45^{\circ}$ minimum angle; [F3] supplies the uniform shape bound and three-generation diameter reduction.

2.2F3F5step 1.2algebra

By [F3], each complete three-generation request reduces every requested parent diameter by at least one half; closure only adds bisections, which cannot increase diameter. The initial reference diameter is $2 \sqrt{2}$ . Since $∥ D Φ ∥_{o p} \leq ∥ D Φ ∥_{F} \leq 3 / 2$ on the square, the mean-value inequality gives mapped diameter at most $(3 / 2) 2^{- k} 2 \sqrt{2}$ . A finite integer $k$ satisfies the stopping inequality for every $τ > 0$ .

3.1F2F5step 2.1step 2.2step 1.3algebra∎

Let $A_{K} = D a_{K}$ . The bounds in step 1.3 imply $κ_{2} (D Φ) \leq ∥ D Φ ∥_{o p} ∥ D Φ^{- 1} ∥_{o p} \leq 9 / 4$ . Since $D (Φ \circ a_{K}) = D Φ (a_{K}) A_{K}$ , submultiplicativity gives $κ_{2} (D (Φ \circ a_{K})) \leq (9 / 4) κ_{2} (A_{K})$ . The spectral condition number of $D (Φ \circ a_{K})^{T} D (Φ \circ a_{K})$ is the square of that derivative condition number, and $κ_{2} (A_{K}^{T} A_{K}) = κ_{2} (A_{K})^{2}$ , proving the stated $81 / 16$ metric bound. The reference triangles have disjoint interiors in a square of area $4$ . Any right-isosceles reference triangle of diameter at least $τ / (3 / 2)$ has area at least $τ^{2} / 9$ ; disjoint interiors therefore allow at most $36 / τ^{2}$ such cells. This packing bound is consistent with the finite uniform refinement and the stated positive feature and angle certificates.

5 · Examples, counterexamples and false statements

None yet.

Curved geometry, mesh generation and conservative transfer

1 · Prerequisites

2 · Summary

3 · Logical flowchart

4 · Definitions, theorems and proofs

Intersection-volume conservative remapping

Definition

Notes

Admissible isoparametric curved cells

Definition

Shape regularity and normals

The nodal P1 interpolant preserves homogeneous boundary values

Statement

Facts & Assumptions

Proof

Curved-domain geometry approximation errors

Definition

Tensor convention

P1 interpolation scaling on uniformly curved cells

Statement

Facts & Assumptions

Proof

Pullback gradients and induced surface metrics

Statement

Facts & Assumptions

Proof

Overlap remapping is an L2 projection, conservative and positive

Statement

Facts & Assumptions

Proof

Geometry error bounds a pulled-back boundary-lift residual

Statement

Facts & Assumptions

Proof

Cofactor, surface-Jacobian, and normal perturbation bounds

Statement

Facts & Assumptions

Proof

Derivative geometry error controls the Laplace tensor defect

Statement

Facts & Assumptions

Proof

P1 approximation of a parabolic shear map

Statement

Facts & Assumptions

Proof

Remap error separates source, target and geometry approximation

Statement

Facts & Assumptions

Proof

Conforming NVB closure preserves curved shared traces

Statement

Facts & Assumptions

Proof

Strang error bound for a parabolic isoparametric P1 family

Statement

Facts & Assumptions

Proof

Exact certified clipping of convex rational polygons

Definition

Failure behavior

Certified clipping returns the exact convex polygon overlap

Statement

Facts & Assumptions

Proof

Delaunay-seeded curved uniform NVB refinement

Definition

Procedure notes

Quality and finite termination for the curved square NVB family

Statement

Facts & Assumptions

Proof

5 · Examples, counterexamples and false statements

Sources