@cite{baker-1985}: The Mirror Principle and Morphosyntactic Explanation

@cite{baker-1985}

This study file verifies the Mirror Principle's predictions against data from Chamorro, Quechua, and Bantu languages, as presented in @cite{baker-1985}.

Structure

• §0: Mirror-Principle substrate (was Theories/Morphology/Core/ MirrorPrinciple.lean; relocated 0.230.455 — Baker is the founding paper, anchor lives here per CLAUDE.md "every file is anchored").
• §1: Chamorro — passive, causative, and number agreement interactions (§§1, 3.1 of the paper)
• §2: Quechua — causative-reciprocal ordering determines interpretation (§4.1)
• §3: Bantu and Huichol — passive-applicative affix ordering (§4.2)
• §4: Cross-linguistic verification of the Agreement Restriction (§3.2)

"Morphological derivations must directly reflect syntactic derivations (and vice versa)." (@cite{baker-1985} (4)) Each grammatical function changing rule (GF-rule) — passive, causative, applicative, reflexive/ reciprocal — simultaneously adds an affix to the verb and changes the grammatical functions of arguments. The Mirror Principle requires the morphological ordering (affix layering) to match the syntactic ordering (rule application sequence).

@cite{baker-1985} §6 argues the Mirror Principle should not be a stipulation but follow from the architecture: in a framework where GF-rules are a single process with both effects, mirroring is by construction. Formalized below via DerivationStep.

inductive Morphology.MirrorPrinciple.GFRuleType : Type

Grammatical function changing rules (GF-rules). @cite{baker-1985} §§2-4.

• passive : GFRuleType
• causative : GFRuleType
• applicative : GFRuleType
• reflexReciprocal : GFRuleType

@[implicit_reducible]

instance Morphology.MirrorPrinciple.instDecidableEqGFRuleType : DecidableEq GFRuleType

Equations

• Morphology.MirrorPrinciple.instDecidableEqGFRuleType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Morphology.MirrorPrinciple.instReprGFRuleType.repr : GFRuleType → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance Morphology.MirrorPrinciple.instReprGFRuleType : Repr GFRuleType

Equations

• Morphology.MirrorPrinciple.instReprGFRuleType = { reprPrec := Morphology.MirrorPrinciple.instReprGFRuleType.repr }

def Morphology.MirrorPrinciple.instBEqGFRuleType.beq : GFRuleType → GFRuleType → Bool

Equations

• Morphology.MirrorPrinciple.instBEqGFRuleType.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

@[implicit_reducible]

instance Morphology.MirrorPrinciple.instBEqGFRuleType : BEq GFRuleType

Equations

• Morphology.MirrorPrinciple.instBEqGFRuleType = { beq := Morphology.MirrorPrinciple.instBEqGFRuleType.beq }

def Morphology.MirrorPrinciple.GFRuleType.toMorphCategory : GFRuleType → Core.Morphology.MorphCategory

Map GF-rules to @cite{bybee-1985}'s morphological categories.

Equations

• Morphology.MirrorPrinciple.GFRuleType.passive.toMorphCategory = Core.Morphology.MorphCategory.voice
• Morphology.MirrorPrinciple.GFRuleType.causative.toMorphCategory = Core.Morphology.MorphCategory.valence
• Morphology.MirrorPrinciple.GFRuleType.applicative.toMorphCategory = Core.Morphology.MorphCategory.valence
• Morphology.MirrorPrinciple.GFRuleType.reflexReciprocal.toMorphCategory = Core.Morphology.MorphCategory.valence

structure Morphology.MirrorPrinciple.DerivationStep : Type

A single step bundling morphological + syntactic effects. By bundling, the Mirror Principle holds by construction.

• rule : GFRuleType
• affix : String
• isPrefix : Bool

@[implicit_reducible]

instance Morphology.MirrorPrinciple.instDecidableEqDerivationStep : DecidableEq DerivationStep

Equations

• Morphology.MirrorPrinciple.instDecidableEqDerivationStep = Morphology.MirrorPrinciple.instDecidableEqDerivationStep.decEq

