Tuple codes and orbit classification (issue #11 unit 3b)

Every finite tuple of local EM carrier elements is coded by choosing (noncomputably, and with no canonicity claim) quotient representatives, taking the union of their finite skeleton supports, and compressing each representative against that common support (LocalEMContext.tupleCode). The code forgets the actual J-values of the support while retaining the term shapes and the equality/order pattern — so the code type is the countable LocalEMTupleCode Λ n (LocalEMCompression.lean).

The decisive endpoint is exists_carrierEquiv_of_tupleCode_eq: over a highly order-transitive skeleton, EQUAL CODES IMPLY THE SAME AUTOMORPHISM ORBIT — an order automorphism carrying the first support's increasing enumeration to the second's (high transitivity) renames the first tuple's representatives into the second's (locJRename_expand between the two expansions), and descends to the induced structure automorphism (carrierEquiv_mkClass). The code is NOT invariant under changing representatives, and need not be: distinguishing equivalent tuples only creates more codes, and countability plus "same code ⇒ same orbit" is all the countably-many-types argument consumes.

noncomputable def FirstOrder.Language.LocalEMContext.tupleSupport {Λ : Language} {J : Type} [LinearOrder J] {M : Type} [Λ.Structure M] (ctx : Λ.LocalEMContext J) {n : ℕ} (a : Fin n → Carrier Λ J ctx) : Finset J

The common finite skeleton support of a tuple's chosen representatives.

Equations

• ctx.tupleSupport a = Finset.univ.biUnion fun (i : Fin n) => Λ.locJSupport J (Quotient.out (a i))

theorem FirstOrder.Language.LocalEMContext.locJSupport_out_subset_tupleSupport {Λ : Language} {J : Type} [LinearOrder J] {M : Type} [Λ.Structure M] (ctx : Λ.LocalEMContext J) {n : ℕ} (a : Fin n → Carrier Λ J ctx) (i : Fin n) : Λ.locJSupport J (Quotient.out (a i)) ⊆ ctx.tupleSupport a

noncomputable def FirstOrder.Language.LocalEMContext.tupleCode {Λ : Language} {J : Type} [LinearOrder J] {M : Type} [Λ.Structure M] (ctx : Λ.LocalEMContext J) {n : ℕ} (a : Fin n → Carrier Λ J ctx) : Λ.LocalEMTupleCode n

The tuple code: representatives compressed against their common support. Noncanonical (it depends on Quotient.out), but countable and orbit-complete — which is all that is needed.

Equations

• ctx.tupleCode a = ⟨(ctx.tupleSupport a).card, fun (i : Fin n) => Λ.locJCompress J (ctx.tupleSupport a) (Quotient.out (a i)) ⋯⟩

theorem FirstOrder.Language.LocalEMContext.exists_carrierEquiv_of_tupleCode_eq {Λ : Language} {J : Type} [LinearOrder J] {M : Type} [Λ.Structure M] (ctx : Λ.LocalEMContext J) (hJ : HighlyOrderTransitive J) {n : ℕ} {a b : Fin n → Carrier Λ J ctx} (h : ctx.tupleCode a = ctx.tupleCode b) : ∃ (e : J ≃o J), ∀ (i : Fin n), (ctx.carrierEquiv e) (a i) = b i

The orbit theorem: over a highly order-transitive skeleton, tuples with equal codes lie in the same orbit of the induced structure automorphisms — some order automorphism of J carries one tuple to the other through the descended equivalence.