The Physical Cutoff Does Not Restore Homogenization: Phase-Dependent Burning in the Strain G-Equation

Michele Caprio

Source-linked AI summary

The Physical Cutoff Does Not Restore Homogenization: Phase-Dependent Burning in the Strain G-Equation

Michele Caprio

arXiv:2608.15337v1Aug 15, 2026math.APcs.LG

TL;DR

The paper asks whether the physical positive part strain G-equation has a phase-independent effective burning velocity in cellular flows. Using Hamiltonian comparison and control interpretations, it shows that microscopic phase information persists and prevents locally uniform homogenization under physical scaling.

Problem
Nonconvex, noncoercive strain Hamiltonians make it difficult to determine whether cellular flames possess a single effective large-time propagation speed.
Method
The proof sandwiches the Hamiltonian between comparators, interpreting the upper comparator as rectangular state-dependent uncertainty with dynamically selectable controls.
Results
Microscopic phase information persists linearly for every unit planar direction, with a propagation rate at least CA/log A and no locally uniformly convergent rescaled subsequence.
Takeaways & Limitations
The results disprove the expected universal effective burning velocity and shift attention toward structures that could restore phase-independent rates.
Takeaways & Limitations
The classification of geometric, dynamical, or communication structures that restore a phase-independent effective rate remains open.

Abstract

from arXiv · show

We disprove the expectation stated by Xin, Yu, and Ronney that the physical positive part strain $G$-equation should possess an effective burning velocity in cellular flows. For the standard cellular flow in dimension two $V_A(x_1,x_2)=A(-\sin x_1\cos x_2,\cos x_1\sin x_2)$, if $0<d<20/399$ and $\sqrt{1+4d^2}<Ad\le1+d/10$, then for every unit planar slope the periodic correction develops oscillations at least linearly in time. The solution remains bounded below on an explicit horizontal channel through $(π,0)$, while at $(π/2,0)$ it decreases at rate at least $CA/\log A$, with $C>0$ universal. The same conclusions hold for arbitrary continuous periodic perturbations of planar initial data. Under the physical scaling $V_A(x/\varepsilon)$ and $d_\varepsilon=\varepsilon d$, an order one value gap persists between points at distance $O(\varepsilon)$ at every positive macroscopic time, so the rescaled solutions have no locally uniformly convergent subsequence. The proof uses the Hamiltonian sandwich $H_{\mathrm{unc}}\le H_+\le\widehat H$. The upper comparator $\widehat H$ is a rectangular support function, equivalently an upper expectation over a state-dependent credal set, whose reversed control dynamics possess an invariant comparison channel. We also prove that for any $C^2$ incompressible periodic flow, every $\varepsilon$-outward barrier certificate has covering radius at most $2d\varepsilon$ for all sufficiently small $\varepsilon$. We further discuss implications for statistics and machine learning: rectangular, time-consistent local uncertainty need not imply forgetting of the initial state in the long run, so additional global stability or ergodicity conditions are needed in robust sequential decision making. Two Lean 4 appendices record conditional formalizations of a sufficient $p=e_1$ subregime and of the logical assembly of the rigidity theorem for barrier certificates.

1. Introduction

The physical strain G-equation truncates strain-corrected burning at zero, creating a noncoercive and direction-dependent Hamiltonian. In standard cellular flows, this cutoff does not restore a single effective burning velocity: periodic corrections grow in oscillation, and order-one gaps persist under physical rescaling.

Model formulation: The physical strain G-equation replaces negative strain-corrected burning speeds by zero, while transport by the surrounding flow can still move the flame front.The positive-part cutoff suppresses burning under strong compression without permitting reversal.
Hamiltonian structure: Strong compression makes the Hamiltonian noncoercive because the positive-part cutoff can prevent it from tending to +∞ as |q| grows.When burning vanishes in a direction, transport remains and has opposite signs in opposite directions, making one direction nonpositive.
Hamiltonian structure: The Hamiltonian is also sharply direction-dependent because strain changes with q/|q|, so its value at an intermediate direction need not obey an averaging bound.The same flow can produce normal burning in some directions and complete suppression in others.
Main result: For the standard two-dimensional cellular flow, the authors disprove the expected existence of an effective burning velocity for every unit planar direction under the stated parameter regime.The result directly addresses Xin, Yu, and Ronney’s expectation for cellular flows and their question concerning incompressible periodic flows.
Main result: An order-one value gap persists between points at distance O(ε) after physical small-scale rescaling, while the same phase separation survives arbitrary continuous periodic perturbations of planar initial data.The periodic correction’s oscillation is measured across one 2π×2π cell, and the slow estimate holds on an explicit channel through (π,0).