def Morphology.MirrorPrinciple.instDecidableEqDerivationStep.decEq (x✝ x✝¹ : DerivationStep) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.

def Morphology.MirrorPrinciple.instReprDerivationStep.repr : DerivationStep → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance Morphology.MirrorPrinciple.instReprDerivationStep : Repr DerivationStep

Equations

• Morphology.MirrorPrinciple.instReprDerivationStep = { reprPrec := Morphology.MirrorPrinciple.instReprDerivationStep.repr }

@[implicit_reducible]

instance Morphology.MirrorPrinciple.instBEqDerivationStep : BEq DerivationStep

Equations

• Morphology.MirrorPrinciple.instBEqDerivationStep = { beq := Morphology.MirrorPrinciple.instBEqDerivationStep.beq }

def Morphology.MirrorPrinciple.instBEqDerivationStep.beq : DerivationStep → DerivationStep → Bool

Equations

• Morphology.MirrorPrinciple.instBEqDerivationStep.beq { rule := a, affix := a_1, isPrefix := a_2 } { rule := b, affix := b_1, isPrefix := b_2 } = (a == b && (a_1 == b_1 && a_2 == b_2))
• Morphology.MirrorPrinciple.instBEqDerivationStep.beq x✝¹ x✝ = false

@[reducible, inline]

abbrev Morphology.MirrorPrinciple.Derivation : Type

Steps ordered first-applied (innermost) to last-applied (outermost).

Equations

• Morphology.MirrorPrinciple.Derivation = List Morphology.MirrorPrinciple.DerivationStep

def Morphology.MirrorPrinciple.ruleOrder (d : Derivation) : List GFRuleType

Equations

• Morphology.MirrorPrinciple.ruleOrder d = List.map (fun (x : Morphology.MirrorPrinciple.DerivationStep) => x.rule) d

def Morphology.MirrorPrinciple.affixOrder (d : Derivation) : List String

Equations

• Morphology.MirrorPrinciple.affixOrder d = List.map (fun (x : Morphology.MirrorPrinciple.DerivationStep) => x.affix) d

theorem Morphology.MirrorPrinciple.mirror_by_construction (d : Derivation) : (ruleOrder d).length = (affixOrder d).length

The orderings are isomorphic by construction — the Mirror Principle.

inductive Morphology.MirrorPrinciple.AgreementPosition : Type

• inner : AgreementPosition
• outer : AgreementPosition

@[implicit_reducible]

instance Morphology.MirrorPrinciple.instDecidableEqAgreementPosition : DecidableEq AgreementPosition

Equations

• Morphology.MirrorPrinciple.instDecidableEqAgreementPosition x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Morphology.MirrorPrinciple.instReprAgreementPosition : Repr AgreementPosition

Equations

• Morphology.MirrorPrinciple.instReprAgreementPosition = { reprPrec := Morphology.MirrorPrinciple.instReprAgreementPosition.repr }

def Morphology.MirrorPrinciple.instReprAgreementPosition.repr : AgreementPosition → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance Morphology.MirrorPrinciple.instBEqAgreementPosition : BEq AgreementPosition

Equations

• Morphology.MirrorPrinciple.instBEqAgreementPosition = { beq := Morphology.MirrorPrinciple.instBEqAgreementPosition.beq }

def Morphology.MirrorPrinciple.instBEqAgreementPosition.beq : AgreementPosition → AgreementPosition → Bool

Equations

• Morphology.MirrorPrinciple.instBEqAgreementPosition.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

inductive Morphology.MirrorPrinciple.GFReference : Type

• semantic : GFReference
• surface : GFReference

@[implicit_reducible]

instance Morphology.MirrorPrinciple.instDecidableEqGFReference : DecidableEq GFReference

Equations

• Morphology.MirrorPrinciple.instDecidableEqGFReference x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Morphology.MirrorPrinciple.instReprGFReference.repr : GFReference → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance Morphology.MirrorPrinciple.instReprGFReference : Repr GFReference

Equations

• Morphology.MirrorPrinciple.instReprGFReference = { reprPrec := Morphology.MirrorPrinciple.instReprGFReference.repr }

