PaperlayerView exact revision on arXiv

Source-linked AI summary

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

Michele Caprio

arXiv:2608.15337v1math.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 a Hamiltonian comparison argument, it shows that microscopic phase information persists at linear rate, preventing locally uniform homogenization under physical scaling.

  • Problem

    Determining a single effective propagation speed is difficult because strain makes the Hamiltonian direction-dependent, generally nonconvex, and potentially noncoercive.

    Source: §1 · pp. 4–5

  • Method

    The proof sandwiches the physical Hamiltonian between comparators and interprets the upper comparator as a rectangular, state-dependent credal-set control problem with an invariant comparison channel.

    Source: §2.1 · p. 13

  • Results

    Microscopic phase information persists linearly for every unit planar direction, while physical scaling leaves an order-one gap across O(ε) distances and eliminates locally uniform subsequential convergence.

    Source: §1 · p. 7, §11 · p. 34

  • Takeaways & Limitations

    The results shift the agenda from universal effective-rate existence toward classifying geometric, dynamical, or communication structures that restore phase-independent rates.

    Source: §11 · p. 35

    Several questions about which structures restore a phase-independent effective rate remain open.

    Source: §11 · p. 35

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 paper introduces the physical strain G-equation, whose cutoff prevents backward burning but leaves a generally noncoercive and nonconvex Hamiltonian. It disproves effective burning-velocity homogenization for a standard cellular flow and establishes phase separation, rescaled noncompactness, and barrier-certificate rigidity.

1. Introduction

  • The physical positive-part cutoff suppresses burning under strong compression without permitting reversal, while gas transport can still move the flame.The model combines normal burning modified by strain with advection by the surrounding flow.Source: §1 · p. 4, Figure 1 · p. 5
  • The Hamiltonian is generally noncoercive and nonconvex because burning can vanish in compressed directions and depends sharply on gradient direction.These properties remove two central structures normally used to analyze large-scale Hamilton-Jacobi behavior.Source: §1 · pp. 4–5
  • For the standard two-dimensional cellular flow, Xin, Yu, and Ronney’s expected effective burning velocity is disproved: under the stated parameter regime, every planar direction develops linearly growing periodic phase separation.The periodic correction has a slow-decreasing region and a universal lower bound on its oscillation gap.Source: §1 · p. 7
  • The phase separation persists for arbitrary continuous periodic perturbations of planar initial data and, after physical small-scale rescaling, yields an order-one gap across O(ε) distances at every positive macroscopic time.This rules out locally uniform subsequential convergence of the rescaled solutions.Source: §1 · p. 7
  • The paper also proves that nearly outward-blocking regions in incompressible periodic flows must come close to every point within one flow period.This is the stated rigidity result for outward barrier certificates.Source: §1 · p. 7

1.1. Organization

  • The paper’s organization separates the phase-separation and stability proofs, barrier-certificate rigidity, small-scale noncompactness, control representation, and conditional Lean 4 formalizations.Sections 4–8 treat microscopic phase separation, Section 9 treats rigidity, Section 10 treats noncompactness, and Appendices B–D provide representation and formalization results.Source: §1.1 · p. 7

2. Main Theorems: Overview

The main theorems establish phase-dependent propagation and failure of homogenization in a cellular-flow strain equation, together with global rigidity bounds for approximate outward barrier certificates. Their proofs combine Hamiltonian comparisons, trapped-channel constructions, and incompressibility-based distance contraction, while the applications highlight the need for additional stability or ergodicity conditions under rectangular, time-consistent uncertainty.

2. Main Theorems: Overview

  • The phase-separation estimates remain valid for arbitrary continuous periodic perturbations of planar initial data.This stability follows from the same comparison argument used for the planar initial condition.Source: §2 · p. 9, §2.1 · p. 15
  • Under physical scaling, an order-one separation persists at vanishing spatial scales, so no subsequence converges locally uniformly and the equation does not homogenize to a deterministic first-order Hamilton-Jacobi equation.The same nonhomogenization conclusion holds for every unit planar slope.Source: §2 · pp. 9–10

