Faust & Lampitelli (2026): Guttural Synseresis in Tigrinya and Tigre

[FL26]

[FL26]'s headline claim: in the Ethiosemitic languages Tigre and Tigrinya, gutturals (ʔ, h, ħ, ʕ) function as low glides — the consonantal counterpart of low vowels [ʌ, a]. Sequences /ʌGV/ undergo synersis (the /ʌ/ syncopated, only G surfaces) just as /iIu/ → [ju] in classical hiatus-resolution; both patterns instantiate the same Element-Theoretic operation ([KLV85], [Bac11]) of element-fusion under OCP.

Two co-equal headline contributions (paper §1, eq. 2):

• Empirical: gutturals = low glides (the |A|-as-consonantal analogue of |I|-as-glide |j| and |U|-as-glide |w|).
• Polemical: synersis is economy-driven (eq. 2b: "two homorganic elements are realized in one if possible"), not phonotactic-driven (eq. 2a: "fancy Latinate name for gliding"). The Ethiosemitic facts force (2b): /mibarak/ → [mɨbɨrak] (paper eq. 18c, 39b) shows synersis applies even when no surface phonotactic problem would arise from leaving the sequence unfused.

What this file formalizes

• §1 ET decomposition of Tigrinya/Tigre vowels and gutturals (paper eq. 20-22), as a per-segment projection from the theory-neutral fragment files.
• §0 The Strict-CV substrate (StrictCV namespace below): VStatus, CVSeq, ProperlyGoverned, ECPSatisfied, LicensesPrecedingC. Inlined here as a single-consumer concept (CLAUDE.md graduation rule).
• §2 Strict-CV representations of the paper's worked examples, encoded as CVSeq values with per-V-slot melodic status.
• §3 Five named theorems:
  • T0_economy_drives_syneresis — witness /mibarak/ → [mɨbɨrak].
  • T1_gutturals_are_lowGlides — structural; ET decomposition.
  • T2_synersis_iff_fused_and_governed — analysis's core biconditional.
  • T3_selfLicensing_blocks_dissociation — explains [ʕarifu].
  • T4_walker_rose_2015_overshoots — divergence with witness /mismaʕa/.
• §4 The OCP-merger reading: |A|+|A| → |A| as instance of the shared OCP.collapse substrate.
• §5 Paper self-flagged limits as LIMITATION-tagged comments.

What this file does NOT formalize

• The full GP/Strict-CV apparatus (Coda Mirror, lateral relation typology). The StrictCV namespace below carries the simplified form per the paper's n. 16.
• The phonetic implementation of [ɨ] vs [a]/[ʌ] — see [Fau24] for the cross-linguistic theory.
• Templatic morphology beyond bare CV patterns (see [Fau14], [Fau17b], [FL23]).

Cross-framework engagement

• §3 T4 makes explicit the divergence with [WR15].
• The OCP merger operation (OCP.collapse) unifies this paper's |A|+|A| fusion with [Lio22a]'s TRN merger (Laal subtonal phonology). They are instances of one operation on different feature spaces; the framework choice (binary-feature TRN vs privative-element |A|) lives at the segment-representation level, not at the merger-operation level.

Convention

Predicates in this file are Prop-valued with Decidable instances, matching mathlib + the existing OCP style. Worked examples are checked via decide rather than rfl where appropriate.

§0 Strict-CV Government Phonology substrate

[KLV85] [KLV90] [Cha91] [Low96] [Sch04a] [SS01]

Inlined here as a StrictCV namespace; single-consumer concept per CLAUDE.md graduation rule. Government Phonology (GP) and its Strict-CV (CVCV) descendant ([Low96], [Sch04a]) build phonological representations as alternating C-V skeletal sequences, with three core lateral relations between V-slots:

• Proper Government ([KLV90]): a contentful nucleus governs a preceding empty nucleus, allowing the empty nucleus to remain phonetically silent.
• Empty Category Principle (ECP, simplified): an empty nucleus may be phonetically non-interpreted iff it is properly governed.
• Licensing ([SS01]): a contentful nucleus licenses an adjacent position (typically the preceding onset).

The substrate here gives the simplified form of these definitions used in [FL26], which acknowledges the simplification (paper n. 16).

inductive FaustLampitelli2026.StrictCV.VStatus : Type

