Companion equivalence below a level

Under allowedness of the path and level-uniform approximation along it, the companion and the base are equivalent as empty tuples.

• PathApproxAt Lc Bstar B π β N: from position N on, the component B (π k) is β-equivalent to the default as empty tuples. PathApprox … α: every β < α has such a threshold.
• companion_bfEquiv_of_pathApproxAt: at one level β with threshold N, the companion and the base are β-equivalent. The proof is the same-level assembly bfEquiv_of_fiberBF along the Hilbert-hotel bijection shiftRows hπ N with the vacuous empty-tuple matching and fiberBF_of_no_points; the fiberwise obligation splits as: fibers of a non-tail row are equal; a tail prefix π|ₖ against π|ₖ₊₁ differs only at prefixLabel π k, where B_* faces B (π k) in that orientation; the path row against π|ₙ agrees at labels of length ≤ N, and at a longer on-path label prefixLabel π j (j ≥ N) the pair is B (π j) against B_*, the symmetric orientation.
• companion_bfEquiv: below α, with the threshold chosen separately for each level. No single bijection is claimed to work at every level.

Hypotheses: the ambient setup (letters, the default and component structures over Lc, and the allowed sets), allowedness of the path (IsAllowedPath A π), and the approximation hypothesis (PathApproxAt at the given level, or PathApprox below α); no countability, relationality, nesting, non-defaultness, rank bounds, or ordinal-limit assumption.

Level-uniform path approximation

def FirstOrder.Language.FiberAssembly.PathApproxAt {U : Type u} (Lc : Language) (Bstar : Type u) (B : U → Type u) [Lc.Structure Bstar] [(u : U) → Lc.Structure (B u)] (π : ℕ → U) (β : Ordinal.{u}) (N : ℕ) : Prop

(H_path-approx) at level β with threshold N.

Equations

• FirstOrder.Language.FiberAssembly.PathApproxAt Lc Bstar B π β N = ∀ (k : ℕ), N ≤ k → FirstOrder.Language.BFEquiv β 0 Fin.elim0 Fin.elim0

def FirstOrder.Language.FiberAssembly.PathApprox {U : Type u} (Lc : Language) (Bstar : Type u) (B : U → Type u) [Lc.Structure Bstar] [(u : U) → Lc.Structure (B u)] (π : ℕ → U) (α : Ordinal.{u}) : Prop

(H_path-approx) below α: every level has a threshold.

Equations

• FirstOrder.Language.FiberAssembly.PathApprox Lc Bstar B π α = ∀ β < α, ∃ (N : ℕ), FirstOrder.Language.FiberAssembly.PathApproxAt Lc Bstar B π β N

Transport along component-index equalities

theorem FirstOrder.Language.FiberAssembly.isPathPrefix_eq_prefixLabel {U : Type u} {π : ℕ → U} {τ : Label U} (h : IsPathPrefix π τ) : τ = prefixLabel π ((↑τ).length - 1)

A nonempty label on the path is the prefix label of its predecessor length.

The equivalence

theorem FirstOrder.Language.FiberAssembly.companion_bfEquiv_of_pathApproxAt {U : Type u} [LinearOrder U] {Lc : Language} (Bstar : Type u) (B : U → Type u) [Lc.Structure Bstar] [(u : U) → Lc.Structure (B u)] {A : ℕ → Set U} {π : ℕ → U} (hπ : IsAllowedPath A π) {β : Ordinal.{u}} {N : ℕ} (happ : PathApproxAt Lc Bstar B π β N) : BFEquiv β 0 Fin.elim0 Fin.elim0

Companion equivalence at one level. Under allowedness and approximation from threshold N at level β, the companion and the base are β-equivalent as empty tuples.

theorem FirstOrder.Language.FiberAssembly.companion_bfEquiv {U : Type u} [LinearOrder U] {Lc : Language} (Bstar : Type u) (B : U → Type u) [Lc.Structure Bstar] [(u : U) → Lc.Structure (B u)] {A : ℕ → Set U} {π : ℕ → U} (hπ : IsAllowedPath A π) {α : Ordinal.{u}} (happ : PathApprox Lc Bstar B π α) (β : Ordinal.{u}) : β < α → BFEquiv β 0 Fin.elim0 Fin.elim0

Companion equivalence below α, with the threshold chosen separately for each level.