2.2. The Proof of Theorem 2.5 in Three Moves

  • For incompressible periodic flows, every sufficiently accurate ε-outward barrier certificate has covering radius at most 2dε, and every exact certificate is the whole torus.The proof begins by showing that points farther than 2dε from the certificate move closer under the forward fluid flow, causing distance contraction.Source: §2 · p. 11, §2.2 · p. 16

2. Main Theorems: Overview

  • As ε_j decreases to zero, approximate outward certificates become asymptotically dense and cannot retain a complement of uniformly positive macroscopic size.This is the stated asymptotic-density corollary of the barrier rigidity theorem.Source: §2 · p. 11

2.1. The Proof of Theorem 2.1 in Four Moves

  • The cellular proof sandwiches the physical Hamiltonian between the uncut model and a convex rectangular support-function majorant whose reversed control dynamics trap trajectories in a horizontal channel.The majorant is also an upper expectation over a dynamically rectangular, state-dependent credal set, making the comparison interpretable through robust control and imprecise probability.Source: §2.1 · pp. 12–15

2. Main Theorems: Overview

  • The physical cutoff still permits phase-dependent propagation, with periodic-correction oscillations growing at least as C A/log A and no phase-independent effective burning velocity.The result combines a fast-propagating phase inherited through comparison with a stagnation phase controlled by an auxiliary upper Hamiltonian.Source: §2.1 · p. 15

2.2. The Proof of Theorem 2.5 in Three Moves

  • The flow carries the whole r-neighborhood of D into successively smaller neighborhoods approaching the 2dε error scale, while incompressibility preserves Lebesgue measure, yielding R(D) ≤ 2dε.When ε = 0, every point of the torus has distance zero from D, so D = T^n.Source: §2.2 · pp. 16–17

2.3. Relevance to Machine Learning and Statistics

  • Rectangular ambiguity supports time-consistent Bellman recursion, yet long-horizon values can remember their starting state through robust traps and positive-rate propagation [23, 28, 37].Thus valid dynamic programming does not imply a universal average reward or state-independent long-run behavior [33, Chapters 8-9].Source: §2.3 · p. 17
  • Plausible-law or credal-set construction does not ensure asymptotic forgetting; robust procedures require separate mixing, ergodicity, or global-stability mechanisms.The counterexample has well-behaved local uncertainty and dynamic programming but lacks a state-independent long-run rate.Source: §2.3 · pp. 17–18
  • The barrier theorem limits precise outward certificates to near-global coverage, while leaving other global invariance or blocking mechanisms possible.A uniform estimation error transfers directly into geometric coverage error, but probabilistic bounds require additional sampling assumptions.Source: §2.3 · p. 18

3. Related Literature

The paper situates its counterexample across combustion, Hamilton–Jacobi homogenization, robust control, and imprecise probability. It extends prior results by showing that physical strain cutoffs can preserve phase dependence and that locally rectangular uncertainty need not erase initial-state effects.

3. Related Literature

  • The literature review spans combustion, Hamilton–Jacobi homogenization, robust control, and imprecise probability as the paper’s methodological foundations.Source: §3 · p. 18

3.1. 𝐺-equations, Flame Stretch, and Effective Speeds

  • Prior 𝐺-equation studies established homogenization and effective-speed theory, while uncut strain results identified intermediate nonhomogenization that the present work proves persists under the positive-part correction.The review also notes cellular-flow enhancement at the A/log A scale and the physical curvature equation’s effective burning velocity results.Source: §3.1 · p. 19

3.2. Noncoercive and Nonconvex Hamilton-Jacobi Homogenization

  • Noncoercive and nonconvex homogenization precedents show that microscopic information or position-dependent long-time behavior can survive, while this paper attributes the effect to directional degeneracy and persistent trapping.The strain Hamiltonian is positively homogeneous, direction-dependent, and nonconvex, with burning vanishing in some directions despite large drift.Source: §3.2 · pp. 19–20