A V-slot's melodic status. Per Strict CV ([Low96]), every consonant-cluster representation interpolates empty V-slots, so the same skeletal position may surface silently if properly governed, or with an epenthetic vowel if not.

• full : VStatus

  The V-slot has melodic content.

• empty : VStatus

  The V-slot has no melodic content.

@[implicit_reducible]

instance FaustLampitelli2026.StrictCV.instDecidableEqVStatus : DecidableEq VStatus

Equations

• FaustLampitelli2026.StrictCV.instDecidableEqVStatus x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def FaustLampitelli2026.StrictCV.instReprVStatus.repr : VStatus → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance FaustLampitelli2026.StrictCV.instReprVStatus : Repr VStatus

Equations

• FaustLampitelli2026.StrictCV.instReprVStatus = { reprPrec := FaustLampitelli2026.StrictCV.instReprVStatus.repr }

def FaustLampitelli2026.StrictCV.VStatus.IsFull : VStatus → Prop

Equations

• FaustLampitelli2026.StrictCV.VStatus.full.IsFull = True
• FaustLampitelli2026.StrictCV.VStatus.empty.IsFull = False

@[implicit_reducible]

instance FaustLampitelli2026.StrictCV.VStatus.instDecidablePredIsFull : DecidablePred IsFull

Equations

• FaustLampitelli2026.StrictCV.VStatus.full.instDecidablePredIsFull = isTrue trivial
• FaustLampitelli2026.StrictCV.VStatus.empty.instDecidablePredIsFull = isFalse not_false

def FaustLampitelli2026.StrictCV.VStatus.IsEmpty : VStatus → Prop

Equations

• FaustLampitelli2026.StrictCV.VStatus.empty.IsEmpty = True
• FaustLampitelli2026.StrictCV.VStatus.full.IsEmpty = False

@[implicit_reducible]

instance FaustLampitelli2026.StrictCV.VStatus.instDecidablePredIsEmpty : DecidablePred IsEmpty

Equations

• FaustLampitelli2026.StrictCV.VStatus.empty.instDecidablePredIsEmpty = isTrue trivial
• FaustLampitelli2026.StrictCV.VStatus.full.instDecidablePredIsEmpty = isFalse not_false

structure FaustLampitelli2026.StrictCV.CVSeq : Type

A Strict-CV sequence is a list of V-slot statuses. C-slots are implicit between each pair ([Low96]). The list [v₁, v₂, v₃] represents the skeleton C₁ V₁ C₂ V₂ C₃ V₃.

• vStatus : List VStatus

@[implicit_reducible]

instance FaustLampitelli2026.StrictCV.instReprCVSeq : Repr CVSeq

Equations

• FaustLampitelli2026.StrictCV.instReprCVSeq = { reprPrec := FaustLampitelli2026.StrictCV.instReprCVSeq.repr }

def FaustLampitelli2026.StrictCV.instReprCVSeq.repr : CVSeq → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance FaustLampitelli2026.StrictCV.instDecidableEqCVSeq : DecidableEq CVSeq

Equations

• FaustLampitelli2026.StrictCV.instDecidableEqCVSeq = FaustLampitelli2026.StrictCV.instDecidableEqCVSeq.decEq

def FaustLampitelli2026.StrictCV.instDecidableEqCVSeq.decEq (x✝ x✝¹ : CVSeq) : Decidable (x✝ = x✝¹)

Equations

• FaustLampitelli2026.StrictCV.instDecidableEqCVSeq.decEq { vStatus := a } { vStatus := b } = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

def FaustLampitelli2026.StrictCV.CVSeq.vCount (s : CVSeq) : ℕ

Equations

• s.vCount = s.vStatus.length

def FaustLampitelli2026.StrictCV.CVSeq.vAt (s : CVSeq) (i : ℕ) : Option VStatus

Equations

• s.vAt i = s.vStatus[i]?

def FaustLampitelli2026.StrictCV.CVSeq.ofList (vs : List VStatus) : CVSeq

Equations

• FaustLampitelli2026.StrictCV.CVSeq.ofList vs = { vStatus := vs }

def FaustLampitelli2026.StrictCV.CVSeq.ProperlyGoverned (s : CVSeq) (i : ℕ) : Prop

Proper Government ([KLV90], simplified per [FL26] eq. 23a): V-slot at index i is properly governed iff V-slot i+1 exists and is contentful.

