Anderson (2006): Auxiliary Verb Constructions

@cite{anderson-2006} @cite{heine-1993}

Cross-linguistic typology of auxiliary verb constructions (AVCs): classification by inflectional distribution between auxiliary and lexical verb, with diachronic grounding in @cite{heine-1993}'s grammaticalization framework.

Key contributions formalized

1. Inflectional pattern typology (InflPattern from substrate): auxHeaded, lexHeaded, doubled, split, splitDoubled — defined in Typology/AuxiliaryVerbs.lean, verified per-datum here.
2. Semantic head invariant (Anderson p. 23, Table 3.1 p. 117): the lexical verb is always the semantic head, regardless of where inflection sits.
3. Typed inflectional distribution: InflDistribution (from Core.Morphology) records which MorphCategory values each element hosts.
4. Grammaticalization grounding: Anderson ch. 7 traces AVCs onto Heine 1993's cline (Anderson p. 5: "According to Heine (1993: 48ff.)..."). The cline lives in Theories/Diachronic/Grammaticalization.lean, anchored on @cite{heine-1993} ch. 3.

Coverage

Sample of 9 AVC datums across 7 languages, covering all 5 patterns:

• English have eaten (aux-headed) — Anderson ch. 2 canonical example
• Doyayo lex-headed (Anderson ch. 3 ex. 15a, p. 121)
• Doyayo split/doubled (Anderson ch. 5 ex. 129, p. 223)
• Gorum (doubled)
• Jakaltek (split, abs/erg)
• Pipil split/doubled (Anderson ch. 5 ex. 133, p. 224)
• Pipil lex-headed (Anderson p. 220-221 fn. 6, with weli)
• Finnish split (negative auxiliary ei) @cite{karlsson-2017}
• Hemba split/doubled

2026-04-30 audit fixes

PDF-verified against Anderson 2006 (book pp. 5, 114, 117, 121, 224) and Heine 1993 (book p. 48ff. via Anderson p. 5):

• Doyayo .split → .lexHeaded (Ch 3 ex. 15a) + new doyayoSplitDoubled (Ch 5 ex. 129). Anderson never classifies Doyayo as plain split.
• Pipil .split → .splitDoubled (Ch 5 ex. 133, with subjects doubly marked). Fragment splitDistribution corrected to put .agreement on AUX (matches the gloss 1-AUX 1-2PL-show).
• Cline reattributed to @cite{heine-1993} (Anderson p. 5 explicitly cites Heine 1993:48ff.). Substrate GramStage.toMorphStatus projection moved to Theories/Diachronic/Grammaticalization.lean.
• negStrategyStage moved to NegativeAuxiliaries.lean as NegStrategy.toGramStage : NegStrategy → Option GramStage, with .negParticle => none (not on the verbal cline) — fixes the earlier formaliser-introduced collapse of @cite{miestamo-2005}'s particle-vs-verb distinction.
• Dropped Table 2.3 reference: Anderson's Table 2.3 (p. 114) catalogs non-finite forms within AUX-headed AVCs (a single- pattern grid of language exemplars), not a cross-pattern prediction. The pattern→LV-form prediction lives in Ch 2-5 prose, not in any single table.
• English exemplar: switched from will go (modal) to have eaten (perfect) as Anderson's canonical Ch 2 AUX-headed example; gloss corrected from FUT (non-Andersonian for will) to AUX.PRS + PTCP.
• 9× native_decide → decide: structural reduction is tractable; native_decide bypasses the kernel.
• finnish_form_from_paradigm: paired with finnish_1sg_in_paradigm witness lemma, now provably grounded in the Fragment paradigm rather than passing through the dead none fallback branch.
• Sorace bridge chains through @cite{sorace-2000}'s vendlerClassToTypicalTransitivity for a 2-step Vendler → TransitivityClass derivation.
• Cross-framework theorem anderson_miestamo_agree_on_neg_morphology documents the corrected mapping that preserves Miestamo's particle-vs-verb distinction.

Per-language AVC data