2. Main Theorems: Overview

The paper constructs a cellular-flow counterexample in which the physical positive-part strain G-equation retains phase-dependent propagation and fails to homogenize. A separate rigidity theorem shows that sufficiently accurate outward barrier certificates must cover nearly the entire periodic domain.

Cellular-flow counterexample: The same phase separation persists for arbitrary continuous periodic perturbations of planar initial data and produces no locally uniformly convergent subsequence under the physical scaling.At every positive macroscopic time, an order-one value gap remains between points separated by O(epsilon), so the rescaled physical strain equation does not homogenize to a deterministic first-order Hamilton-Jacobi equation.
Barrier-certificate rigidity: For any C^2 incompressible periodic flow, every sufficiently accurate epsilon-outward barrier certificate has covering radius at most 2d epsilon.The bound depends on d, L, and the C^2 norm of the flow; exact outward certificates force D to equal the whole torus, and increasingly accurate certificates have vanishing complement radius.
Comparison mechanism: The upper Hamiltonian comparator is a rectangular support function, equivalently an upper expectation over state-dependent credal sets with independently selectable horizontal and vertical corrections.This correspondence gives the counterexample simultaneous Hamilton-Jacobi, robust-control, and imprecise-probability interpretations.
Implications: Rectangular, time-consistent local uncertainty can preserve dependence on the initial state, so robust sequential procedures require additional global stability or ergodicity conditions.The results exhibit a robust trap alongside positive-rate propagation despite compact convex local credal sets and a valid dynamic programming principle.

3. Related Literature

The related literature spans combustion G-equations, Hamilton-Jacobi homogenization, noncoercive Hamiltonians, robust control, and imprecise probability. It situates this work’s counterexample within prior homogenization results and connects its auxiliary model to rectangular local uncertainty and barrier-certificate geometry.

Combustion and G-equations: The G-equation literature established its combustion origins, level-set framework, and effective burning-velocity problem for physical models.Williams formally introduced the G-equation, Markstein presented an earlier form, Osher and Sethian systematized the level-set methodology, and Xin, Yu, and Ronney surveyed the field.
Hamilton-Jacobi homogenization: Periodic homogenization is established for inviscid equations in incompressible flows, with cellular-flow enhancement scaling as A/log A.Quantitative behavior depends on flow geometry; shear and three-dimensional flows exhibit different mechanisms.
Strain and curvature corrections: Prior strain and curvature studies identify thresholds, coexisting fast and stagnant regions, trapping, and bifurcations, showing that physical cutoffs are not universally homogenizing.The uncut strain equation has three intensity regimes, while physical curvature equations exhibit both effective burning velocities and homogenization–nonhomogenization bifurcations.
Noncoercive Hamiltonians: Noncoercive and nonconvex Hamiltonians can retain position-dependent long-time behavior, especially when geometric, dynamical, or controllability conditions fail.The strain Hamiltonian is positively homogeneous, direction-dependent, nonconvex, and potentially degenerate in burning despite large drift.
Robust control and imprecise probability: The auxiliary Hamiltonian is exactly an upper expectation over local convex compact credal sets, yet dynamically rectangular uncertainty need not make robust values forget their initial state.The construction uses a support-function upper bound and relates to first-order sublinear expectations, while remaining distinct from Peng’s second-order G-expectation framework.
Barrier-certificate geometry: Theorem 2.1 concerns asymptotic state dependence, whereas Theorem 2.5 concerns outward certificates that fill the torus and become dense as accuracy increases.This separates long-run state dependence from the geometry of exact and increasingly accurate outward barrier certificates.

4. Setting and the Hamiltonian Sandwich

Section 4 sets the proof on the 2π-periodic torus, establishes regularity and comparison for the uncut and physical-cutoff Hamiltonians, and derives phase separation from a Hamiltonian sandwich. This separation rules out a phase-independent long-time rate and therefore an effective burning velocity.

