Laoide-Kemp (2026): Irish preverbal d' as a floating segment

[LK26]

[LK26] resolves an apparent ordering paradox in Irish initial consonant mutation (ICM). The preverbal tense particle d' (glossed HIST) is usually taken as the trigger of lenition on the following verb, yet its appearance is conditioned on the post-lenition form: d' surfaces before vowel-initial verbs (d' ól 'I drank') and before lenited f-initial verbs (d' fhág 'I left'), but not before C-initial verbs (*d' bhog).

If d' is the trigger of lenition, how can its insertion depend on the output of lenition? The autosegmental answer (Figs. 1, 2, 5 of the paper): the historic-tense morpheme is (d) + {L} where both elements are floating. {L} (the lenition-inducing bundle) docks onto the immediately-following consonant if present; (d) is a floating melodic segment that surfaces only if it can link to an adjacent C-skeleton position that is both segmentally empty and directly followed by a non-empty V-slot. C-initial verbs leave the first C-slot full; vowel-initial verbs leave it empty; f-initial verbs leave it empty after {L} deletes the f segmental content.

The analysis is strictly modular in the sense of [BO12]: morphosyntax inserts the floating morpheme in all phonological contexts, and the phonology determines whether (d) surfaces by ordinary representational constraints. The paper contrasts this with a morphosyntactic alternative (two separate [+HIST] exponents in different spell-out cycles) and argues empirically against it on the basis of Munster Irish (§6.1) and past-tense impersonal mutation resistance (§6.2).

Grounding: FloatingForm over a CV backbone

This file is founded on Autosegmental.FloatingForm CVKind Segment — the project's floating-autosegmental substrate, which [LK26]'s floating consonants are a named motivating consumer of. Three substrate features carry the analysis directly:

• Morpheme membership on every tier/backbone element distinguishes the historic-tense (d), the verb stem, and the past-tense impersonal exponent.
• The underlying/surface split (links vs surfaceLinks) models lenition the way the paper does — as a delinking of the f segment from its skeletal slot, leaving the underlying form intact and the C-slot surface-empty (FloatingForm.deleteTierElem).
• The historic-tense and impersonal exponents are prefixed by Graph.concat, so the morpheme composition the paper draws (Fig. 1: (d) to the left of the stem; Fig. 5: an empty CV unit to the left) is true by construction, not stipulated.

Lenition is keyed on the melodic element linked to the leftmost skeletal slot (initialConsonantIdx), not the leftmost melody element: in a prefixed form (Fig. 5) the stem's f is no longer adjacent to the left edge, and the empty CV unit correctly blocks {L} from docking onto it.

What this file formalises

• §1 An Irish segment type and CV-skeleton kind.
• §2 Morphemes (HIST, the stem, PST.IMPERS).
• §3 Verb-stem FloatingForms for bog, ól, fág.
• §4 The exponents (d)/{L} and the empty-CV impersonal prefix, composed onto stems via Graph.concat.
• §5 Lenition modelled as surface delinking of f on the leftmost consonant (the {L} effect).
• §6 The docking predicate dPrimeSurfaces — Laoide-Kemp's central empirical generalisation, formulated on the surface graph.
• §7 Worked-example theorems for Figs. 1a (bog → bhog), 1b (ól → d' ól), 1c (fág → d' fhág), and 5 (past-tense impersonals bogadh, óladh, fágadh, all *d').

What this file does NOT formalise

• Figure 2 (r-initial vs fr-initial) — rith (r-initial; d' cannot dock because the first C-slot has /r/) and freagair (fr-initial; {L} deletes /f/, leaving an empty C in an Infrasegmental Government domain that licenses (d)-docking despite the empty V-slot pattern). The IG-domain account requires [Sch98] substrate which linglib doesn't carry yet; deferred.
• §6.1 Munster Irish dialectal variation — dh' appears after all lenition-triggering preverbal particles in Munster, not just historic tense. The paper argues this is naturally accommodated by positing (d) as part of the lenition bundle in Munster; encoded here as a docstring sketch only.
• §5 morphosyntactic alternative — the rejected analysis using two separate [+HIST] exponents in different spell-out cycles. Encoded only via the predictions the phonological account makes (§6 of this file); the alternative would predict the same distribution for Standard Irish but fails the Munster and impersonal tests (paper §6).

Convention

(d) and {L} in the paper are typeset with parentheses and braces to indicate floating status. In Lean identifiers we write dPrime and the HIST morpheme. {L} itself is modelled as the lenition process (lenite) rather than a distinct tier element, matching the paper's treatment of it as abstract lenition-inducing material; (d) is modelled as a genuine floating melodic segment (Segment.dPrime).

§1 Segment inventory and CV skeleton

A minimal Irish segment inventory sufficient for the paper's worked examples. Only the segments appearing in bog, ól, fág, and their past-tense impersonals are enumerated; full Irish phonology lives in Fragments/Irish/ (currently absent — Celtic phonology is a flagged gap in linglib).

inductive LaoideKemp2026.Segment : Type

Irish segment, minimal coverage.

• b : Segment

  Consonant b.

• g : Segment

  Consonant g.

• l : Segment

  Consonant l.

• f : Segment

  Consonant f.

• r : Segment

  Consonant r.

• m : Segment

  Consonant m.

• o : Segment

  Vowel o.

• ó : Segment

  Vowel ó.

• á : Segment

  Vowel á.

• i : Segment

  Vowel i.

• a : Segment

  Schwa-like vowel a (Irish a).

• dPrime : Segment

  The historic-tense floating segment (d).

@[implicit_reducible]

instance LaoideKemp2026.instDecidableEqSegment : DecidableEq Segment

Equations

• LaoideKemp2026.instDecidableEqSegment x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance LaoideKemp2026.instReprSegment : Repr Segment

Equations

• LaoideKemp2026.instReprSegment = { reprPrec := LaoideKemp2026.instReprSegment.repr }

def LaoideKemp2026.instReprSegment.repr : Segment → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• LaoideKemp2026.instReprSegment.repr LaoideKemp2026.Segment.b prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LaoideKemp2026.Segment.b")).group prec✝
• LaoideKemp2026.instReprSegment.repr LaoideKemp2026.Segment.g prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LaoideKemp2026.Segment.g")).group prec✝
• LaoideKemp2026.instReprSegment.repr LaoideKemp2026.Segment.l prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LaoideKemp2026.Segment.l")).group prec✝
• LaoideKemp2026.instReprSegment.repr LaoideKemp2026.Segment.f prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LaoideKemp2026.Segment.f")).group prec✝
• LaoideKemp2026.instReprSegment.repr LaoideKemp2026.Segment.r prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LaoideKemp2026.Segment.r")).group prec✝
• LaoideKemp2026.instReprSegment.repr LaoideKemp2026.Segment.m prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LaoideKemp2026.Segment.m")).group prec✝
• LaoideKemp2026.instReprSegment.repr LaoideKemp2026.Segment.o prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LaoideKemp2026.Segment.o")).group prec✝
• LaoideKemp2026.instReprSegment.repr LaoideKemp2026.Segment.ó prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LaoideKemp2026.Segment.ó")).group prec✝
• LaoideKemp2026.instReprSegment.repr LaoideKemp2026.Segment.á prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LaoideKemp2026.Segment.á")).group prec✝
• LaoideKemp2026.instReprSegment.repr LaoideKemp2026.Segment.i prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LaoideKemp2026.Segment.i")).group prec✝
• LaoideKemp2026.instReprSegment.repr LaoideKemp2026.Segment.a prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LaoideKemp2026.Segment.a")).group prec✝

def LaoideKemp2026.Segment.isF : Segment → Bool

Is the segment f (the target of the special lenition → deletion rule in the paper's §2.2)?

Equations

• LaoideKemp2026.Segment.f.isF = true
• x✝.isF = false

inductive LaoideKemp2026.CVKind : Type

CV-skeleton kind. A 2-kind skeleton (C for consonant slot, V for vowel slot), matching the Strict-CV convention ([Low96]); a project-canonical Strict-CV substrate does not exist (see CLAUDE.md for the deferral rationale).

• C : CVKind
• V : CVKind

@[implicit_reducible]

instance LaoideKemp2026.instDecidableEqCVKind : DecidableEq CVKind

Equations

• LaoideKemp2026.instDecidableEqCVKind x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def LaoideKemp2026.instReprCVKind.repr : CVKind → ℕ → Std.Format

Equations

• LaoideKemp2026.instReprCVKind.repr LaoideKemp2026.CVKind.C prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LaoideKemp2026.CVKind.C")).group prec✝
• LaoideKemp2026.instReprCVKind.repr LaoideKemp2026.CVKind.V prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LaoideKemp2026.CVKind.V")).group prec✝

@[implicit_reducible]

instance LaoideKemp2026.instReprCVKind : Repr CVKind

Equations

• LaoideKemp2026.instReprCVKind = { reprPrec := LaoideKemp2026.instReprCVKind.repr }

§2 Morphemes

Every tier and backbone element of a FloatingForm carries morpheme membership. We tag the three morphemes the analysis distinguishes: the verb stem (a free word), the historic-tense exponent HIST (carrying floating (d)), and the past-tense impersonal exponent (carrying the empty CV unit; §6.2).

§3 Verb stems as FloatingForms

A verb stem is a FloatingForm CVKind Segment: the upper tier is the segmental melody (Segment), the lower tier is the CV skeleton (CVKind), and association lines (k, j) link melody element k to skeleton position j. The surface state mirrors the underlying state on input (FloatingForm.mkInput).

def LaoideKemp2026.bog : Autosegmental.FloatingForm CVKind Segment

The verb bog 'soft', the C-initial example in [LK26] Fig. 1a. Melody = [b, o, g]; skeleton = [C, V, C]; identity associations.

Equations

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

def LaoideKemp2026.ól : Autosegmental.FloatingForm CVKind Segment

The verb ól 'drink', the V-initial example in [LK26] Fig. 1b. Melody = [ó, l]; skeleton = [C, V, C, V]; the initial C-slot has no melodic association. This is the key structural property: the underlying form has an empty C-slot at position 0.

Equations

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

def LaoideKemp2026.fág : Autosegmental.FloatingForm CVKind Segment

The verb fág 'leave', the f-initial example in [LK26] Fig. 1c. Melody = [f, á, g]; skeleton = [C, V, C]; identity associations. Under lenition, the f segmental content deletes, leaving an empty C₁-slot — exactly the configuration that licenses (d)-docking.

Equations

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

§4 The exponents and morpheme composition

The historic-tense morpheme contributes a floating (d) melodic segment with no skeleton of its own (it docks onto the stem's skeleton). The past-tense impersonal morpheme contributes an empty CV unit — a [C, V] skeleton with no melody (Fig. 5). Both are prefixed onto a stem with Graph.concat, which shifts the stem's association lines by the prefix's tier lengths.

def LaoideKemp2026.historicExponent : Autosegmental.Graph (Autosegmental.TierSpec Segment) (Autosegmental.SegSpec CVKind)

The historic-tense exponent: a floating (d) melodic segment, no skeleton, no associations ([LK26] Fig. 1).

Equations

• LaoideKemp2026.historicExponent = { upper := LabeledTuple.ofList [LaoideKemp2026.mel✝ LaoideKemp2026.Segment.dPrime LaoideKemp2026.mHist✝], lower := LabeledTuple.empty, links := ∅ }

def LaoideKemp2026.impersonalExponent : Autosegmental.Graph (Autosegmental.TierSpec Segment) (Autosegmental.SegSpec CVKind)

The past-tense impersonal exponent: an empty CV unit ([C, V] skeleton), no melody, no associations ([LK26] §6.2, Fig. 5).

Equations

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

def LaoideKemp2026.withHist (stem : Autosegmental.FloatingForm CVKind Segment) : Autosegmental.FloatingForm CVKind Segment

Prefix the historic-tense exponent onto a stem (Fig. 1): floating (d) becomes melody index 0; the stem's melody shifts right by one.

Equations

• LaoideKemp2026.withHist stem = LaoideKemp2026.ofGraph✝ (LaoideKemp2026.historicExponent.concat stem.toGraph)

def LaoideKemp2026.withImpers (stem : Autosegmental.FloatingForm CVKind Segment) : Autosegmental.FloatingForm CVKind Segment

Prefix the empty-CV impersonal exponent onto a stem (Fig. 5): the stem's skeleton shifts right by two, so the left edge is an empty C₀V₀ unit.

Equations

• LaoideKemp2026.withImpers stem = LaoideKemp2026.ofGraph✝ (LaoideKemp2026.impersonalExponent.concat stem.toGraph)

§5 Lenition: the {L} deletion rule for f

The Irish lenition mutation has many surface effects (stop → fricative, voiceless → voiced, etc.) but the only effect relevant to the distribution of (d) is the deletion of word-initial /f/ ([LK26] §2.2; [Gus86], [NC91]). Under the autosegmental analysis, the lenition-inducing bundle {L} docks onto the initial consonant and deletes its segmental content; the C-skeletal slot remains behind, surface-empty.

We model this as a surface delinking (deleteTierElem): the f melody element is deleted from the surface, leaving its C-slot surface-empty while the underlying form is preserved. Lenition targets the consonant linked to the leftmost skeletal slot — in a prefixed impersonal form (Fig. 5), the stem's f is no longer at the left edge, so {L} cannot reach it and the f stays unmutated.

def LaoideKemp2026.initialConsonantIdx (f : Autosegmental.FloatingForm CVKind Segment) : Option ℕ

The melody index of the consonant linked to the leftmost skeletal slot (skeleton position 0), if any — the target of {L}.

Equations

• LaoideKemp2026.initialConsonantIdx f = List.find? (fun (k : ℕ) => decide ((k, 0) ∈ f.surfaceLinks)) (List.range f.upper.len)

def LaoideKemp2026.lenite (f : Autosegmental.FloatingForm CVKind Segment) : Autosegmental.FloatingForm CVKind Segment

Apply lenition: if the consonant on the leftmost skeletal slot is f, delete its melodic content on the surface (leaving the slot surface-empty). All other surface effects of lenition (b → v, etc.) are out of scope for the d' distribution question.

Equations

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

§6 The docking predicate

(d) surfaces iff the post-lenition surface form has an empty C-slot at position 0 directly followed by a non-empty V-slot at position 1 ([LK26] §4, Fig. 1). The predicate inspects the surface graph (FloatingForm.surfaceGraph): the actual (d) surfacing is then a deterministic consequence of the autosegmental linking convention.

def LaoideKemp2026.isCSlot (f : Autosegmental.FloatingForm CVKind Segment) (j : ℕ) : Prop

Skeleton position j is a C-slot.

Equations

• LaoideKemp2026.isCSlot f j = (Option.map Autosegmental.SegSpec.seg (f.lower.get? j) = some LaoideKemp2026.CVKind.C)

@[implicit_reducible]

instance LaoideKemp2026.instDecidableIsCSlot (f : Autosegmental.FloatingForm CVKind Segment) (j : ℕ) : Decidable (isCSlot f j)

Equations

• LaoideKemp2026.instDecidableIsCSlot f j = LaoideKemp2026.instDecidableIsCSlot._aux_1 f j

def LaoideKemp2026.isVSlot (f : Autosegmental.FloatingForm CVKind Segment) (j : ℕ) : Prop

Skeleton position j is a V-slot.

Equations

• LaoideKemp2026.isVSlot f j = (Option.map Autosegmental.SegSpec.seg (f.lower.get? j) = some LaoideKemp2026.CVKind.V)

@[implicit_reducible]

instance LaoideKemp2026.instDecidableIsVSlot (f : Autosegmental.FloatingForm CVKind Segment) (j : ℕ) : Decidable (isVSlot f j)

Equations

• LaoideKemp2026.instDecidableIsVSlot f j = LaoideKemp2026.instDecidableIsVSlot._aux_1 f j

def LaoideKemp2026.dDockable (f : Autosegmental.FloatingForm CVKind Segment) : Prop

The configuration that licenses (d)-docking, evaluated on the surface graph: position 0 is an empty C-slot, position 1 is a non-empty V-slot. The structural predicate at the heart of the paper's analysis ([LK26] §4.1).

Equations

• LaoideKemp2026.dDockable f = (LaoideKemp2026.isCSlot f 0 ∧ ¬f.surfaceGraph.IsLinkedLower 0 ∧ LaoideKemp2026.isVSlot f 1 ∧ f.surfaceGraph.IsLinkedLower 1)

@[implicit_reducible]

instance LaoideKemp2026.instDecidableDDockable (f : Autosegmental.FloatingForm CVKind Segment) : Decidable (dDockable f)

Equations

• LaoideKemp2026.instDecidableDDockable f = LaoideKemp2026.instDecidableDDockable._aux_1 f

def LaoideKemp2026.dPrimeSurfaces (f : Autosegmental.FloatingForm CVKind Segment) : Prop

(d) surfaces in the historic-tense form f iff the post-lenition surface form is (d)-dockable. [LK26] §4.1.

Equations

• LaoideKemp2026.dPrimeSurfaces f = LaoideKemp2026.dDockable (LaoideKemp2026.lenite f)

@[implicit_reducible]

instance LaoideKemp2026.instDecidableDPrimeSurfaces (f : Autosegmental.FloatingForm CVKind Segment) : Decidable (dPrimeSurfaces f)

Equations

• LaoideKemp2026.instDecidableDPrimeSurfaces f = LaoideKemp2026.instDecidableDPrimeSurfaces._aux_1 f

§7 Worked examples (paper Figs. 1a, 1b, 1c)

The three figures in [LK26] §4.1 establish the core empirical pattern. In every historic-tense form, (d) is melody index 0 and is floating before docking — the floating status the whole analysis turns on.

theorem LaoideKemp2026.dPrime_floating_bog : (withHist bog).IsFloating 0

(d) is floating (alive but unlinked) in the historic-tense form of every stem before docking — the premise of the analysis.

theorem LaoideKemp2026.bog_no_dPrime : ¬dPrimeSurfaces (withHist bog)

Fig. 1a (C-initial: bog). The first C-slot is occupied by b; (d) cannot dock. Lenition affects b (b → v / β) but does not vacate the C-slot — there is still a segment there. (d) therefore stays unpronounced: dDockable fails on the ¬ IsLinkedLower 0 conjunct (C₁ is surface-linked to b).

theorem LaoideKemp2026.ól_yes_dPrime : dPrimeSurfaces (withHist ól)

Fig. 1b (V-initial: ól). The underlying form has an empty C₁-slot already (the vowel ó associates to V₁, not to C₀). Lenition is a no-op: C₀ has no linked consonant (the verb is V-initial), so {L} has nothing to delete. dDockable holds; (d) surfaces. The historic form is d' ól.

theorem LaoideKemp2026.fág_yes_dPrime : dPrimeSurfaces (withHist fág)

Fig. 1c (f-initial: fág). Underlyingly, f occupies C₁ and (d) would not be able to dock. Lenition deletes f's segmental content on the surface (via lenite), leaving C₁ surface-empty; dDockable then holds on the lenited form; (d) surfaces. The historic tense form is d' fhág.

§8 Past-tense impersonals (paper Fig. 5)

Past tense impersonal verbs carry an underlying empty CV unit at their left edge ([LK26] §6.2, Fig. 5), modelled here by prefixing impersonalExponent with Graph.concat. This empty unit does double duty: {L} cannot dock onto the stem's initial consonant (it is no longer adjacent to the left edge — lenite is a no-op), and the empty C₀ is followed by an empty V₀, so the (d)-docking condition IsLinkedLower 1 fails. Both effects fall out of the same piece of structure, and (d) never surfaces — exactly the paper's account of why preverbal d' is absent on past-tense impersonals.

theorem LaoideKemp2026.bogadh_no_dPrime : ¬dPrimeSurfaces (withHist (withImpers bog))

Fig. 5a (C-initial impersonal: bogadh). *d' bogadh.

theorem LaoideKemp2026.óladh_no_dPrime : ¬dPrimeSurfaces (withHist (withImpers ól))

Fig. 5b (V-initial impersonal: óladh). *d' óladh — the empty V₀ of the impersonal prefix breaks the docking condition even though the verb is V-initial.

theorem LaoideKemp2026.fágadh_no_dPrime : ¬dPrimeSurfaces (withHist (withImpers fág))

Fig. 5c (f-initial impersonal: fágadh). *d' fágadh — the empty C₀ blocks {L} from docking onto the stem's f (so f stays, unlike Fig. 1c), and the empty V₀ blocks (d).

§9 Side-by-side: the paper's empirical core

Putting the theorems together gives [LK26]'s central observation: in Standard Irish historic tense, (d) surfaces iff the verb is V-initial (Fig. 1b) or f-initial (Fig. 1c), but not when C-initial (Fig. 1a); and it never surfaces on past-tense impersonals (Fig. 5), regardless of the stem's initial segment.

theorem LaoideKemp2026.laoideKemp_fig1_fig5 : (¬dPrimeSurfaces (withHist bog) ∧ dPrimeSurfaces (withHist ól) ∧ dPrimeSurfaces (withHist fág)) ∧ ¬dPrimeSurfaces (withHist (withImpers bog)) ∧ ¬dPrimeSurfaces (withHist (withImpers ól)) ∧ ¬dPrimeSurfaces (withHist (withImpers fág))

The paper's central empirical generalisation, Figs. 1 + 5.

§10 Modularity: the analysis lives in the monoidal subcategory

[LK26]'s strict-modularity thesis, formalised against the monoidal-subcategory framework (Autosegmental.WellFormedAR). Three theorems, one per modular commitment: the morpheme is composed by the monoidal product ⊗ = concat (not inserted by a non-local rule); the composition preserves well-formedness because the No-Crossing Constraint is morpheme-modular (ncc_isMonoidal); and the (d)-surfacing decision is left-edge local — invariant under material appended on the right (no look-ahead, the apparent paradox dissolved).

theorem LaoideKemp2026.withHist_eq_concat (stem : Autosegmental.FloatingForm CVKind Segment) : (withHist stem).toGraph = historicExponent.concat stem.toGraph

The historic-tense morpheme is composed by the monoidal product: withHist stem is literally historicExponent ⊗ stem. The formal content of "morphosyntax concatenates the floating morpheme" ([BO12]'s strict modularity) — not a non-local insertion rule.

theorem LaoideKemp2026.withHist_isPlanar (stem : Autosegmental.FloatingForm CVKind Segment) (hP : stem.IsPlanar) : (withHist stem).IsPlanar

Composing the historic-tense morpheme preserves autosegmental well-formedness — a direct consequence of the No-Crossing Constraint being morpheme-modular (ncc_isMonoidal). The floating (d) is prefixed without ever creating a crossing association line, for any planar stem.

theorem LaoideKemp2026.dPrime_right_invariant : dPrimeSurfaces (withHist ól) ↔ dPrimeSurfaces (withHist (LaoideKemp2026.ofGraph✝ (ól.concat LaoideKemp2026.someSuffix✝.toGraph)))

Left-edge locality (no look-ahead), concrete witness. Appending phonological material on the right of the stem does not change whether (d) surfaces. Shown here for ól with a concrete suffix; the general statement (any suffix, configuration level) is dDockable_withHist_concat_right below. This is the categorical resolution of the paper's apparent ordering paradox — the conditioning looks boundary-spanning but is in fact morpheme-local.

The general no-look-ahead theorem

dPrime_right_invariant above is the concrete witness; here it is for every suffix. The floating (d) shifts melody indices only, so surface-linkedness of a skeletal slot reduces to the stem's underlying links; and suffix material concatenated on the right lands at skeletal positions ≥ stem.lower.len, never touching slots 0/1. The docking configuration is therefore determined by the stem's left edge alone — the formal content of strict modularity (no look-ahead).

theorem LaoideKemp2026.dDockable_withHist_concat_right (stem suffix : Autosegmental.FloatingForm CVKind Segment) (h2 : 2 ≤ stem.lower.len) : dDockable (withHist (LaoideKemp2026.ofGraph✝ (stem.concat suffix.toGraph))) ↔ dDockable (withHist stem)

The general no-look-ahead theorem. For any suffix, the (d)-docking configuration of the historic-tense form is determined by the stem's left two skeletal slots alone — appending phonological material on the right cannot change it (the stem already supplies those slots). The general form of dPrime_right_invariant: the formal content of strict modularity. (The post-lenition version dPrimeSurfaces additionally requires {L}-docking to be left-local, which holds for in-bounds stems; this is the configuration-level statement, on which it rests.)

Lifting to the post-lenition predicate

The configuration-level theorem above is pre-lenition. The full dPrimeSurfaces version additionally needs {L}-docking (lenite) to be left-local: lenite targets the consonant on skeletal slot 0, which is the stem's, and deletes the same melody index in both forms. This needs the stem in-bounds (stem.toGraph.InBounds): otherwise a stem link with an out-of-range melody index would sit outside withHist stem's initialConsonantIdx search range but inside the longer suffixed range, and lenite could target different indices.

theorem LaoideKemp2026.dPrimeSurfaces_withHist_concat_right (stem suffix : Autosegmental.FloatingForm CVKind Segment) (h2 : 2 ≤ stem.lower.len) (hib : stem.InBounds) : dPrimeSurfaces (withHist (LaoideKemp2026.ofGraph✝ (stem.concat suffix.toGraph))) ↔ dPrimeSurfaces (withHist stem)

The general no-look-ahead theorem, post-lenition. For any suffix, whether (d) surfaces — dPrimeSurfaces, i.e. dockability after {L}-lenition — is determined by the stem's left edge alone. Both the docking configuration (dDockable_withHist_concat_right) and the {L}-docking target (initialConsonantIdx_concat, needing InBounds) are left-local, so the full predicate is too. This is the paper's central claim, in full: preverbal d' never looks rightward past the word it attaches to.

§11 Layer 2 — the historic morpheme as a monoidal-category functor

The deepest categorical content: morpheme prefixation is not merely a function on representations but an endofunctor on the monoidal category WellFormedAR — mathlib's tensorLeft. This consumes the full MonoidalCategory (WellFormedAR α β) instance (not merely the concat operation), and the associativity of prefixation is WellFormedAR's associator, exhibited by tensorLeftTensor — a natural isomorphism that does not exist without coherence (pentagon + triangle).

(d) acts on the left edge, so it is left-tensoring (tensorLeft), not right: the categorical encoding of the morpheme's directionality as a preverbal particle rather than a suffix.

The remaining Layer-2 frontier — modelling lenition and docking themselves as functors WellFormedAR ⥤ WellFormedAR (acting on morphisms, not just objects) — is left open. The conjecture is that they are functorial only over the precedence-preserving Graph.SubgraphEmbeds, not over all of AR.Hom; settling it either way is a genuine result. The extensional content (no look-ahead) is fully captured by dPrimeSurfaces_withHist_concat_right above: for any suffix, whether (d) surfaces depends only on the stem's left edge.

def LaoideKemp2026.historicExponentAR : Autosegmental.WellFormedAR (Autosegmental.TierSpec Segment) (Autosegmental.SegSpec CVKind)

The historic-tense exponent as an object of the monoidal category WellFormedAR (well-formed: no links, hence in-bounds and planar).

Equations

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

def LaoideKemp2026.withHistFunctor : CategoryTheory.Functor (Autosegmental.WellFormedAR (Autosegmental.TierSpec Segment) (Autosegmental.SegSpec CVKind)) (Autosegmental.WellFormedAR (Autosegmental.TierSpec Segment) (Autosegmental.SegSpec CVKind))

The historic morpheme is an endofunctor on WellFormedAR. Prefixing (d) is left-tensoring by historicExponentAR — mathlib's tensorLeft, which exists only because WellFormedAR is a MonoidalCategory. Left- rather than right-tensoring encodes the morpheme's directionality as a preverbal particle.

Equations

• LaoideKemp2026.withHistFunctor = CategoryTheory.MonoidalCategory.tensorLeft LaoideKemp2026.historicExponentAR

theorem LaoideKemp2026.withHistFunctor_obj_toGraph (X : Autosegmental.WellFormedAR (Autosegmental.TierSpec Segment) (Autosegmental.SegSpec CVKind)) : (withHistFunctor.obj X).obj.toGraph = historicExponent.concat X.obj.toGraph

The functor's action on objects is morpheme prefixing: it agrees with withHist at the level of the underlying graph (withHist_eq_concat).

noncomputable def LaoideKemp2026.prefixAssoc (X : Autosegmental.WellFormedAR (Autosegmental.TierSpec Segment) (Autosegmental.SegSpec CVKind)) : CategoryTheory.MonoidalCategory.tensorLeft (CategoryTheory.MonoidalCategoryStruct.tensorObj historicExponentAR X) ≅ (CategoryTheory.MonoidalCategory.tensorLeft X).comp (CategoryTheory.MonoidalCategory.tensorLeft historicExponentAR)

Associativity of prefixation is the associator. This natural isomorphism — prefixing the compound (d) ⊗ X equals prefixing X then prefixing (d) — is built from WellFormedAR's associator, so it does not exist unless the monoidal structure is coherent (pentagon + triangle). It is the concrete artifact that makes WellFormedAR's coherence load-bearing rather than decorative.

Equations

• LaoideKemp2026.prefixAssoc X = CategoryTheory.MonoidalCategory.tensorLeftTensor LaoideKemp2026.historicExponentAR X

§11.5 The morphism-functor frontier: why lenition is precedence-sensitive

Layer 2 modelled morpheme prefixing as the functor tensorLeft. The deeper question is whether a phonological process — {L}-lenition — is a functor on the autosegmental category, acting on morphisms and not just objects. At the graph level, lenition is delinkInitial: erase the association lines to the leftmost (word-initial) skeletal slot.

The answer is a sharp dichotomy. delinkInitial is not a functor on the full category AR α β: a label-preserving reindexing (AR.Hom) can move a non-initial element into initial position, after which there is no morphism between the delinked images at all (delinkInitial_not_functorial). But over PrecAR, the precedence-preserving wide subcategory (Autosegmental/Embedding.lean: order-embedding tier maps; SubgraphEmbeds translations are canonical instances), it lifts to a genuine endofunctor delinkInitialFunctor (built from delinkInitial_map / _id / _comp; precedence-preservation discharges the reflects-initial-slot hypothesis via precPreserving.reflects_zero). This is the categorical content of the linguistic fact that lenition targets the word-initial consonant: the process is functorial over exactly the maps that preserve precedence.

def LaoideKemp2026.delinkInitial {α : Type u_1} {β : Type u_2} (A : Autosegmental.AR α β) : Autosegmental.AR α β

The model of {L}-lenition: erase the association lines to the leftmost (slot-0) skeletal position. Erasing links preserves in-boundedness, so it is an endomap of AR.

Equations

• LaoideKemp2026.delinkInitial A = { toGraph := have __src := A.toGraph; { upper := __src.upper, lower := __src.lower, links := {p ∈ A.links | p.2 ≠ 0} }, inBounds := ⋯ }

@[simp]

theorem LaoideKemp2026.delinkInitial_links {α : Type u_1} {β : Type u_2} (A : Autosegmental.AR α β) : (delinkInitial A).links = {p ∈ A.links | p.2 ≠ 0}

def LaoideKemp2026.delinkInitial_map {α : Type u_1} {β : Type u_2} {A B : Autosegmental.AR α β} (f : A.Hom B) (hf : ∀ (j : Fin A.lower.len), ↑(f.fL.toFun j) = 0 → ↑j = 0) : (delinkInitial A).Hom (delinkInitial B)

delinkInitial is functorial over precedence-preserving morphisms. An AR.Hom that reflects slot 0 (never maps a non-initial slot to slot 0) lifts to a morphism between the delinked graphs, with the same index maps. Precedence-preserving SubgraphEmbeds translations satisfy the hypothesis: a translation sends slot j to j + δ, which is 0 only when j = 0.

Equations

• LaoideKemp2026.delinkInitial_map f hf = { fU := f.fU, fL := f.fL, links_preserve := ⋯ }

theorem LaoideKemp2026.delinkInitial_map_id {α : Type u_1} {β : Type u_2} (A : Autosegmental.AR α β) : delinkInitial_map (Autosegmental.AR.Hom.id A) ⋯ = Autosegmental.AR.Hom.id (delinkInitial A)

Functor law: delinkInitial_map preserves identities.

theorem LaoideKemp2026.delinkInitial_map_comp {α : Type u_1} {β : Type u_2} {A B C : Autosegmental.AR α β} (f : A.Hom B) (g : B.Hom C) (hf : ∀ (j : Fin A.lower.len), ↑(f.fL.toFun j) = 0 → ↑j = 0) (hg : ∀ (j : Fin B.lower.len), ↑(g.fL.toFun j) = 0 → ↑j = 0) (hfg : ∀ (j : Fin A.lower.len), ↑((f.comp g).fL.toFun j) = 0 → ↑j = 0) : delinkInitial_map (f.comp g) hfg = (delinkInitial_map f hf).comp (delinkInitial_map g hg)

Functor law: delinkInitial_map preserves composition.

def LaoideKemp2026.delinkInitialFunctor {α : Type u_1} {β : Type u_2} : CategoryTheory.Functor (Autosegmental.PrecAR α β) (Autosegmental.PrecAR α β)

delinkInitial is an endofunctor of the precedence-preserving subcategory PrecAR (Autosegmental/Embedding.lean). Lenition lifts to a morphism exactly when the reindexing preserves precedence — delinkInitial_not_functorial shows it fails on the full AR. The object endomap is delinkInitial, the morphism action delinkInitial_map; precedence-preservation transports for free because delinkInitial_map keeps the tier maps unchanged. This makes "lenition respects linear adjacency" a typed theorem ([Jar17] Ch. 7's process-as- graph-relation view, here in categorical form).

Equations

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

The negative counterexample

theorem LaoideKemp2026.delinkInitial_not_functorial : ∃ (A : Autosegmental.AR ℕ ℕ) (B : Autosegmental.AR ℕ ℕ) (x : A.Hom B), IsEmpty ((delinkInitial A).Hom (delinkInitial B))

delinkInitial is not a functor on the full category. negSwap is a morphism negA → negB, yet after delinking there is no morphism delinkInitial negA → delinkInitial negB at all: the surviving slot-1 link of negA has been moved onto slot 0 of negB, which delinking erases, so link-preservation becomes impossible. A functor would have to supply such a morphism; none exists. The positive delinkInitial_map shows the obstruction is exactly the failure to preserve precedence.

§12 The strict-modularity payoff

The phonological analysis above is strictly modular in the sense of [BO12]: morphosyntax inserts the historic- tense morpheme (d) + {L} uniformly, and the phonology decides whether (d) surfaces by inspecting the post-lenition skeletal configuration of the verb. No look-ahead in morphology; no post-lenition reference in spell-out; no module-transcending diacritic. The paper's §1 frames this in opposition to four non-modular alternatives:

• Morphology directly manipulates phonological structure ([And92]).
• Readjustment rules triggered by module-transcending diacritics ([HN99]).
• Co-phonologies ([Ant02], [IZ07]).
• Morpheme-specific phonological constraints ([Pat00], [Pat09]).

The autosegmental approach with floating phonologically-defective material ([Lie83], [Zim22]) is the fifth and only strictly-modular alternative, and it is the one [LK26] adopts.

This file does not formalise the other four alternatives directly. Their predictions for Standard Irish coincide with the autosegmental account; the discriminating data are in §6 of the paper (Munster Irish, past-tense impersonals) and are noted in the module docstring as deferred extensions.