@[implicit_reducible]

instance Morphology.MirrorPrinciple.instBEqGFReference : BEq GFReference

Equations

• Morphology.MirrorPrinciple.instBEqGFReference = { beq := Morphology.MirrorPrinciple.instBEqGFReference.beq }

def Morphology.MirrorPrinciple.instBEqGFReference.beq : GFReference → GFReference → Bool

Equations

• Morphology.MirrorPrinciple.instBEqGFReference.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

structure Morphology.MirrorPrinciple.AgreementPattern : Type

• position : AgreementPosition
• reference : GFReference

def Morphology.MirrorPrinciple.instDecidableEqAgreementPattern.decEq (x✝ x✝¹ : AgreementPattern) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance Morphology.MirrorPrinciple.instDecidableEqAgreementPattern : DecidableEq AgreementPattern

Equations

• Morphology.MirrorPrinciple.instDecidableEqAgreementPattern = Morphology.MirrorPrinciple.instDecidableEqAgreementPattern.decEq

def Morphology.MirrorPrinciple.instReprAgreementPattern.repr : AgreementPattern → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance Morphology.MirrorPrinciple.instReprAgreementPattern : Repr AgreementPattern

Equations

• Morphology.MirrorPrinciple.instReprAgreementPattern = { reprPrec := Morphology.MirrorPrinciple.instReprAgreementPattern.repr }

@[implicit_reducible]

instance Morphology.MirrorPrinciple.instBEqAgreementPattern : BEq AgreementPattern

Equations

• Morphology.MirrorPrinciple.instBEqAgreementPattern = { beq := Morphology.MirrorPrinciple.instBEqAgreementPattern.beq }

def Morphology.MirrorPrinciple.instBEqAgreementPattern.beq : AgreementPattern → AgreementPattern → Bool

Equations

• Morphology.MirrorPrinciple.instBEqAgreementPattern.beq { position := a, reference := a_1 } { position := b, reference := b_1 } = (a == b && a_1 == b_1)
• Morphology.MirrorPrinciple.instBEqAgreementPattern.beq x✝¹ x✝ = false

def Morphology.MirrorPrinciple.deriveReference : AgreementPosition → GFReference

Inner position → pre-rule (semantic) GFs; outer → post-rule (surface).

Equations

• Morphology.MirrorPrinciple.deriveReference Morphology.MirrorPrinciple.AgreementPosition.inner = Morphology.MirrorPrinciple.GFReference.semantic
• Morphology.MirrorPrinciple.deriveReference Morphology.MirrorPrinciple.AgreementPosition.outer = Morphology.MirrorPrinciple.GFReference.surface

def Morphology.MirrorPrinciple.AgreementPattern.isAttested (p : AgreementPattern) : Bool

Equations

• p.isAttested = (p.reference == Morphology.MirrorPrinciple.deriveReference p.position)

theorem Morphology.MirrorPrinciple.inner_semantic_attested : { position := AgreementPosition.inner, reference := GFReference.semantic }.isAttested = true

theorem Morphology.MirrorPrinciple.outer_surface_attested : { position := AgreementPosition.outer, reference := GFReference.surface }.isAttested = true

theorem Morphology.MirrorPrinciple.outer_semantic_unattested : { position := AgreementPosition.outer, reference := GFReference.semantic }.isAttested = false

theorem Morphology.MirrorPrinciple.inner_surface_unattested : { position := AgreementPosition.inner, reference := GFReference.surface }.isAttested = false

theorem Morphology.MirrorPrinciple.agreement_restriction_count : (List.filter (fun (x : AgreementPattern) => x.isAttested) [{ position := AgreementPosition.inner, reference := GFReference.semantic }, { position := AgreementPosition.outer, reference := GFReference.semantic }, { position := AgreementPosition.inner, reference := GFReference.surface }, { position := AgreementPosition.outer, reference := GFReference.surface }]).length = 2

Exactly two of four patterns are attested (Baker (27)).

