2607.19276v1 / Norine/Reproduction.lean

all files

import Norine.Basic
import Norine.ChainObstruction
import Norine.AntipodalModule

/-!
# Assembly and the remaining library interface

The paper-specific construction still missing from this development is isolated
in `PolyhedralChainRealization`: Proposition 5.7 together with the standard
source Smith tower, expressed through the checked `ForbiddenChainMap` interface.

No axiom is declared.  The final theorem below is an ordinary implication from
that explicitly named hypothesis.
-/

namespace Norine

noncomputable section

/-- The exact unformalized geometric construction: a diagonal rook labeling
produces the forbidden finite Smith tower.  In the paper this is obtained from
Freudenthal chains and subdivision-invariant radial polyhedral chains
(Sections 4 and 5). -/
def PolyhedralChainRealization : Prop :=
  ∀ K : ℕ, 2 ≤ K → RookLabeling K K → Nonempty (ForbiddenChainMap (K - 2))

/-- Theorem 2.3 follows from the radial polyhedral-chain construction and the
fully checked algebraic chain obstruction. -/
theorem diagonalRookTheorem_of_polyhedralChainRealization
    (hpoly : PolyhedralChainRealization) :
    DiagonalRookTheorem := by
  intro K hK
  constructor
  intro q
  obtain ⟨F⟩ := hpoly K hK q
  exact (forbiddenChainMap_isEmpty (K - 2)).false F

/-- The central theorem of the paper, conditional only on the explicitly named
polyhedral-chain realization interface above. -/
theorem norine_conjecture_of_polyhedralChainRealization
    (hpoly : PolyhedralChainRealization) :
    NorineConjecture :=
  norine_of_diagonal_rook
    (diagonalRookTheorem_of_polyhedralChainRealization hpoly)

#print axioms monoConnected_iff_walk
#print axioms rookLabelingEquivNaive
#print axioms norine_of_diagonal_rook
#print axioms norm_tower_aug_zero
#print axioms chain_level_borsuk_ulam
#print axioms forbiddenChainMap_isEmpty
#print axioms basisNorm_ker_eq_range
#print axioms norine_conjecture_of_polyhedralChainRealization

end

end Norine