Equations

• s.ProperlyGoverned i = (s.vAt (i + 1) = some FaustLampitelli2026.StrictCV.VStatus.full)

@[implicit_reducible]

instance FaustLampitelli2026.StrictCV.CVSeq.instDecidableProperlyGoverned (s : CVSeq) (i : ℕ) : Decidable (s.ProperlyGoverned i)

Equations

• s.instDecidableProperlyGoverned i = FaustLampitelli2026.StrictCV.CVSeq.instDecidableProperlyGoverned._aux_1 s i

def FaustLampitelli2026.StrictCV.CVSeq.ECPSatisfied (s : CVSeq) (i : ℕ) : Prop

Empty Category Principle ([Kay92], simplified per [FL26] eq. 23b): an empty V-slot may surface silently iff it is properly governed; a full V-slot is always realized; out-of-range positions vacuously hold.

Equations

• s.ECPSatisfied i = match s.vAt i with | some FaustLampitelli2026.StrictCV.VStatus.empty => s.ProperlyGoverned i | x => True

@[implicit_reducible]

instance FaustLampitelli2026.StrictCV.CVSeq.instDecidableECPSatisfied (s : CVSeq) (i : ℕ) : Decidable (s.ECPSatisfied i)

Equations

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

def FaustLampitelli2026.StrictCV.CVSeq.LicensesPrecedingC (s : CVSeq) (i : ℕ) : Prop

Licensing ([SS01], simplified per [FL26] eq. 24): V-slot at index i licenses its preceding C-position iff i is contentful.

Equations

• s.LicensesPrecedingC i = (s.vAt i = some FaustLampitelli2026.StrictCV.VStatus.full)

@[implicit_reducible]

instance FaustLampitelli2026.StrictCV.CVSeq.instDecidableLicensesPrecedingC (s : CVSeq) (i : ℕ) : Decidable (s.LicensesPrecedingC i)

Equations

• s.instDecidableLicensesPrecedingC i = FaustLampitelli2026.StrictCV.CVSeq.instDecidableLicensesPrecedingC._aux_1 s i

theorem FaustLampitelli2026.StrictCV.CVSeq.empty_not_governed_violates_ecp (s : CVSeq) (i : ℕ) (hempty : s.vAt i = some VStatus.empty) (hpg : ¬s.ProperlyGoverned i) : ¬s.ECPSatisfied i

An empty nucleus that is not properly governed violates ECP.

theorem FaustLampitelli2026.StrictCV.CVSeq.full_ecp_satisfied (s : CVSeq) (i : ℕ) (hfull : s.vAt i = some VStatus.full) : s.ECPSatisfied i

A full nucleus is always ECP-satisfied (vacuous).

§1 Element-Theoretic decomposition of Tigrinya/Tigre segments

The vowel decompositions (paper eq. 20-22)

• [a] = headed |A| (the marked low vowel)
• [ʌ] = bare |A| (the unmarked low vowel; this contrast is paper eq. 21)
• [i] = headed |I|
• [u] = headed |U|
• [e] = headed |I| + bare |A|
• [o] = headed |U| + bare |A|
• [ɨ] = empty bundle (eq. 22 — phonetic realization of an empty vocalic position)

The guttural decompositions (paper eq. 20)

All four attested gutturals contain |A|. The pharyngeal/laryngeal contrast is the headedness of |A|: pharyngeals (ħ, ʕ) are headed by |A|, laryngeals (ʔ, h) have |A| as operator.

def FaustLampitelli2026.vowelET : Tigrinya.Phonology.Vowel → ElementTheory.MR

Element-Theoretic decomposition of Tigrinya/Tigre vowels per [FL26] eq. 20-22.

Equations

• FaustLampitelli2026.vowelET Tigrinya.Phonology.Vowel.a = ElementTheory.MR.headedSimplex ElementTheory.Element.A
• FaustLampitelli2026.vowelET Tigrinya.Phonology.Vowel.aBare = ElementTheory.MR.simplex ElementTheory.Element.A
• FaustLampitelli2026.vowelET Tigrinya.Phonology.Vowel.i = ElementTheory.MR.headedSimplex ElementTheory.Element.I
• FaustLampitelli2026.vowelET Tigrinya.Phonology.Vowel.u = ElementTheory.MR.headedSimplex ElementTheory.Element.U
• FaustLampitelli2026.vowelET Tigrinya.Phonology.Vowel.e = ElementTheory.MR.headPlusOp ElementTheory.Element.I ElementTheory.Element.A
• FaustLampitelli2026.vowelET Tigrinya.Phonology.Vowel.o = ElementTheory.MR.headPlusOp ElementTheory.Element.U ElementTheory.Element.A
• FaustLampitelli2026.vowelET Tigrinya.Phonology.Vowel.weak = ElementTheory.MR.empty

