Documentation

LeanPool.NandakumarRamanaRao.NRR.AAK.SimplestRoute

AAK simplest route #

This module records the hybrid route. The order-complex realization supplies the compact glued configuration model, while the top cycle is defined by the genuine cellular incidence sum.

source
theorem NRR.AAK.simplestRoute_actualBoundaryReduction {p : ℕ} (hp : Nat.Prime p) (a : BarredPermutation p) :
FoxNeuwirth.actualTopBoundaryCoefficient a = ↑(FoxNeuwirth.topExtensionMultiplicity a) * ↑a.orientationSign

The first completed reduction: actual boundary coefficients are extension multiplicities.

source
noncomputable def NRR.AAK.simplestRouteCellularCycle {p : ℕ} (hp : Nat.Prime p) (H : FoxNeuwirth.FacetShuffleCardinality p) :
FiniteIncidenceCycle (ZMod p)

The finite shuffle-cardinality theorem is sufficient to construct the genuine cellular incidence cycle.

Equations
Instances For
    source
    theorem NRR.AAK.simplestRoute_facetTheorem (p : ℕ) (hp : Nat.Prime p) :
    FoxNeuwirth.FacetShuffleCardinality p

    The facet--shuffle theorem is unconditional.

    source
    theorem NRR.AAK.simplestRoute_cellularStage (p : ℕ) (hp : Nat.Prime p) :
    Nonempty (FiniteIncidenceCycle (ZMod p))

    The genuine cellular-cycle stage is closed for every prime.

    source
    theorem NRR.AAK.simplestRoute_topIncidenceStage (p : ℕ) (hp : Nat.Prime p) :
    (FoxNeuwirth.topIncidenceBoundary (FoxNeuwirth.orientedTopChain p) = fun (x : BarredPermutation p) => 0) ∧ FoxNeuwirth.zeroFacetBoundary (FoxNeuwirth.topIncidenceBoundary (FoxNeuwirth.orientedTopChain p)) = fun (x : PUnit.{0}) => 0

    The exact two-term top incidence complex is unconditional. No lower-dimensional Fox--Neuwirth incidence convention is assumed.

    source
    def NRR.AAK.SimplestRouteObstructionTheorem :
    Prop

    The exact analytic/topological theorem needed after the finite cellular and affine stages. Its output is a locally constant orbit obstruction on the complement of the projected zero set.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      noncomputable def NRR.AAK.simplestRouteStep (H : SimplestRouteObstructionTheorem) (p : ℕ) (hp : Nat.Prime p) (K : Geometry.ConvexBody Geometry.Plane) (A : ℝ) (hA : 0 < A) [Nonempty (BodySpace K A)] (phi : NiceMV (BodySpace K (A / ↑p))) :
      FlexiblePrimeRefinementStep hp hA phi

      A locally constant obstruction on the order-complex model produces a model-independent prime-refinement step.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        theorem NRR.AAK.simplestRoute_implies_flexiblePrimeRefinement (H : SimplestRouteObstructionTheorem) :
        FlexiblePrimeRefinementTheorem

        The locally constant obstruction theorem closes the flexible prime-refinement interface.

        source
        theorem NRR.AAK.avvakumov_akopyan_karasev_of_simplestRoute (H : SimplestRouteObstructionTheorem) (K : Geometry.ConvexBody Geometry.Plane) (n : ℕ) :
        0 < n → ∃ (P : ConvexPartition K n), P.IsFair

        The locally constant obstruction theorem and the model-independent prime-factor iteration yield the full arbitrary-number conclusion.