3.3. Differential Games, Robust Control, and Hamiltonian Comparisons

  • The comparison method upper-bounds the physical Hamiltonian by a rectangular velocity-set support function to obtain a lower solution bound, while the uncut Hamiltonian supplies the complementary upper bound.The counterexample requires both comparison directions simultaneously.Source: §3.3 · p. 20

3.4. Imprecise Probability, Credal Dynamics, and Robust Learning

  • The auxiliary Hamiltonian is exactly an upper expectation over local convex compact credal sets, yet dynamic rectangularity does not ensure that long-run robust values forget their initial states.The connection to Peng’s framework is exact only for first-order local sublinear expectations and the convex majorant, not the generally nonconvex physical Hamiltonian.Source: §3.4 · pp. 21–22
  • The review distinguishes the paper’s asymptotic state-dependence result in Theorem 2.1 from Theorem 2.5, which forces increasingly accurate outward barrier certificates to become dense.Source: §3.4 · p. 22

4. Setting and the Hamiltonian Sandwich

This section formalizes the cellular-flow setting and establishes the comparison framework for the uncut and physical-cutoff Hamiltonians. A Hamiltonian sandwich yields phase separation and rules out a phase-independent long-time rate, hence an effective burning velocity.

4.1. The Cellular Flow

  • The proof works on the 2π-periodic torus and establishes that the uncut and cutoff Hamiltonians are continuous, periodic, positively homogeneous, and uniformly globally Lipschitz in q.These properties ensure both Hamiltonians satisfy the hypotheses of Theorem A.1.Source: §4.1 · p. 22

4.2. Comparison for Planar Data

  • For common planar initial data p·x, periodic viscosity comparison applies after writing each solution as p·x plus a periodic correction.The order-reversal lemma converts Hamiltonian inequalities into corresponding solution inequalities.Source: §4.2 · p. 23
  • The quantitative phase-separation proposition shows that a Hamiltonian sandwich forces persistent oscillation in the periodic correction, excluding a phase-independent long-time rate and effective burning velocity.The second half of the sandwich is supplied by the credal majorant constructed in Section 6.Source: §4.2 · p. 24

5. The Fast Point From the Uncut Equation

This section imports Xin and Yu’s fast-point estimate for the uncut strain equation and shows that the physical cutoff preserves it. The comparison is made in the paper’s original normalization, with no spatial or temporal rescaling.

Fast point from the uncut equation

  • Xin and Yu’s uncut-equation theorem [40, Theorem 1.3(ii)] applies to planar initial data G_unc(x,0) = p·x with unit p at times t ≥ C A log A.The theorem is stated using the cellular flow, period, amplitude A, Markstein parameter d, and distinguished point x_f adopted here.Source: §5 · p. 25

Cutoff preserves the fast point

  • Under Theorem 2.1’s hypotheses, the cutoff preserves the fast-point estimate for every unit vector p once t ≥ C A log A.The universal constant C is the same as in the Xin–Yu estimate.Source: §5 · p. 25

Physical meaning of the comparison

  • The cutoff comparison shows that replacing negative strain-corrected burning speeds by zero prevents reversal while inheriting fast forward propagation from the uncut model.Because the cutoff can only lower the level-set function, the uncut fast-point estimate transfers to the physical equation.Source: §5 · p. 25

6. A Credal Upper Envelope

The section constructs a convex rectangular Hamiltonian that dominates the physical cutoff and supports the phase-separation lower bound. It identifies this majorant with an exact local credal upper expectation and represents it through reversed robust control dynamics with an invariant comparison channel.