theorem Morphology.MirrorPrinciple.attested_are_27a_and_27d : List.filter (fun (x : AgreementPattern) => x.isAttested) [{ position := AgreementPosition.inner, reference := GFReference.semantic }, { position := AgreementPosition.outer, reference := GFReference.semantic }, { position := AgreementPosition.inner, reference := GFReference.surface }, { position := AgreementPosition.outer, reference := GFReference.surface }] = [{ position := AgreementPosition.inner, reference := GFReference.semantic }, { position := AgreementPosition.outer, reference := GFReference.surface }]

theorem Morphology.MirrorPrinciple.derived_reference_attested (pos : AgreementPosition) : { position := pos, reference := deriveReference pos }.isAttested = true

def Morphology.MirrorPrinciple.GFRuleType.Feeds (r1 r2 : GFRuleType) : Prop

Applicative feeds passive: appl creates the DO that passive promotes.

Equations

• r1.Feeds r2 = (r1 = Morphology.MirrorPrinciple.GFRuleType.applicative ∧ r2 = Morphology.MirrorPrinciple.GFRuleType.passive)

@[implicit_reducible]

instance Morphology.MirrorPrinciple.instDecidableRelGFRuleTypeFeeds : DecidableRel GFRuleType.Feeds

Equations

• Morphology.MirrorPrinciple.instDecidableRelGFRuleTypeFeeds x✝¹ x✝ = id inferInstance

def Morphology.MirrorPrinciple.feedingOrder (feeder fed : GFRuleType) : List GFRuleType

Equations

• Morphology.MirrorPrinciple.feedingOrder feeder fed = [feeder, fed]

theorem Morphology.MirrorPrinciple.appl_feeds_passive : GFRuleType.applicative.Feeds GFRuleType.passive

theorem Morphology.MirrorPrinciple.appl_pass_predicted : feedingOrder GFRuleType.applicative GFRuleType.passive = [GFRuleType.applicative, GFRuleType.passive]

inductive Morphology.MirrorPrinciple.MorphDomain : Type

The morphological domain of the Mirror Principle. @cite{baker-1985} §5.

• concatenative : MorphDomain
• cliticization : MorphDomain
• nonconcatenative : MorphDomain

@[implicit_reducible]

instance Morphology.MirrorPrinciple.instDecidableEqMorphDomain : DecidableEq MorphDomain

Equations

• Morphology.MirrorPrinciple.instDecidableEqMorphDomain x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Morphology.MirrorPrinciple.instReprMorphDomain : Repr MorphDomain

Equations

• Morphology.MirrorPrinciple.instReprMorphDomain = { reprPrec := Morphology.MirrorPrinciple.instReprMorphDomain.repr }

def Morphology.MirrorPrinciple.instReprMorphDomain.repr : MorphDomain → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.

def Morphology.MirrorPrinciple.MorphDomain.InScope (d : MorphDomain) : Prop

Equations

• d.InScope = (d = Morphology.MirrorPrinciple.MorphDomain.concatenative)

@[implicit_reducible]

instance Morphology.MirrorPrinciple.instDecidablePredMorphDomainInScope : DecidablePred MorphDomain.InScope

Equations

• Morphology.MirrorPrinciple.instDecidablePredMorphDomainInScope d = id inferInstance

theorem Morphology.MirrorPrinciple.gfRule_inside_agreement (r : GFRuleType) : r.toMorphCategory.peripherality < (Core.Morphology.MorphCategory.agreement Core.Agreement.Controller.subj).peripherality

GF-rule morphemes are inside agreement per Bybee's hierarchy.

def Baker1985.chamorroPassiveAgreement : Morphology.MirrorPrinciple.AgreementPattern

Passive sentence: fan-in-saolak 'be spanked (pl)'.

Morphological structure: [fan [in [saolak]]] fan- (agreement) is OUTSIDE -in- (passive).

By the Mirror Principle, fan- was added after passive, so it references the post-passive (surface) subject — 'the children', the derived subject.

@cite{baker-1985} (15b), (21).

Equations

• Baker1985.chamorroPassiveAgreement = { position := Morphology.MirrorPrinciple.AgreementPosition.outer, reference := Morphology.MirrorPrinciple.GFReference.surface }