The 9 sample datums (7 languages) covering all 5 of Anderson's inflectional patterns. Per-datum verification theorems below ensure each datum's inflPattern and form/distribution derive from the Fragment files (changing a Fragment entry breaks exactly one theorem).

def Anderson2006.english : Typology.AuxiliaryVerbs.AVCDatum

English have eaten — aux-headed (AUX have carries tense and agreement, LV eaten is a past participle). Anderson ch. 2 (p. 40) describes English perfects schematically as have V-ed; the specific have eaten form is this file's instantiation of that pattern, not a verbatim Anderson example.

Equations

• Anderson2006.english = { language := "English", form := "have eaten", inflPattern := Typology.AuxiliaryVerbs.InflPattern.auxHeaded, gloss := "AUX.PRS eat.PTCP" }

def Anderson2006.doyayo : Typology.AuxiliaryVerbs.AVCDatum

Doyayo lex-headed (Anderson Ch 3 ex. 15a, p. 121). mi¹ (gi²) kpel¹-ko¹ 'I'm going to pour'. Auxiliary gi² uninflected (parenthesized in Anderson's gloss); LV carries proximate-future TAM. Form derived from Fragments.Doyayo.AuxiliaryVerbs.lexHeadedForm.

Equations

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

def Anderson2006.doyayoSplitDoubled : Typology.AuxiliaryVerbs.AVCDatum

Doyayo split/doubled (Anderson Ch 5 ex. 129, p. 223). hi¹-za¹ hi¹-zaa³ hi¹-lɔ-mɔ 'they might come bite you'. Subject hi¹ doubly marked on AUX and LV; object -mɔ only on LV. Anderson p. 223: "this pattern... is common in Doyayo."

Equations

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

def Anderson2006.gorum : Typology.AuxiliaryVerbs.AVCDatum

Gorum (doubled): subject + TAM on both AUX and LV. Form derived from Fragments.Gorum.AuxiliaryVerbs.

Equations

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

def Anderson2006.jakaltek : Typology.AuxiliaryVerbs.AVCDatum

Jakaltek (split): absolutive on AUX, ergative on LV. Form derived from Fragments.Jakaltek.AuxiliaryVerbs.

Equations

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

def Anderson2006.pipilSplitDoubled : Typology.AuxiliaryVerbs.AVCDatum

Pipil split/doubled (Anderson Ch 5 ex. 133b, p. 224). n-yu ni-mitsin-ilwitia 'I'm going to show you'. Subject 1 doubly marked (n- on AUX, ni- on LV); object -mitsin- only on LV. AUX root yu lexically encodes prospective TAM. Anderson p. 224: "Subjects are doubly marked... while objects occur only on lexical verbs."

Equations

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

def Anderson2006.pipilLexHeaded : Typology.AuxiliaryVerbs.AVCDatum

Pipil lex-headed (Anderson p. 220-221 fn. 6; Campbell 1985: 139). weli ni-nehnemi wehka 'I can walk far'. AUX weli uninflected; LV carries subject agreement. Anderson explicitly contrasts this with the split/doubled pattern in fn. 6 as a coexisting Pipil construction.

Equations

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

def Anderson2006.finnish : Typology.AuxiliaryVerbs.AVCDatum

Finnish negative auxiliary ei (split): person/number on aux, TAM on lexical verb (connegative form). Anderson §1.7.2 (p. 33-34) treats Uralic negative auxiliaries as a class spanning multiple AVC patterns — Udihe and Neyo as aux-headed, Kokota as split, Kwerba as lex-headed, 'Iipay as doubled. Finnish ei itself is not classified by Anderson in §1.7.2 with a specific pattern label; the split classification here follows @cite{karlsson-2017} §19.5 where the connegative suffix on the LV is the load-bearing diagnostic. The split nature derives from Fragments.Finnish.Negation.finnishNegDistribution: the negative auxiliary hosts negation, tense, and agreement, while the lexical verb retains stem and aspect. The 1sg neg-aux form derives from negParadigm; see the finnish_1sg_form_eq witness lemma for the strong pinning of the form-construction. Gloss style follows Anderson's Uralic convention (Neg-1 read-conneg).