6.1. A Coordinate Rectangular Envelope

  • For the cellular flow, the rectangular envelope bH is continuous, periodic, positively homogeneous, convex, and globally Lipschitz in q, with a spatial Lipschitz bound.The construction uses coordinate directions e_1 and e_2, with the mixed strain vanishing identically and H_+ ≤ bH.Source: §6.1 · pp. 26–27

6. A Credal Upper Envelope

  • The convex majorant bH satisfies H_unc ≤ H_+ ≤ bH, and its solution bG_p lies below G_p while supplying the channel lower bound.This sandwich is the central comparison used to transfer lower bounds from the rectangular envelope to the physical cutoff equation.Source: §6 · p. 26, §6.1 · p. 27

6.2. Upper Expectations and the Local Credal Set

  • The state-dependent rectangle K(x) yields an exact upper expectation of v·q over probability laws supported on K(x), while remaining a pointwise upper bound on the physical Hamiltonian.K(x) is the fluid velocity translated by coordinatewise intervals, making rectangularity explicit through its support function.Source: §6.2 · p. 27

6.3. Robust Control Representation

  • The viscosity solution for bH admits a robust-control representation using the reversed drift, which is essential because characteristics run backward when evaluating a fixed spatial point.The representation also extends to planar affine data plus continuous periodic perturbations through lifted-space dynamics and periodic viscosity uniqueness.Source: §6.3 · p. 28

6.4. A General Comparison Channel Criterion

  • Under the comparison-channel criterion, vanishing vertical dynamics and inward-pointing horizontal dynamics at the channel endpoints keep every reversed controlled trajectory inside the channel.The criterion applies to bounded, Lipschitz, periodic drift and control coefficients when the Hamiltonian is dominated by the rectangular support function.Source: §6.4 · pp. 28–29

7. The Cellular Comparison Channel

The section constructs a horizontal comparison channel D_μ around (π,0), where the cellular flow satisfies the required normal and endpoint conditions. Proposition 6.4 then yields a uniform lower bound for the comparison solution throughout this channel.

Channel construction

  • The channel D_μ=[π−r_μ,π+r_μ]×{0} has r_μ∈(0,π/2) because the lower bound in (6) implies μ>1.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.Source: §7 · p. 29

Endpoint conditions

  • At the channel endpoints, a_1=2 and the horizontal flow components are V_A,1(π+r_μ,0)=A sin r_μ and V_A,1(π−r_μ,0)=−A sin r_μ.These endpoint identities provide the data used to verify the endpoint conditions required by the comparison proposition.Source: §7 · p. 29

Comparison estimates

  • Applying Proposition 6.4 first to H=bH and then to H=H+ yields the whole-channel comparison estimates.The application uses H□=bH, V=V_A, b_1=a_1, b_2=a_2, x_0=π, and y_0=0.Source: §7 · p. 29

Uniform lower bound

  • For every x∈D_μ and t≥0, the comparison solution satisfies u+(x,t)≥πp_1−r_μ|p_1|.This is the uniform lower bound stated in Corollary 7.1.Source: §7 · p. 30

8. Completion of the Proof of Theorem 2.1

Theorem 2.1 follows by combining the whole-channel and fast estimates, yielding linear phase oscillations and ruling out a phase-independent effective burning velocity in every unit direction. Corollary 2.2 extends the same bounds to continuous periodic perturbations, while Remark 8.1 distinguishes the comparison channel from an exact physical outward barrier certificate.

Proof of Theorem 2.1

  • Combining Corollary 7.1, Proposition 5.2, Proposition 4.3, and Theorem 5.1 gives the slow and fast bounds, so osc u_p(·,t)/t does not vanish for any unit direction p.The contradiction with vanishing normalized oscillation rules out a phase-independent effective burning velocity.Source: §8 · p. 30

Proof of Corollary 2.2

  • Order preservation and invariance under addition of constants transfer the slow and fast estimates from planar data to every continuous periodic perturbation.At the distinguished phases, the perturbed solution differs from the planar-data difference by at least m−M, preserving the lower bound after division by t.Source: §8 · p. 30

