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:

• Morph 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).

@[instance_reducible]

instance LaoideKemp2026.instDecidableEqSegment : DecidableEq Segment

Equations

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

@[instance_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

@[instance_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✝

@[instance_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 Morph: 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 Morphology.Morph

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 Morphology.Morph

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 Morphology.Morph

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.FloatingForm CVKind Segment Morphology.Morph

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

Equations

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

def LaoideKemp2026.impersonalExponent : Autosegmental.FloatingForm CVKind Segment Morphology.Morph

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 Morphology.Morph) : Autosegmental.FloatingForm CVKind Segment Morphology.Morph

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.historicExponent.hconcat stem

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

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.impersonalExponent.hconcat stem

§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 Morphology.Morph) : 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 Morphology.Morph) : Autosegmental.FloatingForm CVKind Segment Morphology.Morph

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 Morphology.Morph) (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)

@[instance_reducible]

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

Equations

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

def LaoideKemp2026.isVSlot (f : Autosegmental.FloatingForm CVKind Segment Morphology.Morph) (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)

@[instance_reducible]

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

Equations

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

def LaoideKemp2026.dDockable (f : Autosegmental.FloatingForm CVKind Segment Morphology.Morph) : 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.SurfaceLinkedLower 0 ∧ LaoideKemp2026.isVSlot f 1 ∧ f.SurfaceLinkedLower 1)

@[instance_reducible]

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

Equations

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

def LaoideKemp2026.dPrimeSurfaces (f : Autosegmental.FloatingForm CVKind Segment Morphology.Morph) : 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)

@[instance_reducible]

instance LaoideKemp2026.instDecidableDPrimeSurfaces (f : Autosegmental.FloatingForm CVKind Segment Morphology.Morph) : 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 category of representations. 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 Morphology.Morph) : withHist stem = historicExponent.hconcat stem

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 Morphology.Morph) (hP : Autosegmental.IsNonCrossing stem.links) : Autosegmental.IsNonCrossing (withHist stem).links

Composing the historic-tense morpheme preserves autosegmental well-formedness — a direct consequence of the No-Crossing Constraint being morpheme-modular. The floating (d) shifts the stem's links monotonically, never creating a crossing line.

theorem LaoideKemp2026.dPrime_right_invariant : dPrimeSurfaces (withHist ól) ↔ dPrimeSurfaces (withHist (ól.hconcat LaoideKemp2026.someSuffix✝))

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 Morphology.Morph) (h2 : 2 ≤ stem.lower.len) : dDockable (withHist (stem.hconcat suffix)) ↔ 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.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 Morphology.Morph) (h2 : 2 ≤ stem.lower.len) (hib : stem.InBounds) : dPrimeSurfaces (withHist (stem.hconcat suffix)) ↔ 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 of representations — mathlib's tensorLeft. This consumes the full MonoidalCategory (AR t) instance (not merely the tensor operation), and the associativity of prefixation is the category'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 endofunctors of the representation category (acting on morphisms, not just objects) — is left open. The conjecture is that they are functorial only over precedence-preserving morphisms, not over all broad ones; delinkInitialFunctor settles the lenition case. 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.historicExponentRep : Autosegmental.AR Sigma.fst

The historic-tense exponent as an object of the monoidal category of representations: one floating (d) melody node, no skeleton, no links.

Equations

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

def LaoideKemp2026.withHistFunctor : CategoryTheory.Functor (Autosegmental.AR Sigma.fst) (Autosegmental.AR Sigma.fst)

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

Equations

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

theorem LaoideKemp2026.withHistFunctor_obj (X : Autosegmental.AR Sigma.fst) : withHistFunctor.obj X = CategoryTheory.MonoidalCategoryStruct.tensorObj historicExponentRep X

The functor's action on objects is morpheme prefixing: the tensor of the exponent with the stem.

noncomputable def LaoideKemp2026.prefixAssoc (X : Autosegmental.AR Sigma.fst) : CategoryTheory.MonoidalCategory.tensorLeft (CategoryTheory.MonoidalCategoryStruct.tensorObj historicExponentRep X) ≅ (CategoryTheory.MonoidalCategory.tensorLeft X).comp (CategoryTheory.MonoidalCategory.tensorLeft historicExponentRep)

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

Equations

• LaoideKemp2026.prefixAssoc X = CategoryTheory.MonoidalCategory.tensorLeftTensor LaoideKemp2026.historicExponentRep 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 broad category: a label-preserving reindexing (a broad Graph.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 the precedence-preserving wide subcategory (the foundation's AR.precPreserving), it lifts to a genuine endofunctor delinkInitialFunctor: an arc-preserving morphism transports tier-initiality for free — an arc into v maps to an arc into f v — so the delinked edge conditions carry over. 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.NoPred {S : Type u_1} (X : Autosegmental.Graph S) (v : X.V) : Prop

A vertex with no arc-predecessor: the tier-initial position.

Equations

• LaoideKemp2026.NoPred X v = ∀ (u : X.V), ¬X.arcs.Adj u v

def LaoideKemp2026.delinkInitial {S : Type u_1} {ι : Type u_2} (t : S → ι) (i₀ : ι) (X : Autosegmental.Graph S) : Autosegmental.Graph S

Erase every association line incident to a tier-i₀-initial vertex — the graph model of the paper's initial-position delinking (lenition targeting the word-initial slot). Arcs and labels are untouched.

Equations

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

def LaoideKemp2026.delinkInitialRep {S : Type u_1} {ι : Type u_2} {t : S → ι} (i₀ : ι) (X : Autosegmental.AR t) : Autosegmental.AR t

Delinking preserves the structural axioms: arcs are untouched and the edge set shrinks.

Equations

• LaoideKemp2026.delinkInitialRep i₀ X = { obj := LaoideKemp2026.delinkInitial t i₀ X.obj, property := ⋯ }

def LaoideKemp2026.delinkInitialFunctor {S : Type u_1} {ι : Type u_2} {t : S → ι} (i₀ : ι) : CategoryTheory.Functor (CategoryTheory.WideSubcategory Autosegmental.AR.precPreserving) (CategoryTheory.WideSubcategory Autosegmental.AR.precPreserving)

Initial-position delinking is an endofunctor of the precedence-preserving wide subcategory: an arc-preserving morphism transports tier-initiality for free (an arc into v maps to an arc into f v), so the delinked edge conditions carry over. On the broad category the lift fails (delinkInitial_not_functorial below).

Equations

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

theorem LaoideKemp2026.delinkInitial_not_functorial : IsEmpty ((delinkInitial Sigma.fst false LaoideKemp2026.negA✝.obj).Hom (delinkInitial Sigma.fst false LaoideKemp2026.negB✝.obj))

Delinking is not functorial on the broad category: negSwap is a morphism, yet the delinked images admit no morphism at all — the surviving slot-1 link of negA lands on negB's initial slot, which delinking erased. The obstruction is precisely failure to preserve precedence (delinkInitialFunctor lifts it otherwise).

§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]).
• Morph-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.