Equations

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

def Anderson2006.hemba : Typology.AuxiliaryVerbs.AVCDatum

Hemba split/doubled: subject doubled on both AUX and LV; tense on AUX only; mood on LV only. Form derived from Fragments.Hemba.AuxiliaryVerbs.

Equations

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

def Anderson2006.allData : List Typology.AuxiliaryVerbs.AVCDatum

All 9 AVC datums (covering all 5 of Anderson's patterns).

Equations

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

Per-datum InflPattern verification

Each theorem below is a structural drift sentry: changing a Fragment entry's underlying analysis breaks exactly one theorem.

theorem Anderson2006.english_is_auxHeaded : english.inflPattern = Typology.AuxiliaryVerbs.InflPattern.auxHeaded

theorem Anderson2006.doyayo_is_lexHeaded : doyayo.inflPattern = Typology.AuxiliaryVerbs.InflPattern.lexHeaded

theorem Anderson2006.doyayoSplitDoubled_is_splitDoubled : doyayoSplitDoubled.inflPattern = Typology.AuxiliaryVerbs.InflPattern.splitDoubled

theorem Anderson2006.gorum_is_doubled : gorum.inflPattern = Typology.AuxiliaryVerbs.InflPattern.doubled

theorem Anderson2006.jakaltek_is_split : jakaltek.inflPattern = Typology.AuxiliaryVerbs.InflPattern.split

theorem Anderson2006.pipilSplitDoubled_is_splitDoubled : pipilSplitDoubled.inflPattern = Typology.AuxiliaryVerbs.InflPattern.splitDoubled

theorem Anderson2006.pipilLexHeaded_is_lexHeaded : pipilLexHeaded.inflPattern = Typology.AuxiliaryVerbs.InflPattern.lexHeaded

theorem Anderson2006.finnish_is_split : finnish.inflPattern = Typology.AuxiliaryVerbs.InflPattern.split

theorem Anderson2006.hemba_is_splitDoubled : hemba.inflPattern = Typology.AuxiliaryVerbs.InflPattern.splitDoubled

Per-datum form/distribution Fragment grounding

theorem Anderson2006.doyayo_form_from_fragment : doyayo.form = Fragments.Doyayo.AuxiliaryVerbs.lexHeadedForm

theorem Anderson2006.doyayoSplitDoubled_form_from_fragment : doyayoSplitDoubled.form = Fragments.Doyayo.AuxiliaryVerbs.splitDoubledForm

theorem Anderson2006.gorum_form_from_fragment : gorum.form = Fragments.Gorum.AuxiliaryVerbs.form

theorem Anderson2006.jakaltek_form_from_fragment : jakaltek.form = Fragments.Jakaltek.AuxiliaryVerbs.form

theorem Anderson2006.pipilSplitDoubled_form_from_fragment : pipilSplitDoubled.form = Fragments.Pipil.AuxiliaryVerbs.splitDoubledForm

theorem Anderson2006.pipilLexHeaded_form_from_fragment : pipilLexHeaded.form = Fragments.Pipil.AuxiliaryVerbs.lexHeadedForm

theorem Anderson2006.hemba_form_from_fragment : hemba.form = Fragments.Hemba.AuxiliaryVerbs.form

theorem Anderson2006.doyayo_dist_from_fragment : doyayo.distribution = some Fragments.Doyayo.AuxiliaryVerbs.lexHeadedDistribution

theorem Anderson2006.doyayoSplitDoubled_dist_from_fragment : doyayoSplitDoubled.distribution = some Fragments.Doyayo.AuxiliaryVerbs.splitDoubledDistribution

theorem Anderson2006.gorum_dist_from_fragment : gorum.distribution = some Fragments.Gorum.AuxiliaryVerbs.inflDistribution

theorem Anderson2006.jakaltek_dist_from_fragment : jakaltek.distribution = some Fragments.Jakaltek.AuxiliaryVerbs.inflDistribution

theorem Anderson2006.pipilSplitDoubled_dist_from_fragment : pipilSplitDoubled.distribution = some Fragments.Pipil.AuxiliaryVerbs.splitDoubledDistribution

theorem Anderson2006.pipilLexHeaded_dist_from_fragment : pipilLexHeaded.distribution = some Fragments.Pipil.AuxiliaryVerbs.lexHeadedDistribution

theorem Anderson2006.finnish_dist_from_fragment : finnish.distribution = some Fragments.Finnish.Negation.finnishNegDistribution

theorem Anderson2006.hemba_dist_from_fragment : hemba.distribution = some Fragments.Hemba.AuxiliaryVerbs.inflDistribution

Finnish form construction grounding

The Finnish form construction uses negParadigm.find?, which is Option-typed. The fallback | none => "en lue" was historically chosen to coincide with the success-branch result, making finnish.form = "en lue" pass by rfl even when the lookup would return none. The witness theorem below grounds the construction in the actual paradigm content.

theorem Anderson2006.finnish_1sg_in_paradigm : (List.find? (fun (f : Fragments.Finnish.Negation.NegForm) => f.person == 1 && f.number == "sg") Fragments.Finnish.Negation.negParadigm).isSome = true

The Finnish 1sg negative-auxiliary entry exists in negParadigm.

theorem Anderson2006.finnish_1sg_form_eq : Option.map (fun (x : Fragments.Finnish.Negation.NegForm) => x.form) (List.find? (fun (f : Fragments.Finnish.Negation.NegForm) => f.person == 1 && f.number == "sg") Fragments.Finnish.Negation.negParadigm) = some "en"

Strong pinning: the 1sg paradigm entry's form is exactly "en". Together with finnish_1sg_in_paradigm, this pins finnish.form to the Fragment's actual paradigm content. A future change to negParadigm that altered the 1sg form (or removed the entry entirely) would break this theorem; the dead-branch | none => "en lue" fallback in finnish.form cannot mask the change.

theorem Anderson2006.finnish_form_from_paradigm : finnish.form = "en lue"

The Finnish form is the 1sg negParadigm entry's form concatenated with " lue".

Connection to Finnish Fragment

theorem Anderson2006.finnish_split_from_fragment : have dist := Fragments.Finnish.Negation.finnishNegDistribution; dist.onAux ≠ [] ∧ dist.onLex ≠ []

The Finnish negative auxiliary construction is a split AVC: the auxiliary hosts some inflectional categories and the lexical verb hosts others, with neither element hosting all categories.

Pattern coverage (named witnesses)

All five of Anderson's inflectional patterns are attested in the sample. Each pattern is witnessed by a named datum (existence by witness, not aggregate .any-scan). Adding a new datum doesn't break this theorem; changing one of the named witnesses' patterns does.

theorem Anderson2006.five_patterns_attested : english.inflPattern = Typology.AuxiliaryVerbs.InflPattern.auxHeaded ∧ doyayo.inflPattern = Typology.AuxiliaryVerbs.InflPattern.lexHeaded ∧ gorum.inflPattern = Typology.AuxiliaryVerbs.InflPattern.doubled ∧ jakaltek.inflPattern = Typology.AuxiliaryVerbs.InflPattern.split ∧ hemba.inflPattern = Typology.AuxiliaryVerbs.InflPattern.splitDoubled

Structural theorems on distribution

theorem Anderson2006.gorum_doubled_same_categories : (have dist := Fragments.Gorum.AuxiliaryVerbs.inflDistribution; dist.onAux == dist.onLex) = true

In Gorum's doubled AVC, aux and lex host exactly the same categories.

theorem Anderson2006.doyayo_lexHeaded_aux_agreement_only : Fragments.Doyayo.AuxiliaryVerbs.lexHeadedDistribution.onAux = [Core.Morphology.MorphCategory.agreement Core.Agreement.Controller.subj] ∧ Fragments.Doyayo.AuxiliaryVerbs.lexHeadedDistribution.onLex = [Core.Morphology.MorphCategory.tense]

In Doyayo's lex-headed AVC, the auxiliary hosts ONLY tonal subject agreement (per Anderson p. 120), and the LV carries TAM.

theorem Anderson2006.doyayo_splitDoubled_subj_doubled_obj_lex_only : have dist := Fragments.Doyayo.AuxiliaryVerbs.splitDoubledDistribution; dist.onAux.contains (Core.Morphology.MorphCategory.agreement Core.Agreement.Controller.subj) = true ∧ dist.onLex.contains (Core.Morphology.MorphCategory.agreement Core.Agreement.Controller.subj) = true ∧ dist.onLex.contains (Core.Morphology.MorphCategory.agreement Core.Agreement.Controller.obj) = true ∧ dist.onAux.contains (Core.Morphology.MorphCategory.agreement Core.Agreement.Controller.obj) = false

Anderson Ch 5 §5.2 payoff (Doyayo): subject agreement is doubled across AUX and LV; object agreement appears on LV only. Now Lean-checkable directly via Controller-typed .agreement, rather than via the fragile list-length encoding the 0.230.578 workaround used.

theorem Anderson2006.pipil_splitDoubled_subj_doubled_obj_lex_only : have dist := Fragments.Pipil.AuxiliaryVerbs.splitDoubledDistribution; dist.onAux.contains (Core.Morphology.MorphCategory.agreement Core.Agreement.Controller.subj) = true ∧ dist.onLex.contains (Core.Morphology.MorphCategory.agreement Core.Agreement.Controller.subj) = true ∧ dist.onLex.contains (Core.Morphology.MorphCategory.agreement Core.Agreement.Controller.obj) = true ∧ dist.onAux.contains (Core.Morphology.MorphCategory.agreement Core.Agreement.Controller.obj) = false

Anderson Ch 5 §5.2 payoff (Pipil): same generalization as Doyayo — subject doubled across AUX and LV, object on LV only. The AUX root yu itself encodes TAM lexically (no separate .tense morpheme on AUX).

theorem Anderson2006.pipil_lexHeaded_aux_empty : Fragments.Pipil.AuxiliaryVerbs.lexHeadedDistribution.onAux = []

In Pipil's lex-headed AVC, the auxiliary hosts no inflection.

theorem Anderson2006.finnish_split_disjoint : have dist := Fragments.Finnish.Negation.finnishNegDistribution; (dist.onAux.all fun (c : Core.Morphology.MorphCategory) => !dist.onLex.contains c) = true

In Finnish's split AVC, aux and lex host disjoint category types. (.stem on the lex side is a base, not an inflectional overlap.)

theorem Anderson2006.jakaltek_abs_on_aux_erg_on_lex : have dist := Fragments.Jakaltek.AuxiliaryVerbs.inflDistribution; dist.onAux.contains (Core.Morphology.MorphCategory.agreement Core.Agreement.Controller.obj) = true ∧ dist.onLex.contains (Core.Morphology.MorphCategory.agreement Core.Agreement.Controller.subj) = true ∧ dist.onAux.contains (Core.Morphology.MorphCategory.agreement Core.Agreement.Controller.subj) = false ∧ dist.onLex.contains (Core.Morphology.MorphCategory.agreement Core.Agreement.Controller.obj) = false

Anderson Ch 5 abs/erg payoff (Jakaltek): with role-typed agreement, the absolutive-on-AUX / ergative-on-LV split is now a category-level distinction (.agreement .obj vs .agreement .subj), not just a within-category meta-comment.

theorem Anderson2006.hemba_splitDoubled_agreement_doubled : have dist := Fragments.Hemba.AuxiliaryVerbs.inflDistribution; dist.onAux.contains (Core.Morphology.MorphCategory.agreement Core.Agreement.Controller.subj) = true ∧ dist.onLex.contains (Core.Morphology.MorphCategory.agreement Core.Agreement.Controller.subj) = true ∧ dist.onAux.contains Core.Morphology.MorphCategory.tense = true ∧ dist.onLex.contains Core.Morphology.MorphCategory.tense = false ∧ dist.onAux.contains Core.Morphology.MorphCategory.mood = false ∧ dist.onLex.contains Core.Morphology.MorphCategory.mood = true

In Hemba's split/doubled AVC, subject agreement is doubled (on both elements), tense is AUX-only, mood is LV-only. No object agreement in this construction.

Dual headedness

Anderson p. 117 Table 3.1 distinguishes three notions of head: inflectional, phrasal/syntactic, and semantic. The semantic head (content provider) is always the lexical verb (Anderson p. 23); the inflectional host varies by pattern. This mismatch is what makes AVCs typologically distinctive.

theorem Anderson2006.heads_coincide_iff_lexHeaded (p : Typology.AuxiliaryVerbs.InflPattern) : (p.semanticHead == p.inflHost) = (p == Typology.AuxiliaryVerbs.InflPattern.lexHeaded)

The semantic head and inflectional host coincide only in lex-headed AVCs. In all other patterns they diverge: the semantic head is always the lexical verb, but inflection may sit on the auxiliary (or on both elements).

Negative auxiliaries as AVCs

@cite{anderson-2006} §1.7.2 (p. 33-34) treats negative auxiliaries across multiple AVC patterns: aux-headed in Udihe, Neyo; split in Kokota; lex-headed in Kwerba; doubled in 'Iipay. The substantive theorems about NegStrategy → InflPattern live in Phenomena/AuxiliaryVerbs/NegativeAuxiliaries.lean (negVerb_implies_auxHeaded encodes the most common verbal-negator → aux-headed mapping; the other patterns Anderson documents are not yet a Lean-checkable NegStrategy → InflPattern typology because they require finer sub-typing of NegStrategy.negVerb). This file does not re-export.

LV form predictions across patterns

Anderson predicts the verb form of the lexical verb from the inflectional pattern. AUX-headed AVCs have a nonfinite LV (infinitive/participle/etc.; Anderson Table 2.3 on p. 114 catalogs the LV non-finite-form types within AUX-headed AVCs specifically — the table is a one-pattern grid of language exemplars, not a cross-pattern prediction). All other patterns have a finite LV (carrying at least some inflection, per Anderson chs. 3-5 prose). The pattern→LV-form prediction is formalized in Typology.lvVerbForm.

theorem Anderson2006.auxHeaded_predicts_nonfinite_lv : Typology.AuxiliaryVerbs.InflPattern.auxHeaded.lvVerbForm = UD.VerbForm.Inf

theorem Anderson2006.lexHeaded_predicts_finite_lv : Typology.AuxiliaryVerbs.InflPattern.lexHeaded.lvVerbForm = UD.VerbForm.Fin

theorem Anderson2006.doubled_predicts_finite_lv : Typology.AuxiliaryVerbs.InflPattern.doubled.lvVerbForm = UD.VerbForm.Fin

theorem Anderson2006.split_predicts_finite_lv : Typology.AuxiliaryVerbs.InflPattern.split.lvVerbForm = UD.VerbForm.Fin

theorem Anderson2006.splitDoubled_predicts_finite_lv : Typology.AuxiliaryVerbs.InflPattern.splitDoubled.lvVerbForm = UD.VerbForm.Fin

Bridge to Sorace 2000 (auxiliary selection)

Be/have auxiliary selection (Selection.lean) operates within aux-headed AVCs: the question of which auxiliary appears presupposes the auxiliary hosts inflection. @cite{sorace-2000}'s sister study Studies/Sorace2000.lean provides vendlerClassToTypicalTransitivity; the quantified composition with canonicalSelection is given below.

Sorace's gradient Auxiliary Selection Hierarchy is not yet formalized in linglib (per Sorace2000.lean docstring); the contrastive theorem against Anderson's discrete pattern typology (anderson_silent_on_intermediate_ash) will land when ASH ranks are added.

theorem Anderson2006.selection_presupposes_auxHeaded : Typology.AuxiliaryVerbs.InflPattern.auxHeaded.inflHost = Typology.AuxiliaryVerbs.AVCElement.aux

Auxiliary selection presupposes aux-headed pattern: the selecting auxiliary hosts tense/agreement (is the inflectional head).

theorem Anderson2006.sorace_canonical_chain (v : Features.VendlerClass) : Phenomena.AuxiliaryVerbs.Selection.canonicalSelection (Phenomena.AuxiliaryVerbs.Studies.Sorace2000.vendlerClassToTypicalTransitivity v) = match v with | Features.VendlerClass.achievement => Phenomena.AuxiliaryVerbs.Selection.PerfectAux.be | x => Phenomena.AuxiliaryVerbs.Selection.PerfectAux.have

Quantified Sorace bridge: composing vendlerClassToTypicalTransitivity with canonicalSelection yields .be exactly for achievements, .have elsewhere. This generalizes the per-datum Italian arrivare claim to all Vendler classes, exposing the composition canonicalSelection ∘ vendlerClassToTypicalTransitivity as a single theorem rather than a hand-picked tuple. Falsifiable by changing either lookup.

theorem Anderson2006.italian_arrivare_grounds_chain : Phenomena.AuxiliaryVerbs.Selection.italianArrivare.transitivityClass = Phenomena.AuxiliaryVerbs.Selection.TransitivityClass.unaccusative ∧ Phenomena.AuxiliaryVerbs.Selection.italianArrivare.selectedAux = Phenomena.AuxiliaryVerbs.Selection.PerfectAux.be

Italian arrivare grounds the achievement → unaccusative → BE chain: the Selection datum independently classifies arrivare as unaccusative, and canonicalSelection .unaccusative = .be. Composes with sorace_canonical_chain .achievement.

Cross-framework: Miestamo 2005 (negation morpheme classification)

@cite{miestamo-2005} classifies negation strategies by morpheme type (NegMorphemeType: .auxVerb, .affix, .particle, ...); @cite{anderson-2006} via @cite{heine-1993}'s grammaticalization framework places verbal negators on the cline at .auxiliary and non-verbal negators off the cline (Anderson §1.7.2 covers only verbal negators). The two frameworks classify by independently- motivated criteria but, for the strategies linglib's NegStrategy enum exposes, AGREE on which strategies are "verbal": Anderson's .toGramStage = some .auxiliary is exactly Miestamo's .toNegMorphemeType = .auxVerb.

Composition with @cite{miestamo-2005}'s verbal_constructional_always_derived (in Linglib/Phenomena/Negation/Studies/Miestamo2005.lean) then yields: any NegStrategy Anderson places at the auxiliary cline stage, in any Miestamo datum showing constructional asymmetry, has its asymmetry classified as .derived rather than .independent — a falsifiable empirical prediction whose chain runs Anderson's cline → Miestamo's morpheme type → Miestamo's asymmetry source.

The earlier anderson_miestamo_agree_on_neg_morphology theorem in this slot (0.230.573) was a stapled conjunction of three independent facts; the meta-audit at 0.230.576 replaced it with the quantified-equivalence shape below.

theorem Anderson2006.auxiliary_stage_iff_aux_verb_morpheme (s : Phenomena.AuxiliaryVerbs.NegativeAuxiliaries.NegStrategy) : s.toGramStage = some Diachronic.Grammaticalization.GramStage.auxiliary ↔ s.toNegMorphemeType = Typology.Negation.NegMorphemeType.auxVerb

Cross-framework equivalence: Anderson's grammaticalization-cline placement at .auxiliary and Miestamo's morpheme-type classification as .auxVerb partition the NegStrategy enum identically. Both frameworks classify exactly .negVerb (Finnish ei-style inflecting negators) as the verbal subtype. Falsifiable by changing either projection: a future split of NegStrategy.negVerb into Miestamo-style auxVerb-vs-doubleNeg subtypes would break this without breaking either projection individually.