Remark 8.1 (Comparison Channel versus Outward Barrier Certificate)

  • The invariant segment D_μ belongs only to the reversed controlled dynamics of the majorant Ĥ, not to the physical Hamiltonian as an exact outward barrier certificate.Thus the slow estimate is produced by an upper comparison channel, with the quantitative distinction supplied by Theorem 2.5.Source: §8 · p. 30

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 sufficiently small ε-outward barrier certificate for a C^2 incompressible periodic flow satisfies the quantitative bound R(D) ≤ 2dε.The proof uses trajectory-distance comparison, flow preservation of Lebesgue measure, and a contradiction from any larger covering radius.Source: §9 · p. 32

10. Consequences and Interpretation

The consequences establish failure of the small-scale homogenization limit and a persistent linear phase gap witnessed by fixed physical points. They interpret this as evidence that cutoff, comparison trapping, and time consistency do not ensure coercivity, outward certificates, or ergodicity.

10.1. Failure of the small scale Homogenization Limit

  • No locally uniformly convergent subsequence exists under the physical small-scale rescaling, because continuity of any limit would contradict the persistent difference between nearby rescaled points.This proves Corollary 2.3.Source: §10.1 · p. 33

10.2. A fixed pair Linear Gap

  • The same two physical points exhibit a linear phase gap for every propagation direction, with growth rate at least CA/log A.For any 0 < c < CA/log A, the gap eventually exceeds ct.Source: §10.2 · p. 33

10.3. What the Counterexample Teaches

  • The positive-part cutoff prevents reversal of normal burning but does not restore coercivity or exclude trapping in the auxiliary control dynamics.Thus physical nonnegativity alone does not force homogenization.Source: §10.3 · p. 34
  • Comparison trapping remains compatible with certificate rigidity: the reversed comparison dynamics have an invariant channel, while exact outward certificates for H+ fill the torus and approximate ones become quantitatively dense.Therefore no proper exact certificate of this type exists for the original physical equation, without preventing nonhomogenization.Source: §10.3 · p. 34
  • A dynamically rectangular credal representation and valid dynamic programming principle do not ensure an initial-state-independent long-run value or asymptotic rate.Time consistency alone is therefore insufficient to produce ergodicity.Source: §10.3 · p. 34

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 an explicit cellular-flow regime, establishes persistent microscopic phase dependence, and identifies rigidity and open questions. An appendix records conventions and standard tools supporting the argument.

11. Conclusion and Further Questions

  • The authors disprove Xin, Yu, and Ronney’s expectation [41] for standard smooth two-dimensional incompressible cellular flow in an explicit parameter regime.Source: §11 · p. 34
  • For every unit planar direction, microscopic phase information persists linearly: the solution stays bounded below on D_μ, while x_f=(π/2,0) propagates at least at rate CA/log A.Source: §11 · p. 34
  • Under physical scaling, an order-one gap remains between points O(ε) apart at every positive macroscopic time, preventing locally uniform convergence and any cell-problem effective constant.Source: §11 · p. 34
  • A Hamiltonian sandwich combines the uncut fast-point estimate with a cutoff-adapted rectangular support-function majorant whose inward-pointing endpoint velocities trap a horizontal comparison channel.Source: §11 · pp. 34–35
  • The support-function majorant is also an upper expectation over a rectangular credal set, connecting phase-dependent trapping to imprecise probability and robust dynamic programming.Source: §11 · p. 35
  • For any C^2 incompressible periodic flow, every ε-outward barrier certificate has covering radius at most 2dε, so exact certificates fill the torus and cannot explain this trapping.Source: §11 · p. 35
  • The conclusion shifts attention toward classifying geometric, dynamical, communication, or ergodic conditions that restore phase-independent rates, while posing questions about perturbation stability, averaged velocities, and numerical recovery.Source: §11 · p. 35

A. Background, Conventions, and Standard Tools

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

