Lai · Shkolnikov · Soner / arXiv:2512.17702 / Isabelle/HOL

Theorem 1.1, Unfolded

The value function of the relative-arbitrage exit-time problem is the unique bounded upper semicontinuous viscosity solution of F(∇v,∇²v)=1 on K. Below, the paper's own words sit beside the machine-checked formula — and every constant in it opens.

Theorem_1_1_Statement.thy
Click any underlined constant to unfold its Isabelle definition. Constants inside a definition open too, so you can descend to the primitives; a breadcrumb tracks the path back. Indigo names a definition of this development, teal one from Isabelle's libraries or the AFP, and ochre marks a constant carrying one of the three points of clarification below.
§1

Standing hypotheses

Theorem 1.1, as written

“Let n ≥ 2, k ∈ {1, 2, …, n−1}, and L ≥ 1. Suppose K ⊂ ℝn is compact.”

As formalised

    The pair 1 ≤ k and k < CARD('n) is exactly k ∈ {1,…,n−1}, and it forces n ≥ 2 on its own, so the paper's dimension hypothesis needs no separate assumption. No clause needs K ≠ ∅. The paper's further hypothesis, the Tι family, is not a standing one: it serves the uniqueness clause alone, and appears there, as the premise of conjunct ∧4.

    §2

    Where the equation comes in

    The theorem is about solutions of F(∇v,∇²v) = 1, yet that equation never appears as an equation in the formal statement — and it cannot, since v is merely upper semicontinuous and has no derivatives to speak of. Definition 3.1 is what turns it into something a non-differentiable function can satisfy. Here is each piece, and what becomes of it.

    F(∇v, ∇²v) = 1
    • F

      The fully nonlinear degenerate elliptic operator of Eq. (1.9), formalised as ell_op k L. It is an infimum of -½ trace (M ** a) over the admissible covariation matrices a — so the equation is a statement about the worst case the market can present.

    • ∇v

      Not a gradient of v, which need not exist. A test function φ is brought into contact with v — touching it from above for the subsolution half, from below for the supersolution half — and ∇φ(x) stands in. In the formal statement that gradient is the g x of test_fun_C2 φ g H x.

    • ∇²v

      Likewise the Hessian ∇²φ(x), which is the H of the same touching test function. Requiring φ to be genuinely C² matters: the uniqueness clause assumes this property of a competitor, so a laxer class would weaken the theorem.

    • = 1

      The equality does not survive the relaxation; it becomes two one-sided bounds, one per touching direction. A function satisfying both is a solution, in the viscosity sense. The envelopes F* and F* appear because F itself is not continuous.

    Subsolution 
    ell_op_lsc k L (g x) H ≤ 1

    whenever φ touches v from above across K

    Supersolution 
    1 ≤ ell_op_usc k L (g x) H

    whenever φ touches the lower envelope lsc_envK K v from below

    These two inequalities are the whole content of visc_subsol_env2 and visc_supersol_env2, which is why conjuncts ∧2 and ∧3 below carry the equation without ever writing it down.

    §3

    What the theorem asserts

    The formal statement is a single formula: a five-fold conjunction, each conjunct carrying one clause of the paper's claim. All five speak about one function, fixed once here.

    defines
    v ≡ λz. enn2real (xval k L K z)

    Every v below is this function: the value function of Eq. (1.6), read as a real number. It is the subject of all five clauses, and the thing the uniqueness clause says nothing else can be.

    theorem theorem_1_1 — shows
    
    
    

    
    
  
    

  
  
    
    
    
      §4
      
    Points of clarification
    
    
    
    
    Three places where the wording admits more than one reading, or where a step
      wants restating. In each the formalization had to commit, and in each the intended reading looks
      plain — a word from the authors would settle it. Everything else that once looked like a
      divergence has been closed by proof, and is not listed.
    
    
    
  
    

  
  
    
    
    
      §5
      
    Every constant, in one table
    
    
    
    
    The complete vocabulary of the statement. Constant names open their definition;
      the middle column is the paper's counterpart.
    
    
    
      
    
        
          
    ConstantIn the paperDefined in