Documentation

InfinitaryLogic.ModelTheory.FiberCantorFamily

A Cantor-indexed family of companions of the exact-ω base #

For a binary sequence z : ℕ → Bool, the path π_z (2n) = n, π_z (2n + 1) = n + z n (cantorPath) is nondecreasing, unbounded, allowed under A n = {u | u ≤ n}, and recovers z from its odd coordinates, so distinct sequences give distinct paths (cantorPath_injective). CantorCompanion z is the companion of the exact-ω base Carrier' along π_z.

The family (cantorFamily): the base has internal Scott rank exactly ω (internalScottRank_exactOmega, reused as proved); the companions are countable (instCountableCompanion through the abbreviation); each companion is β-equivalent to the base for every β < ω (companion_bfEquiv, with threshold 2m at level m: π_z k ≥ k / 2 ≥ m for k ≥ 2m, so Fin (π_z k + 1) ≡_m ℕ by bfEquiv_nat_fin_iff); no companion is isomorphic to the base, and distinct sequences give non-isomorphic companions (companion_not_iso, companions_not_iso; every position is non-default since no finite component is isomorphic to ℕ).

"Cantor-indexed" describes the indexing set ℕ → Bool only: no continuity, Borelness, common-carrier coding, or effectiveness is claimed, and no rank is inferred for any companion.

The paths #

source
def FirstOrder.Language.FiberAssembly.ExactOmega.cantorPath (z : ℕ → Bool) :
ℕ → ℕ

The path of a binary sequence: π_z (2n) = n, π_z (2n + 1) = n + z n.

Equations
Instances For
    source
    theorem FirstOrder.Language.FiberAssembly.ExactOmega.cantorPath_even (z : ℕ → Bool) (n : ℕ) :
    cantorPath z (2 * n) = n
    source
    theorem FirstOrder.Language.FiberAssembly.ExactOmega.cantorPath_odd (z : ℕ → Bool) (n : ℕ) :
    cantorPath z (2 * n + 1) = n + if z n = true then 1 else 0
    source
    theorem FirstOrder.Language.FiberAssembly.ExactOmega.cantorPath_le (z : ℕ → Bool) (k : ℕ) :
    cantorPath z k ≤ k

    The path stays below the identity: allowed positionwise.

    source
    theorem FirstOrder.Language.FiberAssembly.ExactOmega.half_le_cantorPath (z : ℕ → Bool) (k : ℕ) :
    k / 2 ≤ cantorPath z k

    The path is unbounded: at least half the position.

    source
    theorem FirstOrder.Language.FiberAssembly.ExactOmega.cantorPath_monotone (z : ℕ → Bool) :
    Monotone (cantorPath z)
    source
    theorem FirstOrder.Language.FiberAssembly.ExactOmega.cantorPath_allowed (z : ℕ → Bool) :
    IsAllowedPath Aiic (cantorPath z)
    source
    theorem FirstOrder.Language.FiberAssembly.ExactOmega.cantorPath_injective :
    Function.Injective cantorPath

    Odd coordinates recover the sequence: distinct sequences give distinct paths.

    The companions and the per-path hypotheses #

    source
    @[reducible, inline]
    abbrev FirstOrder.Language.FiberAssembly.ExactOmega.CantorCompanion (z : ℕ → Bool) :
    Type

    The companion of the exact-ω base along π_z.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem FirstOrder.Language.FiberAssembly.ExactOmega.cantorCompanion_countable (z : ℕ → Bool) :
      Countable (CantorCompanion z)

      Countability, discharged by the companion instance through the abbreviation.

      source
      theorem FirstOrder.Language.FiberAssembly.ExactOmega.cantorPath_pathApproxAt (z : ℕ → Bool) (m : ℕ) :
      PathApproxAt Language.empty ℕ Bfin (cantorPath z) (↑m) (2 * m)

      At level m the threshold 2m works: beyond it the path is at least m.

      source
      theorem FirstOrder.Language.FiberAssembly.ExactOmega.cantorPath_pathApprox (z : ℕ → Bool) :
      PathApprox Language.empty ℕ Bfin (cantorPath z) Ordinal.omega0
      source
      theorem FirstOrder.Language.FiberAssembly.ExactOmega.cantorPath_infinitelyNonDefault (z : ℕ → Bool) :
      InfinitelyNonDefault Language.empty ℕ Bfin (cantorPath z)

      Every position is non-default.

      The package #

      source
      theorem FirstOrder.Language.FiberAssembly.ExactOmega.cantorCompanion_bfEquiv (z : ℕ → Bool) (β : Ordinal.{0}) :
      β < Ordinal.omega0 → BFEquiv β 0 Fin.elim0 Fin.elim0

      Each companion is β-equivalent to the base for every β < ω.

      source
      theorem FirstOrder.Language.FiberAssembly.ExactOmega.cantorCompanion_not_iso (z : ℕ → Bool) :
      IsEmpty ((lang ℕ Language.empty).Equiv (CantorCompanion z) Carrier')

      No companion is isomorphic to the base.

      source
      theorem FirstOrder.Language.FiberAssembly.ExactOmega.cantorCompanions_not_iso {z w : ℕ → Bool} (h : z ≠ w) :
      IsEmpty ((lang ℕ Language.empty).Equiv (CantorCompanion z) (CantorCompanion w))

      Distinct sequences give non-isomorphic companions.

      source
      theorem FirstOrder.Language.FiberAssembly.ExactOmega.cantorFamily :
      internalScottRank Carrier' = Ordinal.omega0 ∧ (∀ (z : ℕ → Bool), Countable (CantorCompanion z)) ∧ (∀ (z : ℕ → Bool), ∀ β < Ordinal.omega0, BFEquiv β 0 Fin.elim0 Fin.elim0) ∧ (∀ (z : ℕ → Bool), IsEmpty ((lang ℕ Language.empty).Equiv (CantorCompanion z) Carrier')) ∧ ∀ (z w : ℕ → Bool), z ≠ w → IsEmpty ((lang ℕ Language.empty).Equiv (CantorCompanion z) (CantorCompanion w))

      The Cantor-indexed family. The base has internal Scott rank exactly ω (reused as proved); the companions indexed by binary sequences are countable, β-equivalent to the base for every β < ω, not isomorphic to it, and pairwise non-isomorphic. No rank is claimed for any companion.