Documentation

LeanPool.BrillNoetherGraphs.Bananas.Theta.ThetaKGeneralClassification

Endpoint-safe theta form of Theorem 4.13 #

The predicate deliberately retains the witness path positions from the all-submodularity classification. This avoids choosing incompatible proof terms for endpoint aliases while stating exactly the three non-endpoint families.

source
def Bananas.ThetaKGeneralCoordinates {k : ℕ} (B : Banana 2) (alpha beta : Fin 3) (i : Utilities.Certificate.SubdivisionGraph.Spec.PathPosition B alpha) (j : Utilities.Certificate.SubdivisionGraph.Spec.PathPosition B beta) :
Prop

The coordinate alternatives for k-general theta markings: nonrecurrent interior marks on distinct strands, or an allowed boundary pair on one strand.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem Bananas.theta_kGeneral_iff_coordinates_nonRecurrent {k : ℕ} (B : Banana 2) (alpha beta : Fin 3) (i : Utilities.Certificate.SubdivisionGraph.Spec.PathPosition B alpha) (j : Utilities.Certificate.SubdivisionGraph.Spec.PathPosition B beta) (hTO : IsTorsionOrder (mark (Utilities.Certificate.SubdivisionGraph.Spec.graph B) (strandVertex B alpha i) (strandVertex B beta j)) k) :
    KGeneralTransmission (mark (Utilities.Certificate.SubdivisionGraph.Spec.graph B) (strandVertex B alpha i) (strandVertex B beta j)) k ↔ ThetaKGeneralCoordinates B alpha beta i j