The appendices establish the compact-torus formulation, viscosity comparison framework, control interpretations, and geometric lemmas supporting the paper’s main arguments. They also define the notation used for Hamiltonians, level-set solutions, credal sets, and barrier geometry.

A.1. Flat Tori, Lifts, and Planar Data

  • Periodic planar-slope problems reduce to a compact torus equation, enabling all comparison arguments to be carried out on a compact state space.A solution with slope p is represented through a periodic correction satisfying u_t + H(x, p + Du) = 0.Source: §A.1 · p. 36

A.2. Viscosity Solutions, Comparison, and Hamiltonian Order

  • Under continuity, uniform global Lipschitz dependence on q, and a spatial modulus condition, periodic Hamilton-Jacobi problems have unique continuous viscosity solutions and contraction semigroups without coercivity or convexity.Hamiltonian ordering reverses at the solution level: a majorant yields a lower bound, while a minorant yields an upper bound.Source: §A.2 · pp. 37–38

A.3. Support Functions and Credal Upper Expectations

  • Support functions are exactly equivalent to upper expectations over credal sets, and the paper’s rectangular majorant has the form b H(x,q) = A V0(x)·q + a1(x)|q1| + a2(x)|q2|.The equivalence follows because probability measures supported on a compact velocity set cannot exceed its support-function maximum, which a maximizing Dirac mass attains.Source: §A.3 · p. 38

A.4. Rectangularity and Deterministic Dynamic Programming

  • Rectangular controls select coordinatewise uncertainties independently and remain admissible under deterministic-time concatenation, producing time-consistent deterministic dynamic programming.The resulting backward characteristics use a forced minus sign in the drift, and the planar periodic class is handled in Appendix B.Source: §A.4 · pp. 38–39

A.5. A Controlled First Exit Lemma

  • If every admissible control points inward at both endpoints of a horizontal segment, every Carathéodory trajectory under measurable controls remains in that segment for all positive times.The proof combines uniqueness on the axis with uniform endpoint inequalities and a first-exit contradiction.Source: §A.5 · pp. 39–40

A.6. Proximal Normals, Distance Derivatives, and Incompressibility

  • Proximal-normal distance estimates and incompressibility provide the geometric inputs for ruling out barriers: divergence-free flows preserve volume, while tubular volumes strictly increase with radius.The upper derivative of distance is controlled by the velocity’s projection onto a proximal outward normal.Source: §A.6 · pp. 40–41

A.7. Notation at a Glance

  • The notation summary distinguishes the uncut, physical-cutoff, and convex-majorant Hamiltonians and solutions, rectangular velocity sets and credal expectations, oscillation, covering radius, proximal normals, and fluid flow maps.It also separates the cellular scalar field Φ(x) from the flow map Φ_t used in the no-barrier argument.Source: §A.7 · p. 41

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

The paper establishes a control representation for the credal envelope and conditionally formalizes a sufficient p=e1 phase-dependent-burning subregime in Lean 4. The formalization derives incompatible slow- and fast-point rate bounds from explicit analytic hypotheses rather than global axioms.

B. Control Representation for the Credal Envelope

  • The control representation gives a unique global controlled trajectory for every measurable control and identifies the value function as the viscosity solution of the envelope Hamilton-Jacobi equation.The construction also shows continuity and periodicity after subtracting the planar slope.Source: B. Control Representation for the… · pp. 42, 44
  • Dynamic programming follows by concatenating measurable controls, while compactness and affine control dependence establish the viscosity subsolution and supersolution properties.The argument uses uniqueness of controlled trajectories, ε-optimal controls, and compactness of the control set.Source: B. Control Representation for the… · pp. 42–43

C. A Conditional Lean 4 Formalization of a Sufficient 𝑝= 𝑒1 Subregime

  • The conditional Lean development restricts the parameter assumptions to 0<d<1/60 and 1+6d^2≤Ad≤1+d/10, making it a sufficient but narrower p=e1 subregime.It contains no sorry, admit, proof hole, or globally declared axiom.Source: C. A Conditional Lean 4 Formalization… · p. 44