Setting: The main proof is formulated on the 2π-periodic torus T2, with viscosity solutions written as planar data plus periodic corrections.For slope p, Gi(x,t)=p·x+ui(x,t), and periodic comparison applies to ui.
Hamiltonian regularity: Hunc and H+ are continuous, periodic in x, positively homogeneous in q, and globally Lipschitz in q uniformly in x.These properties ensure both Hamiltonians satisfy the hypotheses of the viscosity-solution comparison theorem.
Hamiltonian sandwich: Hamiltonian order reverses at the solution level: if H1≤H2, the corresponding viscosity solutions satisfy G2≤G1 under common planar initial data.The result follows by treating the G2 solution as a viscosity subsolution of the H1 equation and applying periodic comparison after subtracting p·x.
Quantitative phase separation: A quantitative Hamiltonian sandwich yields phase separation and excludes a phase-independent long-time rate for the G-equation.The proposition’s oscillation estimate contradicts osc up(·,t)/t→0, which would be necessary for a phase-independent effective rate.

5. The Fast Point From the Uncut Equation

This section transfers Xin–Yu’s fast-point estimate from the uncut strain equation to the physical cutoff model. For every unit planar slope, the cutoff preserves the same universal-constant timescale t ≥ C A log A, because comparison can only lower the level-set function.

Uncut fast point: Theorem 5.1 supplies a universal constant C > 0 for the uncut cellular-flow strain equation with unit planar initial slope.The paper uses Xin–Yu’s estimate in its own normalization, without spatial or temporal rescaling.
Uncut fast point: t ≥ C A log A is the timescale at which the Xin–Yu fast-point estimate applies.Under the stated hypotheses, the same universal constant C is valid.
Cutoff comparison: For every unit vector p ∈ R2, Proposition 5.2 shows that the physical cutoff preserves the fast-point estimate under Theorem 2.1’s hypotheses.The proof applies the uncut estimate through the comparison relation and divides by t > 0.
Physical meaning: Where the uncut local burning speed is negative, the physical cutoff replaces it by zero, preventing reversal and inheriting fast forward propagation.The comparison shows that the cutoff can only lower the level-set function.

6. A Credal Upper Envelope

This section constructs a convex rectangular majorant of the physical cutoff Hamiltonian and identifies it exactly as a credal upper expectation over state-dependent velocity sets. Its reversed control representation supplies the comparison-channel mechanism used to obtain lower bounds.

Hamiltonian envelope: The rectangular majorant b H satisfies H_unc ≤ H_+ ≤ b H, and its associated solution b G_p lies below G_p for every planar slope p.The majorant is continuous, periodic, positively homogeneous, convex, and globally Lipschitz in q, uniformly in x.
Credal interpretation: The state-dependent set K(x) is a translated compact convex rectangle whose support function equals b H(x,q).This rectangular support function replaces the direction-coupled burning term with a pointwise upper bound.
Credal interpretation: b H is exactly the upper expectation of v·q over probability laws supported on K(x), forming a local credal-set representation.The representation is exact even though the rectangular construction provides an upper bound on the original physical Hamiltonian.
Control representation: The viscosity solution for b H admits a control representation with reversed drift, reflecting backward characteristics evaluated at a fixed spatial point.The representation also applies to planar initial data plus continuous periodic perturbations.
Comparison channel: A comparison channel remains invariant when the rectangular control dynamics have vanishing vertical component on the channel and inward-pointing horizontal components at its endpoints.Under these conditions, every trajectory starting in the channel remains there, enabling the control-based comparison.

7. The Cellular Comparison Channel

The section constructs a horizontal comparison channel D_μ around (π,0), verifies its normal and endpoint conditions, and applies Proposition 6.4 to obtain whole-channel estimates. In particular, H_+ remains uniformly bounded below there by πp_1−r_μ|p_1| for all times.

Channel construction: D_μ=[π−r_μ,π+r_μ]×{0} with r_μ∈(0,π/2) provides the comparison channel around (π,0).The lower bound in (6) implies μ>1, yielding the stated range for r_μ.
Channel construction: On D_μ, the coefficients satisfy a_2=(1−μcos z)+=0 and a_1=1+μcos z, while V_A,2(x_1,0)=0.These identities establish the normal conditions throughout the channel.
Endpoint conditions: At the channel endpoints, a_1(π±r_μ,0)=2 and V_A,1 takes the opposite values ±A sin r_μ.Specifically, V_A,1(π+r_μ,0)=A sin r_μ and V_A,1(π−r_μ,0)=−A sin r_μ.
Comparison estimates: Applying Proposition 6.4 first with H=bH and then with H=H_+ yields the whole-channel estimates.The application uses H□=bH, V=V_A, b_1=a_1, b_2=a_2, x_0=π, and y_0=0.
Comparison estimates: For every x∈D_μ and t≥0, H_+(x,t)≥πp_1−r_μ|p_1|.This is the uniform lower bound on the comparison channel.