def FaustLampitelli2026.gutturalET : Tigrinya.Phonology.Guttural → ElementTheory.MR

Element-Theoretic decomposition of Tigrinya/Tigre gutturals per paper eq. 20. All gutturals contain |A|; pharyngeals (ħ, ʕ) have |A| as head, laryngeals (ʔ, h) have |A| as operator.

Equations

• FaustLampitelli2026.gutturalET Tigrinya.Phonology.Guttural.glottalStop = ElementTheory.MR.headPlusOp ElementTheory.Element.glottal ElementTheory.Element.A
• FaustLampitelli2026.gutturalET Tigrinya.Phonology.Guttural.h = ElementTheory.MR.headPlusOp ElementTheory.Element.H ElementTheory.Element.A
• FaustLampitelli2026.gutturalET Tigrinya.Phonology.Guttural.pharyngealVoiced = ElementTheory.MR.headPlusOp ElementTheory.Element.A ElementTheory.Element.glottal
• FaustLampitelli2026.gutturalET Tigrinya.Phonology.Guttural.pharyngealVoiceless = ElementTheory.MR.headPlusOp ElementTheory.Element.A ElementTheory.Element.H

def FaustLampitelli2026.VowelHasA (v : Tigrinya.Phonology.Vowel) : Prop

Vowel v contains the |A| element.

Equations

• FaustLampitelli2026.VowelHasA v = (FaustLampitelli2026.vowelET v).HasElement ElementTheory.Element.A

@[implicit_reducible]

instance FaustLampitelli2026.instDecidablePredVowelVowelHasA : DecidablePred VowelHasA

Equations

• FaustLampitelli2026.instDecidablePredVowelVowelHasA v = FaustLampitelli2026.instDecidablePredVowelVowelHasA._aux_1 v

def FaustLampitelli2026.GutturalHasA (g : Tigrinya.Phonology.Guttural) : Prop

Guttural g contains |A|. By paper eq. 20, all four do.

Equations

• FaustLampitelli2026.GutturalHasA g = (FaustLampitelli2026.gutturalET g).HasElement ElementTheory.Element.A

@[implicit_reducible]

instance FaustLampitelli2026.instDecidablePredGutturalGutturalHasA : DecidablePred GutturalHasA

Equations

• FaustLampitelli2026.instDecidablePredGutturalGutturalHasA g = FaustLampitelli2026.instDecidablePredGutturalGutturalHasA._aux_1 g

theorem FaustLampitelli2026.all_gutturals_have_A (g : Tigrinya.Phonology.Guttural) : GutturalHasA g

All four attested gutturals contain |A| (paper eq. 20).

theorem FaustLampitelli2026.pharyngeals_A_headed : (gutturalET Tigrinya.Phonology.Guttural.pharyngealVoiced).IsHead ElementTheory.Element.A ∧ (gutturalET Tigrinya.Phonology.Guttural.pharyngealVoiceless).IsHead ElementTheory.Element.A

Pharyngeals are headed by |A| (paper eq. 20: ħ, ʕ have A underlined as head).

theorem FaustLampitelli2026.laryngeals_A_not_headed : ¬(gutturalET Tigrinya.Phonology.Guttural.glottalStop).IsHead ElementTheory.Element.A ∧ ¬(gutturalET Tigrinya.Phonology.Guttural.h).IsHead ElementTheory.Element.A

Laryngeals (glottals) are NOT headed by |A| (their |A| is operator, not head; paper eq. 20).

