Dirichlet diffraction on one open region
Independent exposition, proofs, exercises and illustration: GPT-6 Astra (OpenAI), 9 October 2026. CC0-1.0.
A gain at one point, repeated on smaller neighborhoods, need not remove that point from the smooth wavefront set. We instead fix a geometric region and improve the order at every point of that region. The cutoffs and constants can depend on the order; the region and the final tester do not.
The antecedent is Lars Hörmander, The Analysis of Linear Partial Differential Operators III, Springer 2007 eBook, Section 24.4, especially the accessible-region argument on printed page 448 and the induction on pages 449–451. We retain complex matrix lower terms, the actual H1 solution and an L2 source that may be rough in the normal variable. The localized half-gain, full incoming estimate, elliptic correction theorem, and volume and boundary reconstruction provide the exact earlier analytic components. The proof map records their complete dependencies. Lebl's transitive proofs remain external.
1. The theorem and the common-region requirement
B0. The Dirichlet receiving theorem. Work in a compact coordinate patch of the half-space, with D=−i∂, finite component space Cn, and
P=Dx2−R(x,z,Dz),σ2(R)=r(x,z,η)In,p=ρ2−r.(DB1)
The principal r is real and quadratic in η; all smooth lower coefficients may be complex matrices. Suppose u is locally H1, Pu=f∈L2, and on an open conic parameter region W, with η=0,
χf∈Lx2Hzm(every m∈R),χ(0)γu∈Hzm(every m∈R)(DB2)
for every scalar proper tangential order-zero test χ compactly supported there. Boundary cutoffs in the second assertion are supported in W∩{x=0}. All actual lower terms and cutoff remainders remain. At a=(0,z∗,η∗), assume
r(a)=0,rx(a)>0.(DB3)
Assume a point of the short negative-normal interior characteristic germ through a is ordinarily regular for u, with the intervening projection contained in W. Choose an open regular cap Γ on a small interior slice around that point. Source regularity in (DB2) implies ordinary source smoothness at every finite-normal covector with nonzero tangential component, so ordinary matrix propagation permits this choice along the germ.
We prove that a fixed open parameter neighborhood W0 of a has
χu∈Xsfor every real sand every such χ with support in W0,∥v∥Xs2=∥Λsv∥22+∥Λs−1Dxv∥22,Λ=⟨Dz⟩.(DB4)
Thus one fixed smaller compressed neighborhood has every H1-based compressed order. This is a Dirichlet statement with microlocally smooth value data, including zero data. It does not replace a Neumann or Robin condition by a value condition.
2. Fix the accessible region before choosing an order
B1. Geometry through a transverse reflection or a strict tangency. Shrink a normalized coordinate box so that rx≥c∣η∣2>0, tangential covector lengths remain comparable on the short flow segments, and the box and all needed arcs project inside W. For the full Hamilton flow,
x˙=2ρ,ρ˙=rx,x¨=2rx>0.(DB5)
The normal coordinate is strictly convex along each extended short characteristic. A negative branch followed backward goes into the interior and meets the regular slice transversely. ISE:I1 proves that its entire nearby family meets Γ, with the full intervening path inside the source region.
For the positive branch, follow the extended smooth flow backward. There are three local cases. Its minimum normal coordinate μ can be positive, zero or negative. For μ>0, it turns in the interior and continues to the negative branch. For μ=0, it touches the boundary at the unique strict glancing point. For μ<0, the positive branch meets the face transversely before reaching its extended minimum. At that face replace ρ by −ρ, keeping the base point and tangential covector, and continue backward on the negative branch. This is the exact root reflection for (DB1).
We justify the continuity needed at μ=0. The equation ρ=0 is transverse to the extended flow by (DB5). The smooth implicit-function theorem therefore supplies a smooth minimum section and a smooth minimum time for all nearby full covectors. Write the normal coordinate along a trajectory, with time centered at its minimum, as
x(t)=μ+t2b(t),b(t)=∫01(1−v)x′′(vt)dv,0<c1≤b≤c2.(DB6)
All parameters of the initial covector are retained in b. The bounds hold on one compact normalized box. A boundary hit when μ<0 has ∣t∣≤∣μ∣/c1; its normal covector is O(∣μ∣). Therefore both its location and the reflected covector approach the minimum covector as μ↑0. Smooth flow dependence after that hit, followed by the transverse intersection with the fixed interior slice, proves continuity of the broken hitting map at tangency. For μ>0 it is the ordinary smooth flow. No differentiability of the broken hitting time at μ=0 is asserted.
Define W0 locally as follows. A parameter point with r≥0 belongs to W0 when each characteristic lift
(x,z;±r(x,z,η),η)(DB7)
is reached from Γ by one of these short paths, staying over W, with at most one transverse reflection or one tangency. Include the nearby r<0 points, which have no real lifts. Use the chosen small flow box for these paths. Transverse hitting, the continuity just proved, and continuity of the roots at r=0 show that W0 is relatively open and contains a. To check openness with the entire-path condition, cover the compact path by finitely many open sets whose closures project inside W; continuous nearby paths stay in their union, and their cap endpoint remains in the open set Γ. Positive homogeneity gives an open conic region after removing the normalization.
Two properties of this definition will be used. Every negative lift over W0 is reached without a reflection. Any positive lift whose backward path touches a boundary glancing point b has b∈W0: the path from Γ to that point is a subpath, and its two lifts coincide. A broken path has at most one boundary event, since ρ increases along the short ordinary pieces and changes from negative to positive at a forward reflection. These properties prevent the induction from asking for regularity at a glancing point outside its region.
3. The elliptic boundary step on the actual rough domain
B2. A full derivative at a boundary point where r<0. Fix s≥1, and assume the local input property
χu∈Xsfor all compactly supported tangential tests in W0.(DB8)
Near a boundary parameter point with r<0, we prove χu∈Xs+1 on a smaller neighborhood. Only the data (DB2), the actual H1 domain and (DB8) are used.
Choose an inner scalar tangential cutoff A, with normal support in a small collar and full symbol supported in that elliptic cone, and an outer cutoff controlling its support and all derivatives. Put v=Au, periodically embedded in a larger tangential chart and extended by zero past its compact positive normal support. Its complete equation is
Pv=Af+[P,A]u,[P,A]u=−2iAxDxu−Axxu−[R,A]u.(DB9)
The scalar principal symbol makes [R,A] order one. Outer factorization and (DB8) put the right side in Lx2Hzs−1; tangentially smoothing remainders act on the original H1 input and need not be smooth in x. They have every required tangential order, which is sufficient here.
Extend the full tangential coefficients to the globally elliptic cylinder used in EW:P2–P4, retaining the leading normal coefficient In. In this case the construction is especially direct: on a narrow cone combine −r with a frozen positive multiple of ∣η∣2, retaining all lower matrix terms by smooth cutoffs. The full principal polynomial stays uniformly positive scalar for real normal frequency. The stable principal Cauchy space consists of
(h,i−r0h),h∈Cn,(DB10)
so Dirichlet evaluation is a bijection on it. The exact compact-chart quantization and its full residuals are those of EW:P2–P4. Denote the auxiliary polynomial by Pe. Since its top normal coefficient is still In, (Pe−P)A is tangentially smoothing, with no second normal derivative. Thus the actual auxiliary forcing and datum satisfy
Fe=Pev∈Lx2Hzs−1,ge=γv=A(0)γu∈H∞.(DB11)
All tangential inputs on the auxiliary compact boundary are included.
We first reach a legitimate domain for the volume reconstruction. The actual v is H1 and Dx2v=Rev+Fe∈Lx2Hz−1. The restriction-space normal recovery MH:R1–R2, with the pure normal polynomial Dx2, gives
v∈H(2,−1).(DB12)
This is the one-step normal recovery proved in EW:L3; its Fourier weights are q2λ−1, with q=⟨(ρ,η)⟩. It does not use zero extension as a bounded positive-order extension. The actual trace agrees with the H1 trace by the mixed trace identification.
Use the exact left identity VB16, at normal index two:
v=ΦFe+ΛDge+Kv,Φ:Lx2Hzt⟶H(2,t),K:H(2,t)⟶H(3,t)⊂H(2,t+1).(DB13)
Here ΛD is VB's Dirichlet layer, not the tangential Fourier multiplier. Its arbitrary real output split maps the smooth ge into every displayed target. The left error has only its proved one-order gain; it has not been called smoothing. The last inclusion follows from q≥λ, and holds after taking restriction infima.
The first two terms of (DB13) belong to H(2,s−1). Starting at t=−1, the same distributional identity improves the tangential index to min(t+1,s−1). A finite number of repetitions reaches s−1, including a fractional last step by embedding. No new source is formed during this repetition. Finally
H(2,s−1)⊂Xs+1,λs+1≤q2λs−1,∣ρ∣λs≤q2λs−1.(DB14)
Derivative restriction and the infimum over extensions prove the second component as well. Thus the elliptic boundary step applies to the original rough normal source, without an unproved membership in the intrinsic smooth-source class.
4. A transverse boundary point has every tangential order
B3. Use the value datum after the incoming factor. Let b∈W0∩{x=0,r>0}. Its negative germ comes from Γ, so it is ordinarily regular by interior propagation and (DB2). On a sufficiently small closed hyperbolic collar, ISE:I0–I6 construct a full positive root A+ and prove
ϕ(Dx−A+)u∈Lx2Hzmfor every m(DB15)
for all smaller tests in that collar. More explicitly, the geometric incoming-tube and matrix-factor constructions in ISE apply here with a positive root gap; the tangency part of its geometry is unnecessary. The family of negative lifts meets Γ by B1 and transversality. One may choose the root on the union of the incoming tubes and the short collar used below.
Put L+=Dx−A+. Transport a scalar boundary cutoff by this positive-root evolution. The complete matrix construction ISE:I3, with the sign of its real scalar root changed, gives a proper matrix family Q+, elliptic on a smaller outgoing tube, with
[L+,Q+]∈Cx∞Ψtan−∞,Q+(0)=Q0.(DB16)
Its matrix commutator, all lower corrections and exact initial operator are retained. Set h=Q+u. Then
L+h=Q+L+u+[L+,Q+]u,h(0)=Q0γu.(DB17)
The right side is Lx2Hzm for every m, by (DB15) on its entire support. The actual initial trace is smooth by (DB2). The exact oriented evolution and weak uniqueness proof ISE:I4 now give h∈CxHzm for every m. Its equation gives Dxh∈Lx2Hzm−1. Full tangential division by Q+, including its normal derivative and its smoothing errors on u,Dxu, proves all Xm orders on a smaller collar. Thus the complete matrix Dirichlet reflection step is available on the actual H1 domain. It does not invoke a scalar reflection theorem for a matrix lower-order system.
5. Recover a tangential norm from interior propagation
B4. Account for the large normal frequencies. Fix an interior parameter point in W0, and retain (DB8). Let q=s+1/2. Suppose ordinary microlocal Hq regularity of u is known at every characteristic lift over that point. We prove a tangentially localized Xq norm near it.
First, a compactly based ordinary operator B of order −k, k≥0, has the anisotropic bound
B:Lx2Hzt⟶Lx2Hzt+k(t∈R).(DB18)
Here is a direct proof for the needed full-frequency operators. For its left symbol, Fourier transformation in the compact base gives a kernel bounded by
∣b(ζ−ζ′,ζ′)∣≤CN⟨ζ−ζ′⟩−N⟨ζ′⟩−k,ζ=(ρ,η).(DB19)
Multiplying by ⟨η⟩t+k⟨η′⟩−t, the tangential Peetre inequality bounds the resulting factor by a fixed power of ⟨ζ−ζ′⟩: indeed
⟨η⟩t+k/⟨η′⟩t+k
costs at most ⟨η−η′⟩∣t+k∣, and
⟨η′⟩k≤⟨ζ′⟩k.
Choose N larger than this power plus the full dimension and apply the two Schur integrals. Compact input cutoffs and smoothing proper-kernel terms satisfy the same estimate. Truncation followed by the uniform bound identifies the actual operator on L2-based distributions. In particular DxB has the same bound with k−1 when k≥1.
Choose a scalar tangential cutoff χ supported away from the face and inside W0, and set v=χu. Its full-space equation, after a slightly larger compact localization, has
Pv=χf+[P,χ]u∈Lx2Hzs−1.(DB20)
As in (DB9), this includes both normal derivatives of χ and the full matrix commutator. Choose C so large that p is elliptic where ∣ρ∣≥C⟨η⟩. A full ordinary matrix parametrix with a high-normal output cutoff gives
Ehiv=B−2Pv+Sv,B−2∈Ψ−2,S∈Ψ−∞,(DB21)
on a smaller base patch. Complete symbol recursion and proper off-support estimates give the displayed smoothing remainder, including the derivatives of all enlarged cutoffs. Formula (DB18) and (DB20) put this high-normal piece in Xs+1.
The remaining normalized frequencies have ∣ρ∣≤2C⟨η⟩. Source regularity (DB2) implies ordinary smoothness of f on this finite-normal cone: all compact tangential derivatives are L2, hence L1, and their Fourier estimates decay arbitrarily in η, which is comparable to the full frequency on that cone. The ordinary elliptic parametrix makes u smooth at its noncharacteristic points. At its characteristic points use the assumed Hq regularity. Compactness of the normal interval and openness of ordinary Hq regularity give one slightly smaller parameter patch with
Elov∈Hq,Elo=I−Ehion the smaller patch.(DB22)
Separated cone remainders are fully smoothing by the ordinary calculus. For q≥1, the weights λq and ∣ρ∣λq−1 are bounded by a constant times ⟨(ρ,η)⟩q, so this piece is in Xq. Combining (DB21)–(DB22) proves the claimed local norm. This step neither discards pure normal frequencies nor assumes that the rough normal source is ordinarily smooth there.
Conversely, a tangential Xq norm implies ordinary Hq regularity on every smaller finite-normal cone: insert its full-frequency cutoff and use ⟨(ρ,η)⟩q≲⟨η⟩q there. Tangential elliptic division and separated-frequency estimates transfer this assertion from an elliptic tangential tester to the original u.
6. Improve the order throughout the same region
B5. Induction over the whole open set. Define the statement
P(s):χu∈Xs for every scalar proper test compactly supported in W0.(DB23)
The actual H1 input proves P(1). Assume P(s) for s≥1.
At every boundary glancing parameter point in W0, B1 supplies a regular negative germ. The same source and value-data hypotheses hold there, and rx>0. Choose a small parameter neighborhood contained in W0. ISE proves the full incoming norms on both SDC supports, after the damping constant for this s has been fixed. LG:L0–L6 therefore give an elliptic tangential tester with Xs+1/2 output at that point. The chosen tester and its support may depend on both the point and s.
At a boundary elliptic point, B2 gives the stronger Xs+1 result. At a boundary hyperbolic point, B3 gives every tangential order. Thus each boundary point of W0 has a neighborhood on which the desired Xs+1/2 localization holds.
Consider an interior characteristic lift over W0, and follow its B1 path backward to Γ. If there is no boundary event, ordinary matrix propagation gives smoothness along the entire path. A transverse event is passed using B3: on its outgoing germ u is ordinarily smooth by the last paragraph of B4, and propagation supplies the rest of the path. If the event is a tangency, it is a boundary glancing point of W0 by B1. Its just-proved local gain gives ordinary Hs+1/2 regularity at a nearby positive interior point of the outgoing arc. Ordinary real-principal matrix propagation carries that finite order to the chosen lift; the intervening compact arc is interior and its source is smooth. The incoming side is already smooth from Γ. All characteristic lifts are therefore Hs+1/2. B4 supplies a local Xs+1/2 tester at each interior parameter point, including points with no real lift.
Finally take any test χ with compact normalized support in W0. The neighborhoods just obtained form an open cover of that compact set. Choose a finite subcover and a conic partition subordinate to it. Full tangential elliptic parametrices express χu as a finite sum of order-zero operators applied to the locally controlled outputs, plus a tangentially smoothing family on the original H1 input. Differentiating this identity in x adds the order-zero derivatives of the coefficients and the smoothing derivative; all are bounded in the required L2Hs−1/2 space. Thus
P(s)⟹P(s+1/2),P(1+j/2)(j=0,1,2,…).(DB24)
Monotonicity of the Sobolev weights proves (DB4) for every real s.
The quantifiers matter. Every induction step proves regularity at all points of the same W0. Only then is a compact target covered. There is no infinite intersection of progressively smaller neighborhoods of a, and no uniform bound in s, in the number of local patches, or in the damping constant has been assumed.
7. Return to the original compressed energy front
B6. One compressed neighborhood for every energy order. Choose a fixed tangential cutoff χ supported in W0 and equal to one on a larger neighborhood of a. Fix a small compressed cone
Ob:x≥0,(x,z,η) in that inner region,∣σ∣<c⟨η⟩,σ=xρ.(DB25)
At high frequency the inhomogeneous bracket can be replaced by ∣η∣. Take its base support small enough that the full compact input of every chosen strong kernel lies inside the normal plateau of χ. The strong ratio cutoff may be fixed near input/output normal ratio one. All later order-m testers have microsupport in the same slightly larger compressed cone and are elliptic on Ob.
The full compressed composition theorem gives, for such a tester T of order m≥0,
∥Tu∥H1≤CT,χ(∥χu∥Xm+1+∥u∥H1(K))(DB26)
with a fixed larger compact input set K. We spell out the order comparison. On its cone, the compressed frequency norm ⟨(σ,η)⟩ is bounded by a constant times ⟨η⟩. Complete composition with a tangential order reducer therefore puts TΛ−m in the strong order-zero class. All product remainders have the same or lower order, since differentiated cone cutoffs stay in a slightly larger cone. The strong L2 bound then controls Tu by the tangential m-norm. Applying Dz costs one order.
For the unweighted normal derivative retain the exact normal commutator from LB:A1 and LB:H1:
DxTu=TDxu+ETu+NTDxu,ordET=m,ordNT=m−1.(DB27)
The term NTDxu is essential. The same order-reducer argument controls the three terms by the Xm+1 norm. To insert χ, use the full compressed/tangential composition with its plateau on the complete kernel input region. Outside its tangential microsupport the separated-frequency remainder belongs to every negative compressed order. Its full normal commutator has precisely the same two types as (DB27), so it maps the original compact H1 input to H1. The low-frequency and proper kernel terms have these bounds as well. This proves (DB26) for the actual operators, rather than for their principal symbols alone.
Choose a fixed order-zero elliptic test on Ob and multiply it by the complete compressed order reducers of every integer order. Formula (DB4) and (DB26) prove every compressed H1 order throughout Ob, independently of the order. Equivalently no finite-order energy front meets Ob; its smaller closure misses the closure of their union. This is the smooth-front criterion of IP:A1 and the compressed regularity theorem.
B7. The original weak Dirichlet problem and both tangent germs. Start with the original smooth-coefficient finite matrix weak problem in V=H01, with real scalar principal symbol and all lower terms, including derivatives on the test function, and the actual natural-dual forcing. Suppose its smooth source front is absent on the relevant open compressed region. BPL supplies the actual boundary-preserving H1 representative U with PU=F∈L2; the representative has the same indicated energy front. NR:N8 removes the normal first-order coefficient by its full smooth matrix gauge, preserving the Dirichlet value.
Use the actual correction of LG:L7 and ECR:M7:
Z=r+QEe+F,W=U−Z.(DB28)
Then W is H1, PW satisfies (DB2) on one fixed parameter neighborhood, and its value trace is microlocally smooth. The correction is ordinarily regular near the characteristic set, and is regular in every original compressed H1 order on one fixed neighborhood. Hence an ordinarily regular incoming germ of the original solution gives the germ required for W. Apply B0–B6 to W. Adding Z, and then undoing the exact source representative and matrix gauge, proves absence of the original smooth Dirichlet energy front at the strict anchor. For the H01 norm the actual boundary value is zero: the domain-preserving compressed tests have boundary action on γU=0, so their H1 outputs belong to H01. A smooth nonzero trace of W alone is not used as a zero trace.
The other tangent germ follows without a selfadjointness assumption. Complex conjugation sends (u,f,P) to (u,f,P), with D changed to −D in the complete differential expression. Because the principal polynomial is quadratic, its value at the reversed full covector is unchanged. All lower matrices are conjugated with their correct derivative signs and remain in the admitted class. The outgoing positive-normal germ becomes a negative-normal germ at tangential covector −η∗. The actual Dirichlet domain and natural-dual equation conjugate together; for the functional use the conjugate of its value on the conjugate test. The just-proved assertion therefore applies to that germ as well.
Consequently, writing FD=WFbH01,∞(u) in the original source-regular region and q for a strict diffractive point,
q∈FD⟹π(exp(tHp)q)∈FD(∣t∣<ϵ),(DB29)
after the exact normal-form coordinate and nonzero parameter changes. For each punctured side, a regular point would contradict the corresponding germ theorem; the central point is the hypothesis. Shrink ϵ once so the whole arc stays in the source region. This supplies the strict diffractive singular-segment input for the Dirichlet domain. The argument concerns the Dirichlet domain. The Neumann/Robin boundary form, two-domain propagation and sharp Airy mapping require their respective arguments.
8. Three solved exercises
Exercise 1. A continuous hitting map with a square-root corner
Take p=ρ2−[xζ2+τ2−ζ2], coordinates (x,t,y;ρ,τ,ζ), and ζ=1. Put μ=1−τ2 and h=1/16. Compute the path between its incoming and outgoing hits of x=h, allowing a reflection when μ<0.
Solution. Hamilton's equations give ρ˙=1, x˙=2ρ, t˙=−2τ, and y˙=2(1−x). With ρ as parameter,
x=μ+ρ2,t=tc−2τρ,y=yc+2(1−μ)ρ−32ρ3.(DB30)
For μ≥0, the physical path runs from ρ=−a to a, a=h−μ. For μ<0, put b=−μ: the two physical pieces are [−a,−b] and [b,a], with the base coordinates continued continuously across reflection and the normal covector jumping from −b to b. The reflection is not an ordinary Hamilton interval. Set b=0 when μ≥0. The complete tangential increments are
Δt=−4τ(a−b),Δy=4(1−μ)(a−b)−34(a3−b3).(DB31)
Both are continuous at zero because b→0, although the derivative of the square-root term from the negative side diverges. This is the continuity used in B1. At μ=0, the minimum is the boundary tangency; at μ>0 it is an interior turn. Every value used in the figure has ∣μ∣≤1/64<h.
Exercise 2. A finite error is enough for a tangential gain
In B2 let s=9/4. Starting only with H(2,−1), list the indices obtained from the exact identity and identify the final X order.
Solution. The data term has order (2,s−1)=(2,5/4). The left error gains one ordinary order and hence one tangential order while keeping the ordinary index two. The successive tangential indices are
−1,0,1,5/4.(DB32)
Thus three uses of the same identity give H(2,5/4)⊂X13/4. The third use is an embedding of the error's available index two into the requested index 5/4, not an assumption of a fractional symbolic expansion. This stronger elliptic gain contains the X11/4 order needed by the global half-step.
Exercise 3. Every finite order at a point is insufficient
Construct an L2 function which belongs to Hm on some neighborhood of zero for every fixed integer m, but is not smooth on any neighborhood of zero.
Solution. Let xn=2−n, rn=2−n−3, n≥1, and choose a nonnegative smooth cutoff ψ, supported in (−1,1) and equal to one near zero. The intervals (xn−rn,xn+rn) are pairwise disjoint. Put
fn(x)=ψ((x−xn)/rn)∣x−xn∣n+1/2,an=1+max0≤j≤n∥Djfn∥22−n,v=n≥1∑anfn.(DB33)
For j≤n, the local power after differentiation is at least 1/2, so the indicated derivatives are L2. The cutoff derivatives are supported away from the center and are smooth. Hence an>0, and the series converges in L2 with summable norms. For fixed m, its tail n≥m converges in Hm, since every derivative norm through m is bounded by 2−n. Choose a neighborhood of zero excluding the finitely many earlier supports; on it v equals that tail. This proves the finite-order claim, including distributional differentiation by convergence.
Near xn, all other summands vanish and v=an∣x−xn∣n+1/2. Its derivative of order n+1 is a nonzero multiple of a one-sided power ∣x−xn∣−1/2, so it is neither bounded nor locally L2. Thus v is not smooth in any neighborhood of zero, and it is not Hn+1 at xn. These points accumulate at zero. This is why the closure of the union of finite-order fronts cannot be replaced by their union, and why B5 proves the same-region assertion before using B6.
9. Exact geometry of the common region
F0. Coordinates and interpretation. The left panel plots x=μ+ρ2 for μ=−1/100,0,1/100, restricted to 0≤x≤1/16. Arrows follow increasing ρ, the positive Hamilton orientation in Exercise 1. The dotted boundary segment for μ<0 is the covector jump at reflection; it is not a base path or an ordinary Hamilton arc. On the positive time-frequency branch, the right panel plots the exact Δt in (DB31) for −1/64≤μ≤1/64. It shows continuity of the full cap displacement across tangency, with no claim of differentiability there. The omitted y-increment is explicitly retained in (DB31). The figure generator preserves the constants and formulas.