Berent (2026) @cite{berent-2026}

Three arguments for abstraction in phonology. Glossa: a journal of general linguistics 12(1). 1--24.

Three experimental arguments that phonological grammar is substance-free, algebraic, and amodal:

1. Abstract: syllable structure constraints (sonority sequencing) persist under articulatory suppression (TMS, mechanical) and in print reading, engaging Broca's area rather than motor cortex. Formalized as gradient markedness over the abstract SonorityRank type — the grammar sees only the ordering, not the articulatory features that correlate with it.

2. Algebraic: identity restrictions (*XX ban, OCP) generalize to novel feature values unattested in the speaker's language (Hebrew /θ/, novel ASL handshapes). Formalized as the type-polymorphic mkOCP constraint — Lean's parametric polymorphism IS the algebraic property.

3. Amodal: English speakers project spoken-language doubling constraints onto novel ASL signs, with a phonology--morphology split (identity banned in phonological contexts, reduplication preferred in morphological contexts). Formalized as competing OT parses over DoublingParse (see Theories/Phonology/Doubling.lean).

Formalization strategy

The paper's central claims are metatheoretical — they argue about the nature of phonological representations rather than proposing new formal machinery. The deepest formalization insight is that Lean's type system already embodies the distinctions Berent draws:

• Substance-free = SonorityRank is an abstract ordered type, not defined by articulatory features (refactored in Syllable/Defs.lean)
• Algebraic = mkOCP is parametrically polymorphic over α (added to Constraints.lean)
• Amodal = the same polymorphic constraint applies to any feature type, spoken or signed, by construction

The doubling theory (types, constraints, L1-parameterized model) is factored into Theories/Phonology/Doubling.lean. The experimental data supporting the doubling reversal is in @cite{berent-bat-el-brentari-dupuis-vaknin-nusbaum-2016}.

@cite{berent-2026}

inductive Berent2026.OnsetProfile : Type

Onset sonority profile: the relationship between C1 and C2 sonority in a two-segment onset.

The behavioral gradient rise > plateau > fall (@cite{berent-2026}, Figure 1A; data from Berent et al. 2007) maps directly to this classification on the abstract SonorityRank type.

• rise : OnsetProfile
• plateau : OnsetProfile
• fall : OnsetProfile

@[implicit_reducible]

instance Berent2026.instDecidableEqOnsetProfile : DecidableEq OnsetProfile

Equations

• Berent2026.instDecidableEqOnsetProfile x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Berent2026.instReprOnsetProfile.repr : OnsetProfile → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Berent2026.instReprOnsetProfile : Repr OnsetProfile

Equations

• Berent2026.instReprOnsetProfile = { reprPrec := Berent2026.instReprOnsetProfile.repr }

def Berent2026.onsetProfile (c1 c2 : Phonology.Syllable.SonorityRank) : OnsetProfile

Classify a two-segment onset by its sonority profile. Operates on SonorityRank — the abstract hierarchy — not on articulatory features.

Equations

• Berent2026.onsetProfile c1 c2 = if c1.rank < c2.rank then Berent2026.OnsetProfile.rise else if (c1.rank == c2.rank) = true then Berent2026.OnsetProfile.plateau else Berent2026.OnsetProfile.fall

def Berent2026.onsetSSP : Core.Constraint.OT.NamedConstraint OnsetProfile

Onset markedness as an OT constraint: gradient violations by sonority profile. Uses mkMarkGrad from the shared constraint library.

Rise = 0 violations, plateau = 1, fall = 2. This captures the behavioral gradient (blif > bnif > bdif > lbif; @cite{berent-2026}, data from Berent et al. 2007). The gradient is determined entirely by the abstract SonorityRank ordering — the grammar does not inspect whether "rise" means "stop-before-liquid" vs. "nasal-before-vowel".

Equations

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

@[reducible, inline]

abbrev Berent2026.onsetMarkedness : OnsetProfile → ℕ

Gradient markedness of onset sonority profiles (convenience alias).

Equations

