SemanticMainTheorem.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

The main theorem with concrete chain, fibre and finite-reflection inputs

Normalized chains construct the orientals, their ordinal maps and the interval diagonal. Contractions and two-sieve induction show that the finite-poset adjunction units are weak equivalences. Finite reflection commutes with zero fibres; simplexwise clamping proves poset-sieve preservation. Strong deformations and algebraic boundary factorization give simplicial gluing. A semantic quotient of finite formal cells constructs small strict colimits.

theorem OAI.Thomason.Construction.main_with_remaining_published_inputs line 34
Source documentation
All dimensions of the main theorem after discharging the normalized-chain and Alexander–Whitney identities, constructing the oriental edges and proving the finite-poset units, zero-fibre adjunctions, intelligent finite reflection, simplicial gluing from geometric deformation, and poset-sieve preservation. The published-input hypotheses are explicit.
```
theorem main_with_remaining_published_inputs
    (G : RightGrayInput normalizedSimplexIdentities) (t : GrayTruncationInput G)
    (kq : KanQuillenPublishedInput.{0})
    (hj : ∀ X : SSet.{0}, realizationWeakEquivalences (canonicalExtension.app X))
    (transfer : PublishedThomasonReduction normalizedSimplexIdentities)
    (loc : PublishedStreetLocalizationInput normalizedSimplexIdentities) :
    Nonempty (ThomasonModelResult normalizedSimplexIdentities.thomasonLeft
      normalizedSimplexIdentities.streetNerve kq hj) ∧
      ∀ n, Nonempty (ThomasonModelResult ((constructedFiniteReflection n).thomasonLeft normalizedSimplexIdentities)
        (normalizedSimplexIdentities.finiteStreetNerve (n + 1)) kq hj) :=
…
```
Mentions: OAI.Thomason.Construction.RightGrayInput, OAI.Thomason.Construction.normalizedSimplexIdentities, OAI.Thomason.Construction.GrayTruncationInput, OAI.Thomason.Construction.realizationWeakEquivalences, OAI.Thomason.Construction.PublishedThomasonReduction, OAI.Thomason.Construction.PublishedStreetLocalizationInput, OAI.Thomason.Construction.ThomasonModelResult, OAI.Thomason.Construction.constructedFiniteReflection, OAI.Thomason.thomasonLeft

theorem OAI.Thomason.Construction.main_with_semantic_class_inputs line 69

Source documentation

The main theorem assuming the two published semantic class identifications.

theorem main_with_semantic_class_inputs
    (G : RightGrayInput normalizedSimplexIdentities) (t : GrayTruncationInput G)
    (hb : I.rlp = J.rlp ⊓ realizationWeakEquivalences.{0})
    (hh : SSet.anodyneExtensions.{0} = monomorphisms SSet.{0} ⊓ realizationWeakEquivalences)
    (hj : ∀ X : SSet.{0}, realizationWeakEquivalences (canonicalExtension.app X))
    (transfer : PublishedThomasonReduction normalizedSimplexIdentities)
    (loc : PublishedStreetLocalizationInput normalizedSimplexIdentities) :
    let kq := kanQuillenInput_of_class_identifications hb hh
…

Mentions: OAI.Thomason.Construction.RightGrayInput, OAI.Thomason.Construction.normalizedSimplexIdentities, OAI.Thomason.Construction.GrayTruncationInput, OAI.Thomason.Construction.realizationWeakEquivalences, OAI.Thomason.Construction.PublishedThomasonReduction, OAI.Thomason.Construction.PublishedStreetLocalizationInput, OAI.Thomason.Construction.kanQuillenInput_of_class_identifications

theorem OAI.Thomason.Construction.main_with_anodyne_input line 86
Source documentation
The main theorem assuming the published anodyne characterization.
```
theorem main_with_anodyne_input
    (G : RightGrayInput normalizedSimplexIdentities) (t : GrayTruncationInput G)
    (hh : SSet.anodyneExtensions.{0} = monomorphisms SSet.{0} ⊓ realizationWeakEquivalences)
    (hj : ∀ X : SSet.{0}, realizationWeakEquivalences (canonicalExtension.app X))
    (transfer : PublishedThomasonReduction normalizedSimplexIdentities)
    (loc : PublishedStreetLocalizationInput normalizedSimplexIdentities) :
    let kq := kanQuillenInput_of_anodyne_class hh
…
```
Mentions: OAI.Thomason.Construction.RightGrayInput, OAI.Thomason.Construction.normalizedSimplexIdentities, OAI.Thomason.Construction.GrayTruncationInput, OAI.Thomason.Construction.realizationWeakEquivalences, OAI.Thomason.Construction.PublishedThomasonReduction, OAI.Thomason.Construction.PublishedStreetLocalizationInput, OAI.Thomason.Construction.kanQuillenInput_of_anodyne_class
theorem OAI.Thomason.Construction.main_with_acyclic_kan_lifting line 103
Source documentation
The main theorem assuming acyclic Kan lifting, as in Goerss–Jardine, Theorems I.11.3–I.11.4 and Corollary II.8.6.
```
theorem main_with_acyclic_kan_lifting
    (G : RightGrayInput normalizedSimplexIdentities) (t : GrayTruncationInput G)
    (hk : PublishedAcyclicKanLifting)
    (hj : ∀ X : SSet.{0}, realizationWeakEquivalences (canonicalExtension.app X))
    (transfer : PublishedThomasonReduction normalizedSimplexIdentities)
    (loc : PublishedStreetLocalizationInput normalizedSimplexIdentities) :
    let kq := kanQuillenInput_of_acyclic_kan_lifting hk
…
```
Mentions: OAI.Thomason.Construction.RightGrayInput, OAI.Thomason.Construction.normalizedSimplexIdentities, OAI.Thomason.Construction.GrayTruncationInput, OAI.Thomason.Construction.PublishedAcyclicKanLifting, OAI.Thomason.Construction.realizationWeakEquivalences, OAI.Thomason.Construction.PublishedThomasonReduction, OAI.Thomason.Construction.PublishedStreetLocalizationInput, OAI.Thomason.Construction.kanQuillenInput_of_acyclic_kan_lifting