8. Completion of the Proof of Theorem 2.1

The section completes Theorem 2.1 and Corollary 2.2 by combining the whole-channel and fast estimates, proving phase-dependent oscillation growth and ruling out a phase-independent effective burning velocity. It also clarifies that the slow estimate comes from a comparison channel for reversed majorant dynamics, not an exact physical outward barrier.

Proof of Theorem 2.1: Theorem 2.1 follows by combining Corollary 7.1’s whole-channel estimate with Proposition 5.2’s fast estimate through Proposition 4.3.The substitution uses x_s = (π, 0), B = πp_1 − r_μ|p_1|, and c = CA/log A.
Proof of Theorem 2.1: Because the estimates imply osc u_p(·, t)/t does not tend to zero, no phase-independent effective burning velocity exists for any unit direction p.The slow hypothesis comes from Corollary 7.1 and the fast hypothesis from Theorem 5.1.
Proof of Corollary 2.2: Corollary 2.2 extends the slow and fast estimates to arbitrary continuous periodic perturbations using order preservation and invariance under addition of constants.At the two distinguished phases, the solution is bounded below by the planar-data difference plus m − M, preserving the lower bound in (10).
Comparison Channel versus Outward Barrier Certificate: The comparison segment D_μ is invariant only for reversed controlled dynamics of the majorant Ĥ, not for the physical Hamiltonian’s exact outward dynamics.Thus the slow estimate is generated by an upper comparison channel rather than an exact outward barrier certificate.

9. Rigidity of Outward Barrier Certificates

For every C^2 incompressible periodic flow in any dimension, a proper closed set satisfying the outward Hamiltonian inequality must be quantitatively dense in the torus. Specifically, every sufficiently small ε-outward barrier certificate has covering radius at most 2dε.

Rigidity theorem: Every C^2 incompressible periodic flow, in every dimension, satisfies the rigidity result for closed sets obeying the outward Hamiltonian inequality in all proximal normal directions.A proper such set can exist only if it is quantitatively dense in the torus.
Proof mechanism: The same distance estimate ρ(t) ≤ 2dε holds for trajectories starting either outside the barrier set or within it, provided the initial distance is below r0.Scalar comparison and a first-exit argument extend the estimate across connected components of the positive-distance set.
Quantitative density: 2dε is the upper bound on the covering radius R(D) for every sufficiently small ε-outward barrier certificate.The proof concludes R(D) ≤ 2dε by contradiction using flow-preserved Lebesgue measure.

10. Consequences and Interpretation

The consequences distinguish physical nonnegativity from homogenization: the positive-part cutoff does not restore coercivity or prevent trapping. They also show that valid rectangular dynamic programming need not yield an initial-state-independent long-run rate, while outward barrier certificates are quantitatively dense.

Scaling Consequences: A locally uniformly convergent subsequence would have a continuous limit, forcing the phase difference in (13) to vanish.This contradiction establishes Corollary 2.3.
Cutoff versus Coercivity: The positive-part cutoff enforces nonnegative local burning but does not restore coercivity or exclude trapping in auxiliary control dynamics.It prevents reversal of the flame’s normal burning motion without forcing homogenization.
Comparison Trapping versus Outward Barrier Certificates: The reversed comparison dynamics can trap relevant backward trajectories even though no proper exact outward barrier certificate exists for the physical equation.Theorem 2.5 states that exact certificates fill the torus and approximate certificates become quantitatively dense.
Time Consistency versus Ergodicity: Time consistency and dynamic programming do not force the long-run value to become independent of the initial state.The credal construction has a dynamically rectangular control representation, but rectangularity alone does not produce a single state-independent asymptotic rate.

11. Conclusion and Further Questions · A. Background, Conventions, and Standard Tools

The paper disproves phase-independent homogenization for the physical positive-part strain G-equation in a cellular flow and shows that microscopic phase information persists under physical scaling. It closes by replacing universal-existence claims with classification questions about geometric, dynamical, communication, and ergodic mechanisms, while recording conventions and standard tools for the proof.