• Berent2026.onsetMarkedness = Berent2026.onsetSSP.eval

theorem Berent2026.rise_lt_plateau : onsetMarkedness OnsetProfile.rise < onsetMarkedness OnsetProfile.plateau

theorem Berent2026.plateau_lt_fall : onsetMarkedness OnsetProfile.plateau < onsetMarkedness OnsetProfile.fall

theorem Berent2026.rise_unmarked : onsetMarkedness OnsetProfile.rise = 0

theorem Berent2026.sonority_gradient_abstract (r1 r2 : Phonology.Syllable.SonorityRank) : onsetMarkedness (onsetProfile r1 r2) = if r1.rank < r2.rank then 0 else if (r1.rank == r2.rank) = true then 1 else 2

The sonority gradient is determined by abstract rank, not by features. Two segments with the same SonorityRank are treated identically regardless of their articulatory specification.

theorem Berent2026.ocp_detects_aa {α : Type} [DecidableEq α] (a : α) (rest : List α) : Phonology.Constraints.adjacentIdentical (a :: a :: rest) = 1 + Phonology.Constraints.adjacentIdentical (a :: rest)

OCP detects adjacent identity.

theorem Berent2026.ocp_passes_ab {α : Type} [DecidableEq α] (a b : α) (rest : List α) (h : a ≠ b) : Phonology.Constraints.adjacentIdentical (a :: b :: rest) = Phonology.Constraints.adjacentIdentical (b :: rest)

OCP passes over non-identical adjacency.

theorem Berent2026.amodal_doubling_reversal : (Core.Constraint.OT.mkTableau Phonology.Doubling.phonCandidates Phonology.Doubling.phonRanking ⋯).optimal = {Phonology.Doubling.DoublingParse.nonidentical} ∧ (Core.Constraint.OT.mkTableau Phonology.Doubling.morphCandidates Phonology.Doubling.morphRanking ⋯).optimal = {Phonology.Doubling.DoublingParse.reduplication}

The phonology--morphology reversal: the same OCP-XX produces opposite surface preferences depending on whether the morphological context licenses reduplication.

This is the core of @cite{berent-2026}'s third argument: the reversal is amodal (it transfers from speech to sign) and L1-dependent (it depends on the speaker's morphological system). See Phonology.Doubling.doubling_reversal for the proof and @cite{berent-bat-el-brentari-dupuis-vaknin-nusbaum-2016} for the experimental evidence.

Both doubling tableaux lift to generic ConstraintSystems via tableauSystem. The phonology--morphology reversal then becomes a probability-1 reversal: the same OCP-XX assigns probability 1 to .nonidentical in phonological contexts and to .reduplication in morphological contexts.

noncomputable def Berent2026.phonSystem : Core.Constraint.ConstraintSystem Phonology.Doubling.DoublingParse (Core.Constraint.LexProfile ℕ 2)

Phonological-context tableau as a generic ConstraintSystem.

Equations

• Berent2026.phonSystem = Core.Constraint.tableauSystem (Core.Constraint.OT.mkTableau Phonology.Doubling.phonCandidates Phonology.Doubling.phonRanking Berent2026.phonSystem._proof_1)

theorem Berent2026.phonSystem_predict_nonidentical : phonSystem.predict Phonology.Doubling.DoublingParse.nonidentical = 1

In phonological contexts, .nonidentical has probability 1.

noncomputable def Berent2026.morphSystem : Core.Constraint.ConstraintSystem Phonology.Doubling.DoublingParse (Core.Constraint.LexProfile ℕ 3)

Morphological-context tableau as a generic ConstraintSystem.

Equations

• Berent2026.morphSystem = Core.Constraint.tableauSystem (Core.Constraint.OT.mkTableau Phonology.Doubling.morphCandidates Phonology.Doubling.morphRanking Berent2026.morphSystem._proof_1)

theorem Berent2026.morphSystem_predict_reduplication : morphSystem.predict Phonology.Doubling.DoublingParse.reduplication = 1

In morphological contexts where reduplication is available, .reduplication has probability 1.