C.1. Explicit Hypotheses of the Conditional Formalization

  • The formal theorem takes viscosity-solution predicates, Hamiltonian orderings, comparison, the Xin-Yu fast-point estimate, control representation, and trapping as ordinary explicit hypotheses.No analytic input is introduced globally; all four assumptions appear as theorem parameters.Source: §C.1 · p. 45

C.2. Lean Source

  • The Lean source defines asymptotic rate and convergence notions, proves elementary order and incompatibility lemmas, and assembles the analytic inputs into the restricted theorem.The incompatibility argument combines an eventual upper bound at the slow point with an eventual lower bound at the fast point.Source: §C.2 · pp. 45, 48, 49
  • Hamiltonian comparison transfers the fast-point estimate from the uncut solution to the cutoff solution, while the invariant trapping channel yields its slow-point lower bound.The trapping estimate keeps every relevant auxiliary trajectory at first coordinate at least π−3d, and comparison reverses solution ordering under Hamiltonian increase.Source: §C.1 · p. 45, §C.2 · pp. 50–51
  • Under explicit analytic inputs, the Lean theorem proves a positive slow-point bound, a fast-point rate lower bound C A/log A, and failure of any phase-independent long-run rate.The conclusion holds for 0<d<1/60 and 1+6d^2≤Ad≤1+d/10.Source: §C.2 · pp. 50–51

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

This appendix gives a conditional Lean 4 formalization of the quantitative no-barrier theorem. With analytic and geometric inputs supplied explicitly, it constructs a positive threshold, proves the covering-radius bound, and derives exact rigidity at zero error.

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

  • The conditional theorem assembles explicit analytic and geometric hypotheses into R(D) ≤ 2dε for sufficiently small ε and D = T_n when ε = 0.The development treats local drift, contraction, volume preservation, tube limits, and strict tubular growth as hypotheses, then derives both conclusions.Source: D. A Conditional Lean 4 Formalization… · p. 51, §D.2 · p. 53
  • The formalization is genuinely conditional: no sorry, admit, proof hole, or globally declared axiom is used, and unformalized inputs remain theorem parameters.This preserves the logical boundary between the formalized assembly and the analytic or geometric results it assumes.Source: D. A Conditional Lean 4 Formalization… · p. 52, §D.1 · p. 53

D.1. Abstract Data and Explicit Hypotheses

  • The abstract theorem parameterizes points, directions, Hamiltonian, vector field, flow, distance, covering radius, volume, and predicates for regularity, incompressibility, physicality, and barrier normals.The structural assumptions hC2, hDiv, and hPhysical encode the vector field’s C2 regularity, divergence-free property, and physical strain Hamiltonian relation.Source: §D.1 · p. 52
  • Its explicit assumptions package local drift, exponential tube contraction, flow-volume preservation, continuity from above, and strict tubular growth with zero-radius rigidity.Together these assumptions provide the local, dynamical, measure-theoretic, and geometric ingredients required by the contradiction argument.Source: §D.1 · p. 52

D.2. Logical Assembly

  • The logical assembly assumes a radius larger than 2dε, contracts its tube under the flow, uses volume preservation and tube limits, and contradicts strict tubular growth.This contradiction establishes R(D) ≤ 2dε; setting ε = 0 gives radius zero and therefore D = T_n.Source: §D.2 · p. 53

D.3. Lean Source

  • The reproduced Lean source defines the abstract predicates and proves the final theorem with ε0 = r0/(4d), yielding R(D) ≤ 2dε and D = Set.univ at ε = 0.The source explicitly derives volume preservation from incompressibility, applies the covering-radius lemma, and invokes zero-radius geometry for exact rigidity.Source: §D.3 · pp. 53, 54, 59, 60, 61

Related papers

Loading 2608.15337v1…