11. Conclusion and Further Questions: The standard smooth two-dimensional incompressible cellular flow retains microscopic phase information at a linear rate for every unit planar direction.This disproves the expectation associated with Question 11 of Xin, Yu, and Ronney in the stated parameter regime.
11. Conclusion and Further Questions: CA/log A is a lower bound for propagation at the fixed phase xf = (π/2, 0), while the solution remains bounded below on the comparison channel Dμ.The same phase-dependent behavior persists for arbitrary continuous periodic perturbations of planar initial data.
11. Conclusion and Further Questions: An order one value gap persists between points at distance πε/2 at every positive macroscopic time under V_A(x/ε) and dε = εd.Consequently, the oscillatory solutions have no locally uniformly convergent subsequence, a stronger obstruction than failure of a cell problem constant.
11. Conclusion and Further Questions: The proof sandwiches the physical Hamiltonian between the uncut equation and a cutoff-adapted support-function majorant.The majorant has inward-pointing endpoint velocities on a horizontal channel and is the upper expectation generated by a credal set supported on a rectangular velocity set.
11. Conclusion and Further Questions: 2dε bounds the covering radius of every ε-outward barrier certificate for sufficiently small ε in any C2 incompressible periodic flow.Every exact certificate therefore fills the torus, so the comparison trapping mechanism cannot be identified with an exact certificate of this type for the physical Hamiltonian.
11. Conclusion and Further Questions: The conclusions shift the agenda from universal existence to classifying conditions that restore a phase-independent effective rate.Open questions concern homogenization, C2 perturbation stability, comparison-channel criteria, spatially averaged effective velocity, robust long-run values, and numerical recovery of phase-dependent rates.
A. Background, Conventions, and Standard Tools: The background appendix fixes sign conventions and records standard viscosity-solution and credal-set facts used throughout the argument.It is intended to make the paper readable without reconstructing conventions or translating between proof languages, rather than to survey the underlying fields.

A.1. Flat Tori, Lifts, and Planar Data … A.7. Notation at a Glance

The appendices establish the periodic viscosity-solution framework, comparison order, support-function and credal interpretations, deterministic control representation, trapping lemma, and geometric ingredients for incompressibility arguments. They conclude with notation linking these constructions to the paper’s Hamiltonians, level-set solutions, and barrier quantities.

A.1. Flat Tori, Lifts, and Planar Data: Planar-slope solutions reduce to a periodic problem on a compact torus, enabling the paper’s comparison arguments.The reduction uses u_t + H(x, p + Du) = 0 with periodic initial data.
A.2. Viscosity Solutions, Comparison, and Hamiltonian Order: Theorem A.1 gives unique continuous viscosity solutions and semigroup properties under continuity, uniform global Lipschitz, and spatial-modulus assumptions, without coercivity or convexity.The theorem applies to every planar slope and continuous periodic initial datum.
A.2. Viscosity Solutions, Comparison, and Hamiltonian Order: Hamiltonian order reverses at the solution level: a majorant supplies a lower bound, while a minorant supplies an upper bound for the same data.This sign convention underlies the sandwiching of level-set solutions.
A.3. Support Functions and Credal Upper Expectations: A support function equals an upper expectation over the associated weakly compact credal set, and the paper’s rectangular majorant is the support function bH(x,q).The majorant has the form AV0(x)·q + a1(x)|q1| + a2(x)|q2|.
A.4. Rectangularity and Deterministic Dynamic Programming: Rectangular controls permit independent coordinate choices and deterministic-time concatenation, making the associated dynamic programming recursion time consistent.The backward characteristic convention forces a minus sign in the controlled drift.
A.5. A Controlled First Exit Lemma: Every Carathéodory trajectory under measurable controls remains in the invariant segment when endpoint vector fields point inward with uniform strictness.The proof uses uniqueness on the axis and a first-exit contradiction.
A.6. Proximal Normals, Distance Derivatives, and Incompressibility: Distance from a closed set has an upper derivative bounded by velocity projected onto a proximal outward normal; incompressibility preserves volume and makes tubular volumes strictly increase.These facts provide the geometric inputs for the no-barrier argument.
A.7. Notation at a Glance: The notation summary identifies the strain parameters, uncut and cutoff Hamiltonians, rectangular velocity sets, credal expectations, oscillation, covering radius, proximal normals, and flow maps.It distinguishes the scalar field Φ(x) from the fluid flow map Φ_t.

B. Control Representation for the Credal Envelope · C. A Conditional Lean 4 Formalization of a Sufficient 𝑝= 𝑒1 Subregime

Section B establishes the credal-envelope control representation: controlled trajectories are globally well posed, the value function satisfies dynamic programming and the viscosity Hamilton–Jacobi equation, and its planar-periodic structure is preserved. Section C gives a deliberately restricted Lean 4 assembly for the p=e1 subregime, with analytic inputs supplied explicitly as theorem parameters rather than global axioms.