§2 Gutturals are low glides (the paper's headline structural claim)

The paper's headline #1 (paper §1, Conclusion §4): a guttural's |A| element associates to a C-slot just as a high vowel's |I| or |U| element associates to a C-slot to surface as a glide. The proof is structural — the ET decomposition (gutturalET) makes every guttural |A|-bearing, captured by all_gutturals_have_A above.

The synersis-engagement consequence (|A| at C fuses with |A| at preceding V via OCP) is in §4 below.

§3 CV-skeletal modeling and worked examples

The synersis configuration

The paper's synersis trigger is /Aᵥ + A_c/ — a low vowel (|A| at a V-slot) adjacent to a guttural (|A| at a C-slot). The CV sequence encoding tracks per-V-slot melodic status. After the analysis applies fusion + dissociation, the V-slot containing the underlying /ʌ/ becomes empty and is licensed silent (per ECP) iff the next V-slot is contentful.

Below we encode the post-fusion forms of the paper's worked examples; the underlying pre-fusion forms differ only in V-slot status (the target V is .full rather than .empty).

def FaustLampitelli2026.afterFusion_nibhi : StrictCV.CVSeq

The Tigrinya /CʌGV/ pattern from paper eq. (10b), surface [niβah] / [nibh-i] 'bark': three V-slots. The IMP.F [nibh-i] form is the syneresis-applied version where, after fusion + dissociation, V₂ (which underlyingly hosted /ʌ/) is empty.

Equations

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

def FaustLampitelli2026.beforeFusion_nibhi : StrictCV.CVSeq

The /CʌGV/ baseline before fusion (the underlying form): V₂ contentful with /ʌ/. The IMP.M [niβah] form realises this underlying state with V₂ surfacing as the lowered [a].

Equations

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

theorem FaustLampitelli2026.nibhi_v2_properly_governed : afterFusion_nibhi.ProperlyGoverned 1

Verify post-fusion V₂ is properly governed by V₃ (which is full).

theorem FaustLampitelli2026.nibhi_v2_ecp_satisfied : afterFusion_nibhi.ECPSatisfied 1

Verify post-fusion V₂ satisfies ECP (empty + properly governed → silent is licit).

def FaustLampitelli2026.arifu_CV : StrictCV.CVSeq

The /ʕarif-u/ CV configuration (paper eq. 19b: /ʕarif-u/ → [ʕarifu]; analyzed in eq. 28c with self-licensing diagram in eq. 28a-b). Three V-slots, all contentful. The fused element at V₁ self-licenses C₁; the self-licensing domain blocks dissociation, so V₂ stays full even though V₃ would govern it.

Equations

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

theorem FaustLampitelli2026.arifu_v2_full : arifu_CV.vAt 1 = some StrictCV.VStatus.full

def FaustLampitelli2026.tisihib_CV : StrictCV.CVSeq

The /CʌGV/ → [CɨGV] case (paper eq. 17): position retained as epenthetic [ɨ] even though V₃ is full. Witness: PASS-PRF [ti-siħib ~ ti-sɨħib] from eq. (17b) for √sħb. Encoded as V₂ = empty (post-fusion) but realised as [ɨ] surfacing rather than silent — discussed at paper §3.3.3 as a position-retention case not predicted by the basic analysis.

Equations

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

theorem FaustLampitelli2026.tisihib_v2_properly_governed : tisihib_CV.ProperlyGoverned 1

§4 Synersis as fused-and-governed; self-licensing block

def FaustLampitelli2026.IsSynersisLicensedSilent (s : StrictCV.CVSeq) (i : ℕ) : Prop

A V-slot is synersis-licensed silent iff (a) it is empty (post-fusion) and (b) it is properly governed. [FL26] eq. (23)-(28).

Equations

• FaustLampitelli2026.IsSynersisLicensedSilent s i = (s.vAt i = some FaustLampitelli2026.StrictCV.VStatus.empty ∧ s.ProperlyGoverned i)

@[implicit_reducible]

instance FaustLampitelli2026.instDecidableIsSynersisLicensedSilent (s : StrictCV.CVSeq) (i : ℕ) : Decidable (IsSynersisLicensedSilent s i)

Equations

• FaustLampitelli2026.instDecidableIsSynersisLicensedSilent s i = FaustLampitelli2026.instDecidableIsSynersisLicensedSilent._aux_1 s i

theorem FaustLampitelli2026.nibhi_synersis_succeeds : IsSynersisLicensedSilent afterFusion_nibhi 1

The post-fusion [nibh-i] form (paper eq. 10b IMP.F) licenses synersis at V₂. The corresponding IMP.M [niβah] (eq. 10b) realises the unfused underlying form.

theorem FaustLampitelli2026.arifu_blocks_synersis : arifu_CV.vAt 1 = some StrictCV.VStatus.full ∧ ¬IsSynersisLicensedSilent arifu_CV 1

Self-licensing blocks dissociation [FL26] eq. (28a-c). When the fused |A| at V₁ self-licenses preceding C₁ in a self-licensing domain, dissociation does NOT apply, and V₂ stays full.

Witness: in /ʕarif-u/, V₂ remains full (containing the /i/ vocalization), and the surface form is [ʕarifu] (eq. 19b/28c) not *[ʕarfu]. The structural prediction is the absence of an empty V₂, despite V₃'s government potential.

NOTE on T3 — "self-licensing domain"

The "self-licensing domain" itself is paper-specific apparatus (paper n. 18: "this cannot be a general principle in Strict CV"). The inlined StrictCV substrate above deliberately does NOT define self-licensing — this study file is where the Faust-specific stipulation lives. T3 captures the prediction (V₂ full ⇒ no synersis) without committing the substrate to the stipulation that generates it.

§5 Economy drives synersis (witness from eq. 18, 39)

theorem FaustLampitelli2026.mibarak_synersis_licensed_no_phonotactic_motivation : have mibarakAfter := StrictCV.CVSeq.ofList [StrictCV.VStatus.full, StrictCV.VStatus.empty, StrictCV.VStatus.full]; IsSynersisLicensedSilent mibarakAfter 1

Economy drives synersis [FL26] §1, eq. 2b, eq. 18c, eq. 39b. The paper's central polemical claim against the simpler "synersis = phonotactic-driven gliding" view (eq. 2a).

Witness: /mibarak/ → [mɨbɨrak] (eq. 18c, 39b). The underlying form has no guttural and no phonotactic problem; yet synersis applies and the position is retained as [ɨ] rather than left full. The paper concludes (§3.3.3): "the absence of syncope is not as straightforward [as a phonotactic explanation predicts]". The form [mibarak] would not pose a phonotactic problem yet [mɨbɨrak] is what surfaces.

Encoded structurally: the /mibarak/ post-fusion sequence has V₂ empty + properly governed, so synersis structurally licenses silence at V₂ even though no guttural is present. The fact that [ɨ] surfaces rather than silence is a separate observation (covered in §7's discussion of n. 23).

§6 Walker & Rose 2015 divergence (with the strongest witness)

def FaustLampitelli2026.identicalVowel_after : StrictCV.CVSeq

The /mismaʕa/ identical-vowel configuration (paper p. 22-23). Both V-flanking vowels are /a/; the medial consonant is the pharyngeal /ʕ/. The F&L analysis predicts synersis applies (V₁ /a/'s |A| fuses with /ʕ/'s |A|, then V₁ becomes empty under proper government).

Identifier note: the IPA name /mismaʕa/ contains the unicode ʕ which is not a valid Lean identifier character, so the def is named identicalVowel_after.

Equations

• FaustLampitelli2026.identicalVowel_after = FaustLampitelli2026.StrictCV.CVSeq.ofList [FaustLampitelli2026.StrictCV.VStatus.empty, FaustLampitelli2026.StrictCV.VStatus.full]

theorem FaustLampitelli2026.identicalVowel_synersis_overshoots_walker_rose : identicalVowel_after.vAt 0 = some StrictCV.VStatus.empty

T4 — Walker & Rose 2015 overshoots [FL26] §3.3.2 critique of [WR15]. Three refutation legs (the third is the strongest and is the one this theorem encodes):

1. /iIu/ → [ju] (vowel + glide synersis): F&L's analysis predicts (extending to non-guttural |I|), W&R's *VαCVβ does not predict synersis here.
2. Glides like /j/ are the consonants least likely to allow harmony, so subjecting them to *VαCVβ is unmotivated.
3. Synersis applies between identical vowels: in /mismʌʕa/ → [mismaʕa], the analysis applies fusion of the /a/ to the |A| of /ʕ/ (creating the structural configuration of synersis), but *VαCVβ does not apply (α = β = /a/).

The third leg is encoded here as a structural witness: the F&L post-fusion form is [.empty, .full] (V₁ vacated by synersis), and W&R's *VαCVβ-based analysis does not yield this empty V₁ from an identical-flanking-vowel input.

The full surface-form prediction comparison requires modeling W&R's constraint apparatus (deferred — W&R 2015 is a handout, not a published paper [WR15] note 22).

§7 OCP merger as instance of the shared substrate

theorem FaustLampitelli2026.fusion_is_collapse_instance : OCP.collapse [ElementTheory.Element.A, ElementTheory.Element.A] = [ElementTheory.Element.A]

The |A|+|A| → fused |A| operation of paper eq. (26) is an instance of OCP.collapse over a tier of Element values: two adjacent |A| elements collapse to one.

This makes structurally explicit that F&L's "fusion" mechanism is the same operation as [Lio22a]'s mergeTRN for Laal tones, just instantiated over a different value space (privative Element vs binary-feature TRN).

theorem FaustLampitelli2026.fusion_output_is_ocp_clean (xs : List ElementTheory.Element) : OCP.IsClean (OCP.collapse xs)

The OCP-merger output is OCP-clean: no two adjacent identical elements remain. Direct application of the substrate theorem OCP.collapse_clean.

§8 Paper-acknowledged scope limits

The paper itself marks several places where its analysis is incomplete or stipulative. These are documented here as the paper states them, not encoded as theorems — over-formalising them would misrepresent the paper's epistemic stance.

• Ejectives also contain |A| but never undergo syneresis (paper n. 8, page 9). Per [LP88] and [Fau17b], ejectives also lower /ʌ/ to [a], suggesting ejectives also bear the |A| element; per [Bel07]:102-153 for an ET implementation. Yet syneresis never applies before ejectives. The paper hypothesises a structural difference between ejectives and gutturals but does not derive it.

• The Tigre [samʕa] underlying form (paper n. 11, page 11). The parallel form to Tigrinya /sʌmʌʕ-ko/ in the Tigre PRF is [samʕako] 'I heard'. But the unsuffixed Tigre PRF base always lacks the second stem vowel regardless of final-C identity (cf. [samʕa] 'he heard' and [fagra] 'he left' per [Raz80]). The paper concludes [samʕako] is probably not underlyingly /sʌmʌʕ-ko/ in Tigre — flagging an unresolved underlying-form question.

• The supposed weakness of gutturals lacks an external definition (paper n. 17, page 16). The premise of eq. (25) — that gutturals must be licensed — is motivated only by the present analysis; the paper acknowledges no prior study defines this weakness satisfactorily, citing only sketches in [Ang95] and [WR15].

• "Licensing overrides government" is not a general Strict-CV principle (paper n. 18, page 16). In many languages, codas (Cs before empty V-slots) are lost or lenited; if licensing always overrode government, epenthesis would always occur to avoid this lenition, contrary to fact. The self-licensing-domain stipulation is therefore paper-specific apparatus; it is documented in §4 of this file as belonging to the study, not the substrate.

• The TGH generalisation predicts an unattested form (paper n. 23, page 24). The paper generalises TGH to derivations like (37b-c), which would predict [siħab] alongside the attested [sahab]. The paper has not encountered [siħab] but expects it to be possible — a predicted-but-unattested gap.

• "Rules apply" generates derivation loops on opaque cases (paper n. 25 + §3.3.3 discussion of eq. 37, pages 24-25). The derivations in eq. (37b-d) raise an issue: under naive "rules apply", the situation created by TGH /sahab/ could be regarded as identical to the environment of fusion+dissociation, leading to loop /sʌħab/ → /s_ħab/ → /sahab/ → /s_hab/ → /sahab/ → … . The paper offers three escape hatches without committing to one: (i) the output of TGH is somehow different from a fused |A|; (ii) epenthesis/TGH is phonetic implementation, post-phonological; (iii) disallow repeated application of operations.

• The realised vowel position in /tisʌħib/ → [tisɨħib] and /mibarak/ → [mɨbɨrak] is not predicted (paper §3.3.3 final paragraph + discussion of eq. 39, page 26). The paper acknowledges "we do not have an insightful explanation for the retention of the position", tentatively invoking [Buc00]'s morpheme-specific alignment for Tigrinya but admitting Tigre lacks the same morpheme-specific requirement.

• The cross-linguistic rarity of |A|-glides remains unexplained (paper §4 conclusion, page 27). The paper concedes "possibly, the absence of guttural sounds from most languages accounts for the lack of more widespread effects of |A| 'glides'" — a typological observation, not a derived prediction.