def Baker1985.chamorroCausativeAgreement : Morphology.MirrorPrinciple.AgreementPattern

Causative sentence: na'-fan-otchu 'make eat (pl)'.

Morphological structure: [na' [fan [otchu]]] fan- (agreement) is INSIDE na'- (causative).

By the Mirror Principle, fan- was added before causative, so it references the pre-causative (semantic) subject — the underlying subject of 'eat'.

@cite{baker-1985} (15c), (23).

Equations

• Baker1985.chamorroCausativeAgreement = { position := Morphology.MirrorPrinciple.AgreementPosition.inner, reference := Morphology.MirrorPrinciple.GFReference.semantic }

theorem Baker1985.chamorro_passive_attested : chamorroPassiveAgreement.isAttested = true

Both Chamorro agreement patterns are attested.

theorem Baker1985.chamorro_causative_attested : chamorroCausativeAgreement.isAttested = true

theorem Baker1985.chamorro_shows_both_attested : chamorroPassiveAgreement.isAttested = true ∧ chamorroCausativeAgreement.isAttested = true

Chamorro exhibits both attested patterns in a single language, confirming the Agreement Restriction is a property of UG, not a language-specific parameter. @cite{baker-1985} §3.1.

def Baker1985.chamorroCausativePassive : Morphology.MirrorPrinciple.Derivation

Causative of passive: na'-fan-s-in-aolak 'I had the children spanked by their father.'

Morphological structure: [na' [fan [in [saolak]]]] Derivation order: passive first, then causative. fan- is between them — added after passive, before causative. → References the intermediate subject (post-passive, pre-causative) = 'the children' (the derived subject of the passive).

@cite{baker-1985} (25), (26).

Equations

• One or more equations did not get rendered due to their size.

theorem Baker1985.chamorro_passive_before_causative : Morphology.MirrorPrinciple.ruleOrder chamorroCausativePassive = [Morphology.MirrorPrinciple.GFRuleType.passive, Morphology.MirrorPrinciple.GFRuleType.causative]

Quechua causative-reciprocal interactions

Quechua shows that causative -chi and reciprocal -naku can appear in either order on the verb, with different interpretations that the Mirror Principle correctly predicts. The difference in morpheme ordering corresponds to a difference in which arguments are bound by the reciprocal, which follows from the different syntactic derivation orders.

@cite{baker-1985} §4.1.

def Baker1985.quechuaRecipInsideCaus : Morphology.MirrorPrinciple.Derivation

Reciprocal inside causative: maqa-naku-ya-chi-n 'He is causing them to beat each other.'

Morpheme order (inner→outer): root, -naku (recip), -chi (caus) Mirror Principle: reciprocal applied first, then causative. → Reciprocal binds agent and patient of root verb → Causative adds a new causer → Causer causes [reciprocal beating]

@cite{baker-1985} (39a), (45)–(46).

Equations

• One or more equations did not get rendered due to their size.

def Baker1985.quechuaCausInsideRecip : Morphology.MirrorPrinciple.Derivation

Causative inside reciprocal: maqa-chi-naku-rka-n 'They let someone beat each other.'

Morpheme order (inner→outer): root, -chi (caus), -naku (recip) Mirror Principle: causative applied first, then reciprocal. → Causative adds a causer first → Reciprocal then binds the causer and the patient → The causers reciprocally [let someone beat them]

@cite{baker-1985} (39b), (47)–(48).

Equations

• One or more equations did not get rendered due to their size.

theorem Baker1985.quechua_recip_caus_order : Morphology.MirrorPrinciple.ruleOrder quechuaRecipInsideCaus = [Morphology.MirrorPrinciple.GFRuleType.reflexReciprocal, Morphology.MirrorPrinciple.GFRuleType.causative]

Reciprocal-inside-causative: reciprocal applies first.

theorem Baker1985.quechua_caus_recip_order : Morphology.MirrorPrinciple.ruleOrder quechuaCausInsideRecip = [Morphology.MirrorPrinciple.GFRuleType.causative, Morphology.MirrorPrinciple.GFRuleType.reflexReciprocal]

Causative-inside-reciprocal: causative applies first.

theorem Baker1985.quechua_orderings_differ : Morphology.MirrorPrinciple.ruleOrder quechuaRecipInsideCaus ≠ Morphology.MirrorPrinciple.ruleOrder quechuaCausInsideRecip

Different morpheme orderings produce different syntactic orderings and hence different interpretations. The Mirror Principle links all three: morpheme order ↔ syntactic order ↔ interpretation.

Passive-applicative interactions

When both passive and applicative appear on the same verb, the applicative morpheme is universally closer to the root. The Mirror Principle predicts this: applicative creates a new direct object that passive can then promote to subject, so applicative must apply first (its affix is inner).

Attested: V-appl-pass Not attested: *V-pass-appl (for oblique-to-subject promotion)

@cite{baker-1985} §4.2.

def Baker1985.chiMwini : Morphology.MirrorPrinciple.Derivation

Chi-Mwi:ni: tet-el-el-a 'bring-appl-asp-pass' Applicative -el closer to root than passive. @cite{baker-1985} (56c).

Equations

• Baker1985.chiMwini = [{ rule := Morphology.MirrorPrinciple.GFRuleType.applicative, affix := "-el" }, { rule := Morphology.MirrorPrinciple.GFRuleType.passive, affix := "-a" }]

def Baker1985.kinyarwanda : Morphology.MirrorPrinciple.Derivation

Kinyarwanda: andik-iish-w-a 'write-instr-pass-asp' Applicative -iish closer to root than passive -w. @cite{baker-1985} (57c).

Equations

• Baker1985.kinyarwanda = [{ rule := Morphology.MirrorPrinciple.GFRuleType.applicative, affix := "-iish" }, { rule := Morphology.MirrorPrinciple.GFRuleType.passive, affix := "-w" }]

def Baker1985.huichol : Morphology.MirrorPrinciple.Derivation

Huichol: puutinanai-ri-yeri 'buy-ben-pass' Benefactive-applicative -ri closer to root than passive -yeri. @cite{baker-1985} (55).

Equations

• Baker1985.huichol = [{ rule := Morphology.MirrorPrinciple.GFRuleType.applicative, affix := "-ri" }, { rule := Morphology.MirrorPrinciple.GFRuleType.passive, affix := "-yeri" }]

theorem Baker1985.all_appl_before_pass : Morphology.MirrorPrinciple.ruleOrder chiMwini = [Morphology.MirrorPrinciple.GFRuleType.applicative, Morphology.MirrorPrinciple.GFRuleType.passive] ∧ Morphology.MirrorPrinciple.ruleOrder kinyarwanda = [Morphology.MirrorPrinciple.GFRuleType.applicative, Morphology.MirrorPrinciple.GFRuleType.passive] ∧ Morphology.MirrorPrinciple.ruleOrder huichol = [Morphology.MirrorPrinciple.GFRuleType.applicative, Morphology.MirrorPrinciple.GFRuleType.passive]

All three languages show applicative before passive, as predicted by the Mirror Principle.

theorem Baker1985.all_match_feeding_prediction : Morphology.MirrorPrinciple.GFRuleType.applicative.Feeds Morphology.MirrorPrinciple.GFRuleType.passive ∧ Morphology.MirrorPrinciple.ruleOrder chiMwini = [Morphology.MirrorPrinciple.GFRuleType.applicative, Morphology.MirrorPrinciple.GFRuleType.passive] ∧ Morphology.MirrorPrinciple.ruleOrder kinyarwanda = [Morphology.MirrorPrinciple.GFRuleType.applicative, Morphology.MirrorPrinciple.GFRuleType.passive] ∧ Morphology.MirrorPrinciple.ruleOrder huichol = [Morphology.MirrorPrinciple.GFRuleType.applicative, Morphology.MirrorPrinciple.GFRuleType.passive]

All three languages show the order predicted by the feeding relationship: applicative feeds passive, so applicative is universally inner.

def Baker1985.bembaCausRecip : Morphology.MirrorPrinciple.Derivation

Bemba (Bantu) causative-reciprocal: Naa-mon-eshy-ana 'I made Mwape and Mutumba see each other.'

Bemba uses the Chamorro-type causative (underlying subject becomes oblique), unlike Quechua (underlying subject stays as object). This leads to different morpheme ordering for the same interpretation compared to Quechua — but the Mirror Principle still holds: the morpheme ordering reflects the syntactic derivation order.

In Bemba: causative precedes reciprocal morphologically, because Bemba's causative changes GFs differently: the new causer occupies the object position, so reciprocal must apply after causative to bind it.

@cite{baker-1985} (49), (52).

Equations

• Baker1985.bembaCausRecip = [{ rule := Morphology.MirrorPrinciple.GFRuleType.causative, affix := "-eshy" }, { rule := Morphology.MirrorPrinciple.GFRuleType.reflexReciprocal, affix := "-ana" }]

theorem Baker1985.bemba_caus_before_recip : Morphology.MirrorPrinciple.ruleOrder bembaCausRecip = [Morphology.MirrorPrinciple.GFRuleType.causative, Morphology.MirrorPrinciple.GFRuleType.reflexReciprocal]

The Agreement Restriction across languages

@cite{baker-1985} (27) predicts that of four logical possibilities for combining agreement position and GF reference, only two are attested cross-linguistically:

	Semantic GFs	Surface GFs
Inner	✓ (27a)	✗ (27c)
Outer	✗ (27b)	✓ (27d)

Evidence:

• (27a) inner + semantic: Chamorro causative fan-, Turkish, Sanskrit, Quechua (agreement closer to V, references underlying GFs)
• (27d) outer + surface: most agglutinative languages; Chamorro passive fan- (agreement farther from V, references surface GFs)

No clear cases of (27b) or (27c) have been found.

The Mirror Principle derives this restriction: morphological position determines derivational timing, and derivational timing determines which GFs are visible for agreement.

theorem Baker1985.mirror_derives_reference_inner : Morphology.MirrorPrinciple.deriveReference Morphology.MirrorPrinciple.AgreementPosition.inner = Morphology.MirrorPrinciple.GFReference.semantic

The Mirror Principle correctly derives the attested reference for each morphological position.

theorem Baker1985.mirror_derives_reference_outer : Morphology.MirrorPrinciple.deriveReference Morphology.MirrorPrinciple.AgreementPosition.outer = Morphology.MirrorPrinciple.GFReference.surface

theorem Baker1985.derived_always_attested (pos : Morphology.MirrorPrinciple.AgreementPosition) : { position := pos, reference := Morphology.MirrorPrinciple.deriveReference pos }.isAttested = true

Every derived pattern is attested; no stipulation is needed.

theorem Baker1985.chamorro_passive_is_derived : chamorroPassiveAgreement = { position := Morphology.MirrorPrinciple.AgreementPosition.outer, reference := Morphology.MirrorPrinciple.deriveReference Morphology.MirrorPrinciple.AgreementPosition.outer }

The Chamorro passive pattern is exactly the derived pattern for outer agreement.

theorem Baker1985.chamorro_causative_is_derived : chamorroCausativeAgreement = { position := Morphology.MirrorPrinciple.AgreementPosition.inner, reference := Morphology.MirrorPrinciple.deriveReference Morphology.MirrorPrinciple.AgreementPosition.inner }

The Chamorro causative pattern is exactly the derived pattern for inner agreement.

def Baker1985.acheneseAgreement : Morphology.MirrorPrinciple.AgreementPattern

Achenese (Austronesian) provides a test case: verbal agreement references the underlying (semantic) subject in both active and passive sentences, and Achenese has no overt passive morpheme. Since there is no GF-rule morpheme on the verb, the agreement morpheme is trivially "inner" (there is nothing for it to be outer to), and it references semantic GFs — consistent with pattern (27a). @cite{baker-1985} (31).

Equations

• Baker1985.acheneseAgreement = { position := Morphology.MirrorPrinciple.AgreementPosition.inner, reference := Morphology.MirrorPrinciple.GFReference.semantic }

theorem Baker1985.achenese_attested : acheneseAgreement.isAttested = true