B. Control Representation for the Credal Envelope: Boundedness and uniform global Lipschitz continuity of the controlled vector field yield a unique global Carathéodory trajectory for every measurable control and initial state.The trajectory is denoted X_x,η.
B. Control Representation for the Credal Envelope: For planar initial data g(x)=p·x+u0(x) with continuous periodic u0, uniform trajectory estimates make the control value function W_g continuous.The argument uses uniform continuity and linear growth of g, together with a common modulus of continuity on bounded time intervals.
B. Control Representation for the Credal Envelope: Concatenating measurable controls and using ε-optimal controls establishes the dynamic programming identity for W_g.Uniqueness of controlled trajectories supplies the concatenation argument.
B. Control Representation for the Credal Envelope: W_g is a viscosity solution of (W_g)_t + b H(x,DW_g)=0 with initial data g, where the control supremum produces the Hamiltonian b H.The proof establishes both subsolution and supersolution properties, including the compactness limit for short-time controls.
B. Control Representation for the Credal Envelope: Periodicity of the controlled vector field implies that W_g(x,t)−p·x is periodic, identifying W_g with the viscosity solution in the planar periodic class.Taking u0=0 yields the corresponding planar representation used in the paper.
C. A Conditional Lean 4 Formalization of a Sufficient p=e1 Subregime: The Lean formalization assumes 0<d<1/60 and 1+6d^2≤Ad≤1+d/10, deriving the lower inequality in the restricted p=e1 subregime.It is presented as a genuine but deliberately restricted special case of the strengthened analytic result.
C.1. Explicit Hypotheses of the Conditional Formalization: The conditional theorem takes viscosity-solution, Hamiltonian-order, fast-point, control-envelope, and trapping statements as explicit hypotheses, including hComparison, hXinYu, hControl, and hTrap.No analytic input is introduced globally; all four assumptions are ordinary theorem parameters.
C.2. Lean Source: The Lean source assembles the explicit analytic inputs into the restricted conclusion, proving a slow-point lower bound and transferring the fast-point rate estimate to the physical cutoff.The displayed derivation obtains Ghat and Gcut slow-point bounds and a fast-point lower rate C·A/log A.

D. A Conditional Lean 4 Formalization of the Quantitative No Barrier Theorem

The appendix gives a conditional Lean 4 formalization of the quantitative no-barrier theorem, treating analytic and geometric inputs as explicit parameters. From these hypotheses, it constructs a positive ε0, proves R(D) ≤ 2dε, and derives that exact barriers equal the whole torus.

D.1. Abstract Data and Explicit Hypotheses: All analytic inputs are ordinary parameters of the final theorem, with no globally introduced assumption.The Lean assembly uses no sorry, admit, proof hole, or globally declared axiom.
D.1. Abstract Data and Explicit Hypotheses: The theorem is parameterized by abstract points, directions, Hamiltonian, vector field, flow, distance, covering radius, volume, and predicates for the relevant geometric conditions.The inputs represent objects on the flat torus and include closedness, C2 regularity, incompressibility, physical Hamiltonian structure, and unit proximal outward normals.
D.1. Abstract Data and Explicit Hypotheses: The formalization makes local drift, distance contraction, volume preservation, tube-limit continuity, and tubular geometry explicit assumptions.These assumptions encode the analytic and geometric ingredients required by the contradiction argument.
D.2. Logical Assembly: A positive admissible ε0 is constructed so that 2dε < r0 whenever 0 ≤ ε ≤ ε0.The proof begins by choosing ε0 from the positivity of r0 and d.
D.2. Logical Assembly: R(D) ≤ 2dε follows by contradiction: contraction and volume preservation imply a tube-volume upper bound that conflicts with strict tubular growth.The argument uses Φ_t(D_r) ⊆ D_{r_t}, the tube-limit estimate, and the strict inequality |D_{2dε}| < |D_r|.
D.2. Logical Assembly: At ε = 0, the quantitative estimate gives R(D) ≤ 0, and the zero-radius tubular condition yields D = T^n for exact barriers.This is the formalized rigidity conclusion.
D.3. Lean Source: The Lean source defines the abstract predicates and proves the contradiction between contracted tube volume and strict volume growth.The source includes the contraction estimate and the two opposing volume inequalities used in the proof.
D.3. Lean Source: The source derives both the quantitative covering-radius bound and the exact whole-space conclusion from the stated hypotheses.The final declarations invoke the quantitative theorem at ε and at ε = 0.