Root realizations: indices realized in context

Every realizational/separationist framework that adopts late insertion or a separate lexemic index factors a root into an opaque individuator plus context-sensitive form and (optionally) meaning maps: DM's √ individuated by arbitrary indices, form at Vocabulary Insertion ([Har14b], [Mar97], [Emb21]); [Bor13]'s phonological indices (her form individuation R ↪ F is her instance's axiom, not the interface's); PFM's opaque lexeme realized at a cell ([Stu01], [BS17]); [Spe13b]'s lexemic index. [Bea95]'s Separation Hypothesis grounds the form-side separation; the meaning-side separation is DM's List-3 move. Realization fixes that object; sign-based lexicalism, Construction Morphology, and [Has25b]'s morph-based comparative root are rival ontologies its parameters measure, not instances of it (survey: [Loh20]). The interface is agnostic about whether indices are listed or constructed ([Ble16]).

realize is Finset-valued: the empty fiber is non-licensing, a non-singleton an overabundant cell, matching Paradigm/Linkage.lean; the univalent and total strata are IsUnivalent and IsTotal. Frameworks diverge along parameters — what R individuates (√, lexeme, morph), what Ctx is (categorizer configuration vs paradigm cell — vs [Bor13]'s headless categorial frames, a Ctx-instantiation contrast; [Loh20]), what F is (ConsonantalRoot α is a choice of F), whether interpretation is present (Realization.Interpreted) — never along the core.

Hom merges indices with a context translation that may consult the source index; Realization.Interpreted.Hom is the strict tier — root-independent context translation, interpretation-preserving — on which individuation disputes are stated: merged indices must share their whole profile (Hom.profileEq_of_onRoot_eq), so strict mergers collapse only exact profile-duplicates and Interpreted.reduce is terminal among them. The individuation rivalries live at the lax tier, where fat-root and sister-root presentations subsume each other's data: extensional profiles underdetermine individuation, and the discriminators the literature actually uses — first-categorization locality ([Ara05]), the denial that indices are linguistic objects, processing evidence — are extra structure on admissible mergers that studies supply. The interface localizes the dispute precisely because it cannot resolve it. One mild theory-ladenness to note: the strict tier's root-independent context translation forces categorial information into Ctx, quietly encoding the Categorization Assumption.

Main declarations

• Realization — indices with contextual realization; IsLicensed, Realizes, exponents, IsTotal, IsUnivalent.
• IsConstantIn / IsVariantIn — the constancy pair over any contextual map; instantiated as IsInvariant/IsSuppletive (form) and IsIntrinsic/IsAllosemous (meaning).
• Realization.RealizeEq, Realization.IsHomophonous — form identity vs index identity.
• Realization.Hom — index mergers with realization tracking; Interpreted.Hom — the strict, interpretation-preserving tier; Realization.Interpreted.Hom.interp_eq_of_onRoot_eq.
• Realization.Interpreted — the two-map extension ([Mar97]'s List 2 / List 3).
• Realization.comp — Kleisli pipelining; Interpreted.ProfileEq, Interpreted.reduce, Hom.profileEq_of_onRoot_eq — the reduced presentation and the strict-merger bound.

def Morphology.IsConstantIn {R : Type u_1} {Ctx : Type u_2} {X : Type u_5} (g : R → Ctx → Finset X) (r : R) : Prop

Constancy of a contextual map at an index: all values, across all contexts, coincide.

Equations

• Morphology.IsConstantIn g r = ∀ ⦃c c' : Ctx⦄, ∀ x ∈ g r c, ∀ x' ∈ g r c', x = x'

def Morphology.IsVariantIn {R : Type u_1} {Ctx : Type u_2} {X : Type u_5} (g : R → Ctx → Finset X) (r : R) : Prop

Variance of a contextual map at an index: two distinct values arise.

Equations

• Morphology.IsVariantIn g r = ∃ (c : Ctx) (c' : Ctx), ∃ x ∈ g r c, ∃ x' ∈ g r c', x ≠ x'

theorem Morphology.not_isConstantIn_of_isVariantIn {R : Type u_1} {Ctx : Type u_2} {X : Type u_5} {g : R → Ctx → Finset X} {r : R} (h : IsVariantIn g r) : ¬IsConstantIn g r

theorem Morphology.isConstantIn_iff_subsingleton {R : Type u_1} {Ctx : Type u_2} {X : Type u_5} {g : R → Ctx → Finset X} {r : R} : IsConstantIn g r ↔ {x : X | ∃ (c : Ctx), x ∈ g r c}.Subsingleton

Constancy at an index is subsingletonhood of the index's total image — the bridge to mathlib's Set.Subsingleton ecosystem.

structure Morphology.Realization (R : Type u_6) (Ctx : Type u_7) (F : Type u_8) : Type (max (max u_6 u_7) u_8)

A root realization: an opaque index type realized in context. The fiber realize r c is empty where r is unlicensed, non-singleton at an overabundant cell.

• realize : R → Ctx → Finset F

  The realization of an index in a context: Vocabulary Insertion (DM), the paradigm function (PFM), spellout (nanosyntax).

def Morphology.Realization.IsLicensed {R : Type u_1} {Ctx : Type u_2} {F : Type u_3} (S : Realization R Ctx F) (r : R) (c : Ctx) : Prop

r is licensed in c: some realization exists.

Equations

• S.IsLicensed r c = (S.realize r c).Nonempty

def Morphology.Realization.Realizes {R : Type u_1} {Ctx : Type u_2} {F : Type u_3} (S : Realization R Ctx F) (r : R) (f : F) : Prop

f realizes r in some context.

Equations

• S.Realizes r f = ∃ (c : Ctx), f ∈ S.realize r c

def Morphology.Realization.exponents {R : Type u_1} {Ctx : Type u_2} {F : Type u_3} (S : Realization R Ctx F) (r : R) : Set F

The allomorph set of a root.

Equations

• S.exponents r = {f : F | S.Realizes r f}

@[simp]

theorem Morphology.Realization.mem_exponents {R : Type u_1} {Ctx : Type u_2} {F : Type u_3} (S : Realization R Ctx F) {r : R} {f : F} : f ∈ S.exponents r ↔ S.Realizes r f

def Morphology.Realization.IsTotal {R : Type u_1} {Ctx : Type u_2} {F : Type u_3} (S : Realization R Ctx F) : Prop

Every index is licensed everywhere — PFM's stratum.

Equations

• S.IsTotal = ∀ (r : R) (c : Ctx), (S.realize r c).Nonempty

def Morphology.Realization.IsUnivalent {R : Type u_1} {Ctx : Type u_2} {F : Type u_3} (S : Realization R Ctx F) : Prop

At most one form per cell — the stratum of Option-shaped engine outputs.

Equations

• S.IsUnivalent = ∀ (r : R) (c : Ctx), (S.realize r c).card ≤ 1

def Morphology.Realization.IsInvariant {R : Type u_1} {Ctx : Type u_2} {F : Type u_3} (S : Realization R Ctx F) (r : R) : Prop

One form wherever licensed: the classical context-free morpheme, as the degenerate case.

Equations

• S.IsInvariant r = Morphology.IsConstantIn S.realize r

def Morphology.Realization.IsSuppletive {R : Type u_1} {Ctx : Type u_2} {F : Type u_3} (S : Realization R Ctx F) (r : R) : Prop

Distinct forms in distinct contexts — √GO as go and went, [Har14b]'s argument that indices, not forms, individuate.

Equations

• S.IsSuppletive r = Morphology.IsVariantIn S.realize r

theorem Morphology.Realization.not_isInvariant_of_isSuppletive {R : Type u_1} {Ctx : Type u_2} {F : Type u_3} (S : Realization R Ctx F) {r : R} (h : S.IsSuppletive r) : ¬S.IsInvariant r

A suppletive root is not invariant.

theorem Morphology.Realization.isInvariant_iff_subsingleton_exponents {R : Type u_1} {Ctx : Type u_2} {F : Type u_3} (S : Realization R Ctx F) {r : R} : S.IsInvariant r ↔ (S.exponents r).Subsingleton

Invariance is subsingletonhood of the allomorph set.

def Morphology.Realization.IsOverabundant {R : Type u_1} {Ctx : Type u_2} {F : Type u_3} (S : Realization R Ctx F) (r : R) : Prop

Overabundance at an index: some cell offers two forms (dived/dove in one cell, [Tho11]-style — cf. Linkage.HasCellMates). Cell-internal variance, disjoint in kind from suppletion.

Equations

• S.IsOverabundant r = ∃ (c : Ctx), 1 < (S.realize r c).card

def Morphology.Realization.IsProperlySuppletive {R : Type u_1} {Ctx : Type u_2} {F : Type u_3} (S : Realization R Ctx F) (r : R) : Prop

Suppletion proper: two licensed contexts realized by different fibers (√GO: go/went). An unlicensed cell never witnesses it.

Equations

• S.IsProperlySuppletive r = ∃ (c : Ctx) (c' : Ctx), (S.realize r c).Nonempty ∧ (S.realize r c').Nonempty ∧ S.realize r c ≠ S.realize r c'

theorem Morphology.Realization.isSuppletive_iff {R : Type u_1} {Ctx : Type u_2} {F : Type u_3} (S : Realization R Ctx F) {r : R} : S.IsSuppletive r ↔ S.IsOverabundant r ∨ S.IsProperlySuppletive r

The variance decomposition: form variance at an index is overabundance or suppletion proper.

def Morphology.Realization.RealizeEq {R : Type u_1} {Ctx : Type u_2} {F : Type u_3} (S : Realization R Ctx F) (r r' : R) : Prop

Contextwise identity of realization.

Equations

• S.RealizeEq r r' = ∀ (c : Ctx), S.realize r c = S.realize r' c

theorem Morphology.Realization.RealizeEq.symm {R : Type u_1} {Ctx : Type u_2} {F : Type u_3} (S : Realization R Ctx F) {r r' : R} (h : S.RealizeEq r r') : S.RealizeEq r' r

def Morphology.Realization.IsHomophonous {R : Type u_1} {Ctx : Type u_2} {F : Type u_3} (S : Realization R Ctx F) (r r' : R) : Prop

Distinct indices sharing every realization (bank₁/bank₂): spellout is nowhere required to be injective.

Equations

• S.IsHomophonous r r' = (r ≠ r' ∧ S.RealizeEq r r')

theorem Morphology.Realization.IsHomophonous.symm {R : Type u_1} {Ctx : Type u_2} {F : Type u_3} (S : Realization R Ctx F) {r r' : R} (h : S.IsHomophonous r r') : S.IsHomophonous r' r

@[implicit_reducible]

instance Morphology.Realization.instDecidableIsLicensed {R : Type u_1} {Ctx : Type u_2} {F : Type u_3} (S : Realization R Ctx F) (r : R) (c : Ctx) : Decidable (S.IsLicensed r c)

Equations

• S.instDecidableIsLicensed r c = Morphology.Realization.instDecidableIsLicensed._aux_1 S r c

@[implicit_reducible]

instance Morphology.Realization.instDecidableRealizes {R : Type u_1} {Ctx : Type u_2} {F : Type u_3} (S : Realization R Ctx F) [Fintype Ctx] [DecidableEq F] (r : R) (f : F) : Decidable (S.Realizes r f)

Equations

• S.instDecidableRealizes r f = Morphology.Realization.instDecidableRealizes._aux_1 S r f

@[implicit_reducible]

instance Morphology.Realization.instDecidableIsInvariant {R : Type u_1} {Ctx : Type u_2} {F : Type u_3} (S : Realization R Ctx F) [Fintype Ctx] [DecidableEq F] (r : R) : Decidable (S.IsInvariant r)

Equations

• S.instDecidableIsInvariant r = Morphology.Realization.instDecidableIsInvariant._aux_1 S r

@[implicit_reducible]

instance Morphology.Realization.instDecidableIsSuppletive {R : Type u_1} {Ctx : Type u_2} {F : Type u_3} (S : Realization R Ctx F) [Fintype Ctx] [DecidableEq F] (r : R) : Decidable (S.IsSuppletive r)

Equations

• S.instDecidableIsSuppletive r = Morphology.Realization.instDecidableIsSuppletive._aux_1 S r

@[implicit_reducible]

instance Morphology.Realization.instDecidableIsOverabundant {R : Type u_1} {Ctx : Type u_2} {F : Type u_3} (S : Realization R Ctx F) [Fintype Ctx] (r : R) : Decidable (S.IsOverabundant r)

Equations

• S.instDecidableIsOverabundant r = Morphology.Realization.instDecidableIsOverabundant._aux_1 S r

@[implicit_reducible]

instance Morphology.Realization.instDecidableIsProperlySuppletive {R : Type u_1} {Ctx : Type u_2} {F : Type u_3} (S : Realization R Ctx F) [Fintype Ctx] [DecidableEq F] (r : R) : Decidable (S.IsProperlySuppletive r)

Equations

• S.instDecidableIsProperlySuppletive r = Morphology.Realization.instDecidableIsProperlySuppletive._aux_1 S r

@[implicit_reducible]

instance Morphology.Realization.instDecidableRealizeEq {R : Type u_1} {Ctx : Type u_2} {F : Type u_3} (S : Realization R Ctx F) [Fintype Ctx] [DecidableEq F] (r r' : R) : Decidable (S.RealizeEq r r')

Equations

• S.instDecidableRealizeEq r r' = Morphology.Realization.instDecidableRealizeEq._aux_1 S r r'

@[implicit_reducible]

instance Morphology.Realization.instDecidableIsHomophonousOfDecidableEq {R : Type u_1} {Ctx : Type u_2} {F : Type u_3} (S : Realization R Ctx F) [Fintype Ctx] [DecidableEq F] [DecidableEq R] (r r' : R) : Decidable (S.IsHomophonous r r')

Equations

• S.instDecidableIsHomophonousOfDecidableEq r r' = Morphology.Realization.instDecidableIsHomophonousOfDecidableEq._aux_1 S r r'

@[implicit_reducible]

instance Morphology.Realization.instDecidableIsTotal {R : Type u_1} {Ctx : Type u_2} {F : Type u_3} (S : Realization R Ctx F) [Fintype Ctx] [Fintype R] : Decidable S.IsTotal

Equations

• S.instDecidableIsTotal = Morphology.Realization.instDecidableIsTotal._aux_1 S

@[implicit_reducible]

instance Morphology.Realization.instDecidableIsUnivalent {R : Type u_1} {Ctx : Type u_2} {F : Type u_3} (S : Realization R Ctx F) [Fintype Ctx] [Fintype R] : Decidable S.IsUnivalent

Equations

• S.instDecidableIsUnivalent = Morphology.Realization.instDecidableIsUnivalent._aux_1 S

def Morphology.Realization.comp {R : Type u_1} {Ctx : Type u_2} {F : Type u_3} {G : Type u_6} [DecidableEq G] (S : Realization R Ctx F) (T : Realization F Ctx G) : Realization R Ctx G

Pipeline composition — Kleisli of Finset over a shared context: realize through an intermediate inventory. Late-insertion architectures factor the grammar's realization as such a composite; PFM's stem-choice-then-blocks cascade is another.

Equations

• S.comp T = { realize := fun (r : R) (c : Ctx) => (S.realize r c).biUnion fun (f : F) => T.realize f c }

theorem Morphology.Realization.comp_isTotal {R : Type u_1} {Ctx : Type u_2} {F : Type u_3} {G : Type u_6} [DecidableEq G] {S : Realization R Ctx F} {T : Realization F Ctx G} (hS : S.IsTotal) (hT : T.IsTotal) : (S.comp T).IsTotal

Totality is closed under pipelining.

structure Morphology.Realization.Hom {F : Type u_3} {R₁ : Type u_6} {C₁ : Type u_7} {R₂ : Type u_8} {C₂ : Type u_9} (S : Realization R₁ C₁ F) (T : Realization R₂ C₂ F) : Type (max (max (max u_6 u_7) u_8) u_9)

An index merger with spellout tracking: onRoot may merge indices, onCtx translates contexts and may consult the source index. The transport tier — for adjudicating individuation disputes use Realization.Interpreted.Hom, whose root-independent context translation blocks re-encoding the source index in the target context.

• onRoot : R₁ → R₂

  The index translation; non-injectivity is individuation coarsening.

• onCtx : R₁ → C₁ → C₂

  The context translation.

• realize_eq (r : R₁) (c : C₁) : S.realize r c = T.realize (self.onRoot r) (self.onCtx r c)

  Realization is preserved.

def Morphology.Realization.Hom.id {R : Type u_1} {Ctx : Type u_2} {F : Type u_3} (S : Realization R Ctx F) : S.Hom S

The identity hom.

Equations

• Morphology.Realization.Hom.id S = { onRoot := fun (r : R) => r, onCtx := fun (x : R) (c : Ctx) => c, realize_eq := ⋯ }

def Morphology.Realization.Hom.comp {F : Type u_3} {R₁ : Type u_6} {C₁ : Type u_7} {R₂ : Type u_8} {C₂ : Type u_9} {R₃ : Type u_10} {C₃ : Type u_11} {S₁ : Realization R₁ C₁ F} {S₂ : Realization R₂ C₂ F} {S₃ : Realization R₃ C₃ F} (g : S₂.Hom S₃) (f : S₁.Hom S₂) : S₁.Hom S₃

Homs compose: coarsenings chain (morph-level to lexeme-level to √-level).

Equations

• g.comp f = { onRoot := fun (r : R₁) => g.onRoot (f.onRoot r), onCtx := fun (r : R₁) (c : C₁) => g.onCtx (f.onRoot r) (f.onCtx r c), realize_eq := ⋯ }

theorem Morphology.Realization.Hom.isLicensed {F : Type u_3} {R₁ : Type u_6} {C₁ : Type u_7} {R₂ : Type u_8} {C₂ : Type u_9} {S : Realization R₁ C₁ F} {T : Realization R₂ C₂ F} (φ : S.Hom T) {r : R₁} {c : C₁} (h : S.IsLicensed r c) : T.IsLicensed (φ.onRoot r) (φ.onCtx r c)

Homs preserve licensing.

theorem Morphology.Realization.Hom.realizes {F : Type u_3} {R₁ : Type u_6} {C₁ : Type u_7} {R₂ : Type u_8} {C₂ : Type u_9} {S : Realization R₁ C₁ F} {T : Realization R₂ C₂ F} (φ : S.Hom T) {r : R₁} {f : F} (h : S.Realizes r f) : T.Realizes (φ.onRoot r) f

Homs preserve realization: merging indices can only grow allomorph sets.

structure Morphology.Realization.Interpreted (R : Type u_6) (Ctx : Type u_7) (F : Type u_8) (M : Type u_9) extends Morphology.Realization R Ctx F : Type (max (max (max u_6 u_7) u_8) u_9)

The two-map extension ([Mar97]: spellout is List 2, interp List 3 — allosemy, DM/Allosemy.lean). A [Bor13]-style system stays a bare System; a lexicalist lexeme is an Interpreted system whose interpretation is IsIntrinsic.

• realize : R → Ctx → Finset F
• interp : R → Ctx → Finset M

  Contextual interpretation: Encyclopedia access.

def Morphology.Realization.Interpreted.IsIntrinsic {R : Type u_1} {Ctx : Type u_2} {F : Type u_3} {M : Type u_4} (S : Interpreted R Ctx F M) (r : R) : Prop

One meaning in every context: the lexicalist degenerate case.

Equations

• S.IsIntrinsic r = Morphology.IsConstantIn S.interp r

def Morphology.Realization.Interpreted.IsAllosemous {R : Type u_1} {Ctx : Type u_2} {F : Type u_3} {M : Type u_4} (S : Interpreted R Ctx F M) (r : R) : Prop

Context-dependent interpretation: DM allosemy, its failure.

Equations

• S.IsAllosemous r = Morphology.IsVariantIn S.interp r

theorem Morphology.Realization.Interpreted.not_isIntrinsic_of_isAllosemous {R : Type u_1} {Ctx : Type u_2} {F : Type u_3} {M : Type u_4} (S : Interpreted R Ctx F M) {r : R} (h : S.IsAllosemous r) : ¬S.IsIntrinsic r

An allosemous root has no intrinsic meaning.

@[implicit_reducible]

instance Morphology.Realization.Interpreted.instDecidableIsIntrinsicOfFintypeOfDecidableEq {R : Type u_1} {Ctx : Type u_2} {F : Type u_3} {M : Type u_4} (S : Interpreted R Ctx F M) [Fintype Ctx] [DecidableEq M] (r : R) : Decidable (S.IsIntrinsic r)

Equations

• S.instDecidableIsIntrinsicOfFintypeOfDecidableEq r = Morphology.Realization.Interpreted.instDecidableIsIntrinsicOfFintypeOfDecidableEq._aux_1 S r

@[implicit_reducible]

instance Morphology.Realization.Interpreted.instDecidableIsAllosemousOfFintypeOfDecidableEq {R : Type u_1} {Ctx : Type u_2} {F : Type u_3} {M : Type u_4} (S : Interpreted R Ctx F M) [Fintype Ctx] [DecidableEq M] (r : R) : Decidable (S.IsAllosemous r)

Equations

• S.instDecidableIsAllosemousOfFintypeOfDecidableEq r = Morphology.Realization.Interpreted.instDecidableIsAllosemousOfFintypeOfDecidableEq._aux_1 S r

structure Morphology.Realization.Interpreted.Hom {F : Type u_3} {M : Type u_4} {R₁ : Type u_6} {C₁ : Type u_7} {R₂ : Type u_8} {C₂ : Type u_9} (S : Interpreted R₁ C₁ F M) (T : Interpreted R₂ C₂ F M) : Type (max (max (max u_6 u_7) u_8) u_9)

The strict tier of hom, on which individuation disputes are stated: the context translation is root-independent — so the target context cannot re-encode the source index — and interpretation is preserved alongside spellout.

• onRoot : R₁ → R₂

  The index translation.

• onCtx : C₁ → C₂

  The root-independent context translation.

• realize_eq (r : R₁) (c : C₁) : S.realize r c = T.realize (self.onRoot r) (self.onCtx c)

  Realization is preserved.

• interp_eq (r : R₁) (c : C₁) : S.interp r c = T.interp (self.onRoot r) (self.onCtx c)

  Interpretation is preserved.

def Morphology.Realization.Interpreted.Hom.toRealizationHom {F : Type u_3} {M : Type u_4} {R₁ : Type u_6} {C₁ : Type u_7} {R₂ : Type u_8} {C₂ : Type u_9} {S : Interpreted R₁ C₁ F M} {T : Interpreted R₂ C₂ F M} (φ : S.Hom T) : S.Hom T.toRealization

A strict hom is in particular a realization hom.

Equations

• φ.toRealizationHom = { onRoot := φ.onRoot, onCtx := fun (x : R₁) (c : C₁) => φ.onCtx c, realize_eq := ⋯ }

theorem Morphology.Realization.Interpreted.Hom.interp_eq_of_onRoot_eq {F : Type u_3} {M : Type u_4} {R₁ : Type u_6} {C₁ : Type u_7} {R₂ : Type u_8} {C₂ : Type u_9} {S : Interpreted R₁ C₁ F M} {T : Interpreted R₂ C₂ F M} (φ : S.Hom T) {r r' : R₁} (h : φ.onRoot r = φ.onRoot r') (c : C₁) : S.interp r c = S.interp r' c

Merged roots agree contextwise in interpretation — the keystone separating identity from accidental homophony: a strict hom identifying two indices forces their interpretations to coincide in every context, so bank₁/bank₂ never merge.

theorem Morphology.Realization.Interpreted.Hom.realize_eq_of_onRoot_eq {F : Type u_3} {M : Type u_4} {R₁ : Type u_6} {C₁ : Type u_7} {R₂ : Type u_8} {C₂ : Type u_9} {S : Interpreted R₁ C₁ F M} {T : Interpreted R₂ C₂ F M} (φ : S.Hom T) {r r' : R₁} (h : φ.onRoot r = φ.onRoot r') (c : C₁) : S.realize r c = S.realize r' c

The realization analog of interp_eq_of_onRoot_eq: merged roots agree contextwise in realization. Unavailable for the transport tier Realization.Hom, whose index-dependent context translation can separate the merged roots' contexts.

structure Morphology.Realization.Interpreted.LaxHom {F : Type u_3} {M : Type u_4} {R₁ : Type u_6} {C₁ : Type u_7} {R₂ : Type u_8} {C₂ : Type u_9} (S : Interpreted R₁ C₁ F M) (T : Interpreted R₂ C₂ F M) : Type (max (max (max u_6 u_7) u_8) u_9)

The lax tier: realization and interpretation are included rather than matched. Where a strict Hom merger asserts identity, a lax merger asserts subsumption — each source index's forms and readings are among its image's, as when a lexeme's listed properties are among its root's Encyclopedia entry ([Ara05]). Pattern-bound lexemes lax-merge into a total root without ever strict-merging.

• onRoot : R₁ → R₂

  The index translation.

• onCtx : C₁ → C₂

  The root-independent context translation.

• realize_sub (r : R₁) (c : C₁) : S.realize r c ⊆ T.realize (self.onRoot r) (self.onCtx c)

  Realizations are included.

• interp_sub (r : R₁) (c : C₁) : S.interp r c ⊆ T.interp (self.onRoot r) (self.onCtx c)

  Interpretations are included.

def Morphology.Realization.Interpreted.Hom.toLaxHom {F : Type u_3} {M : Type u_4} {R₁ : Type u_6} {C₁ : Type u_7} {R₂ : Type u_8} {C₂ : Type u_9} {S : Interpreted R₁ C₁ F M} {T : Interpreted R₂ C₂ F M} (φ : S.Hom T) : S.LaxHom T

A strict hom is in particular lax.

Equations

• φ.toLaxHom = { onRoot := φ.onRoot, onCtx := φ.onCtx, realize_sub := ⋯, interp_sub := ⋯ }

def Morphology.Realization.Interpreted.LaxHom.comp {F : Type u_3} {M : Type u_4} {R₁ : Type u_6} {C₁ : Type u_7} {R₂ : Type u_8} {C₂ : Type u_9} {R₃ : Type u_10} {C₃ : Type u_11} {S₁ : Interpreted R₁ C₁ F M} {S₂ : Interpreted R₂ C₂ F M} {S₃ : Interpreted R₃ C₃ F M} (g : S₂.LaxHom S₃) (f : S₁.LaxHom S₂) : S₁.LaxHom S₃

Lax homs compose.

Equations

• g.comp f = { onRoot := fun (r : R₁) => g.onRoot (f.onRoot r), onCtx := fun (c : C₁) => g.onCtx (f.onCtx c), realize_sub := ⋯, interp_sub := ⋯ }

def Morphology.Realization.Interpreted.ProfileEq {R : Type u_1} {Ctx : Type u_2} {F : Type u_3} {M : Type u_4} (S : Interpreted R Ctx F M) (r r' : R) : Prop

Contextwise indistinguishability of indices: equal realization and interpretation profiles.

Equations

• S.ProfileEq r r' = ((∀ (c : Ctx), S.realize r c = S.realize r' c) ∧ ∀ (c : Ctx), S.interp r c = S.interp r' c)

def Morphology.Realization.Interpreted.profileSetoid {R : Type u_1} {Ctx : Type u_2} {F : Type u_3} {M : Type u_4} (S : Interpreted R Ctx F M) : Setoid R

Profile equality as a setoid.

Equations

• S.profileSetoid = { r := S.ProfileEq, iseqv := ⋯ }

def Morphology.Realization.Interpreted.reduce {R : Type u_1} {Ctx : Type u_2} {F : Type u_3} {M : Type u_4} (S : Interpreted R Ctx F M) : Interpreted (Quotient S.profileSetoid) Ctx F M

The reduced presentation: indices are realization-and-interpretation profiles. Every system presents its reduction; the strict hom tier is change of presentation, and only the lax tier merges beyond profiles.

Equations

• S.reduce = { realize := Quotient.lift S.realize ⋯, interp := Quotient.lift S.interp ⋯ }

def Morphology.Realization.Interpreted.reduceHom {R : Type u_1} {Ctx : Type u_2} {F : Type u_3} {M : Type u_4} (S : Interpreted R Ctx F M) : S.Hom S.reduce

Reduction is a strict hom: passing to profiles loses nothing.

Equations

• S.reduceHom = { onRoot := Quotient.mk S.profileSetoid, onCtx := id, realize_eq := ⋯, interp_eq := ⋯ }

theorem Morphology.Realization.Interpreted.Hom.profileEq_of_onRoot_eq {R : Type u_1} {Ctx : Type u_2} {F : Type u_3} {M : Type u_4} (S : Interpreted R Ctx F M) {R₂ : Type u_6} {C₂ : Type u_7} {T : Interpreted R₂ C₂ F M} (φ : S.Hom T) {r r' : R} (h : φ.onRoot r = φ.onRoot r') : S.ProfileEq r r'

Mergers along any strict hom refine profile equality: reduce merges as much as the strict tier ever can. Mergers beyond profiles — the hammer carvings, pattern-bound lexemes into an [Ara05] root — are necessarily lax.