Crossing lemma

Does the statement hold: For every phase ψ there is exactly one parameter p in [lo, hi] and one branch σ = ±1 whose value equals ψ modulo the period 2K.

For every phase ψ there is exactly one parameter p in [lo, hi] and one branch σ = ±1 whose value equals ψ modulo the period 2K. Prediction: Lean accepts CrossingData.crossing using only the standard axioms (no sorry).

Formalised in Lean 4 + Mathlib; #print axioms CrossingData.crossing after lake build.

Kernel-checked: CrossingData.crossing compiles and depends only on propext, Classical.choice and Quot.sound.

Abstract: it holds for any data satisfying the CrossingData interface; instantiating it for the SE(2) Jacobi functions is a separate step.

• CrossingData.crossing

  For every phase ψ there is exactly one parameter p in [lo, hi] and one branch σ = ±1 whose value equals ψ modulo the period 2K.

  Re-verify