Companions are not isomorphic to the base, nor to each other

For an arbitrary path π (no allowedness: the companion carrier is defined for every path, and labels include inadmissible words) with infinitely many non-default positions (InfinitelyNonDefault: positions are counted, so repeated occurrences of one non-default component suffice), and a relational component language:

• companion_not_iso: the companion along π is not isomorphic to the base.
• companions_not_iso: for π ≠ σ, the companion along π is not isomorphic to the companion along σ; only the source path's non-default positions are used.

Route: an isomorphism restricts to rows (restrictRows) and, with [Lc.IsRelational], to fiber isomorphisms at every label (restrictFiber). The path row's image is a finite row s or the other path row. In the first case take a non-default position k > s.length: at the prefix label π|ₖ₊₁ the path row has B (π k) while s has the default. In the second case take any coordinate k₀ where the paths differ and a non-default position k ≥ k₀: π|ₖ₊₁ is not on σ (not_isPathPrefix_prefixLabel_of_ne), so again B (π k) faces the default. Both cases end in the shared helper: a fiber isomorphism from the index some (π k) to the index none would make π k default-like. Transport is through the component indices and their canonical structures.

No approximation, countability, nesting, or rank hypothesis enters.

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

(H_path-nondefault) infinitely many non-default positions on the path. Positions are counted, not distinct letters.

Equations

• FirstOrder.Language.FiberAssembly.InfinitelyNonDefault Lc Bstar B π = {k : ℕ | ¬FirstOrder.Language.FiberAssembly.DefaultLike Lc Bstar B (π k)}.Infinite

theorem FirstOrder.Language.FiberAssembly.companion_not_iso {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} [Lc.IsRelational] (π : ℕ → U) (hnd : InfinitelyNonDefault Lc Bstar B π) : IsEmpty ((lang U Lc).Equiv (CompanionCarrier Bstar B A π) (PrefixCarrier Bstar B A))

The companion is not isomorphic to the base.

theorem FirstOrder.Language.FiberAssembly.companions_not_iso {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} [Lc.IsRelational] {π σ : ℕ → U} (hne : π ≠ σ) (hnd : InfinitelyNonDefault Lc Bstar B π) : IsEmpty ((lang U Lc).Equiv (CompanionCarrier Bstar B A π) (CompanionCarrier Bstar B A σ))

Distinct paths give non-isomorphic companions, from the source path's non-default positions only.