Albright & Hayes (2003): Rules vs. analogy in English past tenses

[AH03] [Ber58] [AH02] [Mik97] [PP88] [BM83]

A computational/experimental study of how speakers form past tenses for novel English verbs (wug verbs). The paper's central architectural claim is that morphological knowledge is best modelled as multiple stochastic rules — each with a structural description, a scope, a hit count, and an adjusted-confidence score — and that this model fits human wug-test data better than either a purely analogical model or a single-default-rule dual-mechanism model.

Architectural commitments

Three positions are at stake:

• Single-default-rule dual-mechanism: regular pasts are derived by a single, context-free rule; only irregular pasts are sensitive to phonological context. Predicts that novel-word ratings of regular pasts are invariant in the phonological context of the stem.
• Pure analogy (e.g. GCM-style): all generalisation flows from variegated similarity to existing lexemes. No structured rules; the influence of a model form on a novel form can ride on any feature.
• Multiple stochastic rules (this paper): the lexicon supplies many rules per change, each restricted to a structurally-defined context. A novel form's past-tense rating depends on the adjusted confidence of the most accurate rule whose structural description it satisfies. Predicts both regular and irregular ratings vary with phonological context — specifically, with island-of-reliability membership.

Empirical core: islands of reliability for both regulars and irregulars

A&H's central empirical contribution is that wug ratings of regular past tenses also show context sensitivity, contrary to the single-default-rule prediction. The 4-way Core stimulus design crosses island-of-reliability (IOR) status for regulars × IOR for irregulars, and the published rating data show:

• ratings F(1, 78) = 27.23, P < 0.0001 main effect of islandhood
• production-probability F(1, 78) = 14.05, P < 0.001 main effect of islandhood

with no significant interaction. Both regulars and irregulars are sensitive to IOR membership.

What this file formalises

The shared wug-paradigm vocabulary (formerly Morphology/WugTest.lean, dissolved into this file 2026-07-17) is declared below the module docstring; [BKK26] imports it from here. The paper-specific content supplies:

• The 4-way IOR Core wug stem set (example 14 in the paper);
• A StochasticRule type with scope/hits/rawConfidence;
• A note on Mikheev (1997) lower-confidence-limit adjustment, kept as an abstract specification rather than a numerical implementation;
• An AHWugCell type that participates in the WugTest contract via HasAttestation;
• A local typeclass HasIORForRegular (binary IOR factor — the WugTest HasFrequency analogue for the discrete IOR dimension);
• Two paradigm-level predicates NovelRegularsShowIORGradient and NovelRegularsInvariantInIOR;
• A structural discriminator novelRegularsGradient_inconsistent_with_invariance;
• A concrete A&H step-function model that satisfies the gradient and hence rules out the single-default-rule prediction by structural impossibility.

Out of scope

Per CLAUDE.md "do not encode conclusions as definitions": we do not formalise the numerical correlation tables (r = 0.745 etc.) as Lean theorems with rfl proofs. The numbers are reported in prose and the paper-side citation. We formalise the qualitative prediction-shape contrasts that the empirical correlations support.

We also do not implement the [Mik97] lower-confidence-limit interval. The discriminator below depends only on rawConfidence and on the qualitative shape of the prediction (gradient on novel cells across IOR membership), not on the adjustment formula. We expose adjustedConfidence as a placeholder definition equal to rawConfidence so that downstream code can reference the API name; wiring this to a real Wilson interval (or the [AH02] MGL implementation) is deferred.

Wug-paradigm vocabulary ([Ber58])

Shared typed vocabulary for wug studies, homed in the modern reference paper for gradient wug responses (its other consumer, [BKK26], imports this file). [Ber58] introduced the test as a probe for productive morpho-phonological knowledge: presented with the nonce wug, children produce wugs /wʌgz/ rather than refusing or randomising. A single parametric lens class HasFactor (with lens laws) plus a Rate observable lets studies state the qualitative discriminator between grammar-locus accounts of productivity (novel forms show a factor gradient: indexed-constraint [Pat10], scaled-weight [CP08b]) and listing-locus accounts (novel forms are factor-invariant: UseListed [Zur00]).

inductive Morphology.WugTest.Attestation : Type

Whether a stimulus is an attested lexical item or a novel (nonce, wug-like) form. The basic categorical contrast that [Ber58] introduced and that every wug paradigm crosses.

• attested : Attestation
• novel : Attestation

@[instance_reducible]

instance Morphology.WugTest.instDecidableEqAttestation : DecidableEq Attestation

Equations

• Morphology.WugTest.instDecidableEqAttestation x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Morphology.WugTest.instReprAttestation : Repr Attestation

Equations

• Morphology.WugTest.instReprAttestation = { reprPrec := Morphology.WugTest.instReprAttestation.repr }

def Morphology.WugTest.instReprAttestation.repr : Attestation → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Morphology.WugTest.instInhabitedAttestation : Inhabited Attestation

Equations

• Morphology.WugTest.instInhabitedAttestation = { default := Morphology.WugTest.instInhabitedAttestation.default }

@[instance_reducible]

instance Morphology.WugTest.instFintypeAttestation : Fintype Attestation

Equations

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

Studies' Cell types vary in what additional factors they cross (item, paradigm slot, frequency stratum, IOR membership, …). The shared minimum is that every wug cell carries some collection of factors and a way to swap each one without touching others. The lens laws (get_set, set_get, set_set) make setFactor a proper lens; the paradigm-level predicates rely on them to express "swapping the factor changes the rate" as a statement that quantifies over the rest of the cell uniformly.

HasFactor takes the codomain F as a parameter so that one schema covers Attestation (categorical), ℝ (frequency), Bool (binary IOR membership), and any other factor a future study introduces. Each Cell declares one HasFactor instance per factor it exposes; typeclass synthesis routes by the requested F.

class Morphology.WugTest.HasFactor (Cell F : Type) : Type

A lens on Cell exposing a factor of type F.

• factorOf : Cell → F
• setFactor : F → Cell → Cell
• factorOf_setFactor (f : F) (c : Cell) : factorOf (setFactor f c) = f
• setFactor_factorOf (c : Cell) : setFactor (factorOf c) c = c
• setFactor_setFactor (f₁ f₂ : F) (c : Cell) : setFactor f₁ (setFactor f₂ c) = setFactor f₁ c

@[reducible, inline]

abbrev Morphology.WugTest.HasAttestation (Cell : Type) : Type

Cell has an attestation factor that can be swapped without touching other factors. The [Ber58] dimension.

Equations

• Morphology.WugTest.HasAttestation Cell = Morphology.WugTest.HasFactor Cell Morphology.WugTest.Attestation

@[reducible, inline]

abbrev Morphology.WugTest.HasFrequency (Cell : Type) : Type

Cell exposes a real-valued frequency factor (e.g. log token frequency of the source lexeme; log corpus frequency of an analogous attested compound). Frequency is ℝ-valued because lexical-frequency theories ([CP08b], [CK13a]) operate on log frequencies as a continuous regressor.

Equations

• Morphology.WugTest.HasFrequency Cell = Morphology.WugTest.HasFactor Cell ℝ

@[reducible, inline]

abbrev Morphology.WugTest.Rate (Cell R : Type) : Type

Per-cell numeric outcome — the wug paradigm's primary observable. Polymorphic over the codomain R so that empirical tables (ℚ proportions) and theory predictions (ℝ log-odds, MaxEnt probabilities) can both ride along the same predicate machinery.

Equations

• Morphology.WugTest.Rate Cell R = (Cell → R)

These predicates state empirical patterns at the paradigm level. They are written in terms of setFactor (the lens), so any Cell type with the relevant HasFactor instances can claim them without re-deriving the universal quantification per study. The predicates are abstract; they express a shape ("novel forms show a factor gradient") that empirical studies and theoretical models may or may not satisfy.

def Morphology.WugTest.NovelShowsFactorGradient {Cell F R : Type} [HasAttestation Cell] [HasFactor Cell F] [LT F] [LT R] (rate : Rate Cell R) : Prop

A rate observable shows the novel-form factor gradient if, holding all other factors constant and fixing attestation = novel, varying the F-typed factor strictly varies the rate. This is the prediction of indexed-constraint ([Pat10]), scaled-weight ([CP08b]), and representation-strength ([MC21], [SG16]) theories: novel forms inherit a frequency-conditioned grammar pressure from analogous lexical items and therefore show a factor gradient even though they are themselves unlisted.

Equations

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

def Morphology.WugTest.NovelInvariantInFactor {Cell F R : Type} [HasAttestation Cell] [HasFactor Cell F] (rate : Rate Cell R) : Prop

A rate observable is factor-invariant on novel forms if, holding all other factors constant and fixing attestation = novel, varying the F-typed factor leaves the rate unchanged. This is the prediction of UseListed ([Zur00]): novel forms have no lexical entry, so no entry-keyed factor lookup can affect their grammar pressure. The two hypotheses thus make opposite predictions on the same paradigm cell.

Equations

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

@[reducible, inline]

abbrev Morphology.WugTest.NovelShowsFreqGradient {Cell R : Type} [HasAttestation Cell] [HasFrequency Cell] [LT R] (rate : Rate Cell R) : Prop

Frequency-specific spelling of NovelShowsFactorGradient at F := ℝ. Kept as an abbrev for readability at use sites where "frequency gradient" is the linguist-facing terminology.

Equations

• Morphology.WugTest.NovelShowsFreqGradient rate = Morphology.WugTest.NovelShowsFactorGradient rate

@[reducible, inline]

abbrev Morphology.WugTest.NovelInvariantInFrequency {Cell R : Type} [HasAttestation Cell] [HasFrequency Cell] (rate : Rate Cell R) : Prop

Frequency-specific spelling of NovelInvariantInFactor at F := ℝ.

Equations

• Morphology.WugTest.NovelInvariantInFrequency rate = Morphology.WugTest.NovelInvariantInFactor rate

theorem Morphology.WugTest.novelGradient_inconsistent_with_invariance {Cell F R : Type} [HasAttestation Cell] [HasFactor Cell F] [LT F] [Preorder R] (rate : Rate Cell R) (h_grad : NovelShowsFactorGradient rate) (h_inv : NovelInvariantInFactor rate) (c : Cell) (f₁ f₂ : F) (h_lt : f₁ < f₂) : False

The two predictions are structurally incompatible: any rate observable that satisfies both NovelShowsFactorGradient and NovelInvariantInFactor at the same factor type F must have a vacuous factor space (no two F-distinct values). On any cell whose typeclasses permit f₁ < f₂ for some F-typed factors, the predicates are mutually exclusive — exactly the discriminator a wug paradigm is supposed to provide.

For binary factors (F := Bool), the precondition f₁ < f₂ is discharged automatically by Bool.false_lt_true; for real-valued factors (F := ℝ) any concrete pair like (0 : ℝ) < 1 works.

This is the structural source of the empirical claim that wug paradigms can adjudicate between grammar-locus and listing-locus accounts of productivity: the bridge theorem is a single application of this lemma to a study's cell type.

structure AlbrightHayes2003.IORCategory : Type

Island-of-reliability category for a wug stem. The 4-way Core design crosses (IOR for regulars) × (IOR for irregulars); a stem is in exactly one cell, picked out by two booleans. Structural encoding via product avoids the 4-way enum + 2 helper accessors pattern: the cells of a 2×2 design are the boolean product. Table 3 of [AH03].

• iorForRegular : Bool

  Whether the stem is in an island of reliability for the regular allomorph. Example for regular = true: bredge /brɛdʒ/.

• iorForIrregular : Bool

  Whether the stem is in an island of reliability for some irregular pattern. Example for iorForIrregular = true only: spling /splɪŋ/ (close to spring/sling/sting).

def AlbrightHayes2003.instDecidableEqIORCategory.decEq (x✝ x✝¹ : IORCategory) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance AlbrightHayes2003.instDecidableEqIORCategory : DecidableEq IORCategory

Equations

• AlbrightHayes2003.instDecidableEqIORCategory = AlbrightHayes2003.instDecidableEqIORCategory.decEq

@[instance_reducible]

instance AlbrightHayes2003.instReprIORCategory : Repr IORCategory

Equations

• AlbrightHayes2003.instReprIORCategory = { reprPrec := AlbrightHayes2003.instReprIORCategory.repr }

def AlbrightHayes2003.instReprIORCategory.repr : IORCategory → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance AlbrightHayes2003.instInhabitedIORCategory : Inhabited IORCategory

Equations

• AlbrightHayes2003.instInhabitedIORCategory = { default := AlbrightHayes2003.instInhabitedIORCategory.default }

Named cells of Table 3, retained as abbrevs so that

paper-side terminology survives in the witness definitions.

@[reducible, inline]

abbrev AlbrightHayes2003.IORCategory.regAndIrreg : IORCategory

IOR for both regulars and irregulars: e.g. dize.

Equations

• AlbrightHayes2003.IORCategory.regAndIrreg = { iorForRegular := true, iorForIrregular := true }

@[reducible, inline]

abbrev AlbrightHayes2003.IORCategory.regOnly : IORCategory

IOR for regulars only: e.g. bredge.

Equations

• AlbrightHayes2003.IORCategory.regOnly = { iorForRegular := true, iorForIrregular := false }

@[reducible, inline]

abbrev AlbrightHayes2003.IORCategory.irregOnly : IORCategory

IOR for irregulars only: e.g. spling.

Equations

• AlbrightHayes2003.IORCategory.irregOnly = { iorForRegular := false, iorForIrregular := true }

@[reducible, inline]

abbrev AlbrightHayes2003.IORCategory.neither : IORCategory

IOR for neither: e.g. gude.

Equations

• AlbrightHayes2003.IORCategory.neither = { iorForRegular := false, iorForIrregular := false }

structure AlbrightHayes2003.WugStem : Type

A wug stem with its IPA form and its IOR category. The IPA strings are taken verbatim from example (14) of [AH03].

• ipa : String
• category : IORCategory

@[instance_reducible]

instance AlbrightHayes2003.instReprWugStem : Repr WugStem

Equations

• AlbrightHayes2003.instReprWugStem = { reprPrec := AlbrightHayes2003.instReprWugStem.repr }

def AlbrightHayes2003.instReprWugStem.repr : WugStem → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance AlbrightHayes2003.instInhabitedWugStem : Inhabited WugStem

Equations

• AlbrightHayes2003.instInhabitedWugStem = { default := AlbrightHayes2003.instInhabitedWugStem.default }

Sample stems from each cell of Table 3 (example 14)

def AlbrightHayes2003.stem_dize : WugStem

Equations

• AlbrightHayes2003.stem_dize = { ipa := "daɪz", category := AlbrightHayes2003.IORCategory.regAndIrreg }

def AlbrightHayes2003.stem_fro : WugStem

Equations

• AlbrightHayes2003.stem_fro = { ipa := "fro", category := AlbrightHayes2003.IORCategory.regAndIrreg }

def AlbrightHayes2003.stem_rife : WugStem

Equations

• AlbrightHayes2003.stem_rife = { ipa := "raɪf", category := AlbrightHayes2003.IORCategory.regAndIrreg }

def AlbrightHayes2003.stem_bredge : WugStem

Equations

• AlbrightHayes2003.stem_bredge = { ipa := "brɛdʒ", category := AlbrightHayes2003.IORCategory.regOnly }

def AlbrightHayes2003.stem_gezz : WugStem

Equations

• AlbrightHayes2003.stem_gezz = { ipa := "gɛz", category := AlbrightHayes2003.IORCategory.regOnly }

def AlbrightHayes2003.stem_nace : WugStem

Equations

• AlbrightHayes2003.stem_nace = { ipa := "nes", category := AlbrightHayes2003.IORCategory.regOnly }

def AlbrightHayes2003.stem_fleep : WugStem

Equations

• AlbrightHayes2003.stem_fleep = { ipa := "flip", category := AlbrightHayes2003.IORCategory.irregOnly }

def AlbrightHayes2003.stem_gleed : WugStem

Equations

• AlbrightHayes2003.stem_gleed = { ipa := "glid", category := AlbrightHayes2003.IORCategory.irregOnly }

def AlbrightHayes2003.stem_spling : WugStem

Equations

• AlbrightHayes2003.stem_spling = { ipa := "splɪŋ", category := AlbrightHayes2003.IORCategory.irregOnly }

def AlbrightHayes2003.stem_gude : WugStem

Equations

• AlbrightHayes2003.stem_gude = { ipa := "gud", category := AlbrightHayes2003.IORCategory.neither }

def AlbrightHayes2003.stem_nung : WugStem

Equations

• AlbrightHayes2003.stem_nung = { ipa := "nʌŋ", category := AlbrightHayes2003.IORCategory.neither }

def AlbrightHayes2003.stem_preak : WugStem

Equations

• AlbrightHayes2003.stem_preak = { ipa := "prik", category := AlbrightHayes2003.IORCategory.neither }

inductive AlbrightHayes2003.PastChange : Type

A past-tense structural change (the "input → output" half of a rule). The three regular allomorphs and a residual category for vowel-changing irregulars and zero-derivation.

• suffixD : PastChange
• suffixT : PastChange
• suffixSchwaD : PastChange
• vowelChange : PastChange
• noChange : PastChange

@[instance_reducible]

instance AlbrightHayes2003.instDecidableEqPastChange : DecidableEq PastChange

Equations

• AlbrightHayes2003.instDecidableEqPastChange x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance AlbrightHayes2003.instReprPastChange : Repr PastChange

Equations

• AlbrightHayes2003.instReprPastChange = { reprPrec := AlbrightHayes2003.instReprPastChange.repr }

def AlbrightHayes2003.instReprPastChange.repr : PastChange → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance AlbrightHayes2003.instInhabitedPastChange : Inhabited PastChange

Equations

• AlbrightHayes2003.instInhabitedPastChange = { default := AlbrightHayes2003.instInhabitedPastChange.default }

def AlbrightHayes2003.PastChange.isRegular : PastChange → Bool

Whether a past-tense change is one of the three regular suffixes.

Equations

• AlbrightHayes2003.PastChange.suffixD.isRegular = true
• AlbrightHayes2003.PastChange.suffixT.isRegular = true
• AlbrightHayes2003.PastChange.suffixSchwaD.isRegular = true
• AlbrightHayes2003.PastChange.vowelChange.isRegular = false
• AlbrightHayes2003.PastChange.noChange.isRegular = false

structure AlbrightHayes2003.StochasticRule : Type

A stochastic rule: a structural change applied in a structurally- defined context, together with its scope (number of forms in the lexicon meeting the structural description) and hits (number of those forms on which the change actually obtains).

The bundled invariant hits ≤ scope is a real-data property of rules extracted by a minimal-generalization procedure: every form counted as a hit must be in the scope. This is the structural fact that makes rawConfidence ≤ 1.

The structural-description / context is kept abstract — A&H's rules are extracted from the lexicon by a minimal-generalization procedure, and the discriminator below does not depend on any specific encoding of the contexts.

• change : PastChange
• scope : ℕ
• hits : ℕ
• hits_le_scope : self.hits ≤ self.scope

def AlbrightHayes2003.instReprStochasticRule.repr : StochasticRule → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance AlbrightHayes2003.instReprStochasticRule : Repr StochasticRule

Equations

• AlbrightHayes2003.instReprStochasticRule = { reprPrec := AlbrightHayes2003.instReprStochasticRule.repr }

def AlbrightHayes2003.StochasticRule.rawConfidence (r : StochasticRule) : ℚ

Raw confidence: hits / scope. Defaults to 0 when scope = 0 to avoid division by zero; that case never arises for a rule extracted from real data. [AH03].

Equations

• r.rawConfidence = if r.scope = 0 then 0 else ↑r.hits / ↑r.scope

theorem AlbrightHayes2003.StochasticRule.rawConfidence_le_one (r : StochasticRule) : r.rawConfidence ≤ 1

rawConfidence ≤ 1 follows structurally from hits_le_scope.

noncomputable def AlbrightHayes2003.adjustedConfidence (r : StochasticRule) : ℚ

[Mik97] lower-confidence-limit adjustment to raw confidence, used by [AH03] to penalise rules supported by few forms; A&H §2.3.4 reports the best-fit lower- confidence-limit parameter α = 0.55.

TODO: this is a placeholder equal to rawConfidence. A faithful implementation would apply the Wilson-style interval used in the [AH02] MGL code. The discriminator below depends on rawConfidence, not on this adjustment, so the placeholder is sound for the present proof obligations.

Equations

• AlbrightHayes2003.adjustedConfidence r = r.rawConfidence

structure AlbrightHayes2003.AHWugCell : Type

A cell in the A&H wug-rating paradigm. Carries:

• the stem being rated;
• whether the stem is presented as a wug (novel) or a real verb (attested) — A&H's cross-paradigm comparison;
• the IOR-for-regular factor — the propositional phonological- context dimension that A&H's experiments turn on. The field is Prop rather than Bool because IOR-membership is a propositional property of the stimulus, not a designed numeric coordinate; mathlib quality requires Prop with [Decidable] for such fields rather than Bool standing in for a proposition.

• stem : WugStem
• attestation : Morphology.WugTest.Attestation
• withinIORForRegular : Prop

@[instance_reducible]

instance AlbrightHayes2003.AHWugCell.instHasAttestation : Morphology.WugTest.HasAttestation AHWugCell

The wug-vocabulary HasAttestation instance: BKK and A&H both use the same wug paradigm contract. Lens laws by rfl on the structure projections.

Equations

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

@[reducible, inline]

abbrev AlbrightHayes2003.HasIORForRegular (Cell : Type) : Type

A&H's discriminator runs on the categorical island membership dimension; the WugTest paradigm contract handles this through the HasFactor Cell Prop specialisation, parallel to HasFrequency = HasFactor Cell ℝ. The lens-law shape is shared.

The Prop factor inherits its < from mathlib's complete-Boolean- algebra structure on Prop (p < q ↔ (p → q) ∧ ¬(q → p)), so NovelShowsFactorGradient (F := Prop) instantiates to "rate is strictly higher under any pair where the second IOR proposition strictly entails the first" — exactly A&H's prediction reading IOR as a propositional property.

Equations

• AlbrightHayes2003.HasIORForRegular Cell = Morphology.WugTest.HasFactor Cell Prop

@[instance_reducible]

instance AlbrightHayes2003.AHWugCell.instHasIORForRegular : HasIORForRegular AHWugCell

Equations

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

@[reducible, inline]

abbrev AlbrightHayes2003.NovelRegularsShowIORGradient {Cell R : Type} [Morphology.WugTest.HasAttestation Cell] [HasIORForRegular Cell] [LT R] (rate : Morphology.WugTest.Rate Cell R) : Prop

A rate observable shows the novel-regulars IOR gradient if, on novel cells, switching the IOR-for-regular factor from false to true strictly raises the rate. The shared paradigm-level predicate NovelShowsFactorGradient (F := Bool) already expresses exactly this: the only Bool pair satisfying f₁ < f₂ is false < true. This is the A&H multiple-stochastic-rule prediction: novel regulars receive higher ratings when the stem occupies an island where the regular allomorph works particularly well.

Equations

• AlbrightHayes2003.NovelRegularsShowIORGradient rate = Morphology.WugTest.NovelShowsFactorGradient rate

@[reducible, inline]

abbrev AlbrightHayes2003.NovelRegularsInvariantInIOR {Cell R : Type} [Morphology.WugTest.HasAttestation Cell] [HasIORForRegular Cell] (rate : Morphology.WugTest.Rate Cell R) : Prop

A rate observable is invariant in IOR for novel regulars if, on novel cells, switching the IOR-for-regular factor leaves the rate unchanged. This is the single-default-rule dual-mechanism prediction: regular pasts are derived by one rule whose confidence does not vary with phonological context, so novel regular ratings cannot vary with IOR membership. Specialises NovelInvariantInFactor (F := Prop).

Equations

• AlbrightHayes2003.NovelRegularsInvariantInIOR rate = Morphology.WugTest.NovelInvariantInFactor rate

These definitions are concrete witnesses that the A&H prediction- shape NovelRegularsShowIORGradient is realised by a model. The model is a step function: ratings on IOR=true cells equal slope, ratings on IOR=false cells equal 0. The shape is intentionally minimal — the goal is to exhibit a model satisfying the gradient, not to fit the empirical numbers.

noncomputable def AlbrightHayes2003.ahRegularRating (slope : ℝ) (c : AHWugCell) : ℝ

Step-function regular-rating model: rating = slope when the IOR-for-regular proposition holds, 0 otherwise. A faithful proxy for the monotonic relationship between IOR-supported rule- confidence and novel-form ratings reported in [AH03] for the regulars panel. Noncomputable because the IOR-for-regular field is Prop rather than Bool; Classical.propDecidable discharges the Decidable-of-if.

Equations

• AlbrightHayes2003.ahRegularRating slope c = if c.withinIORForRegular then slope else 0

theorem AlbrightHayes2003.ah_satisfies_NovelRegularsShowIORGradient (slope : ℝ) (hSlope : 0 < slope) : NovelRegularsShowIORGradient (ahRegularRating slope)

A&H's model satisfies NovelRegularsShowIORGradient for any positive rating slope. The Prop-valued IOR factor satisfies f₁ < f₂ iff f₁ → f₂ and ¬(f₂ → f₁); the only consistent case (modulo classical reasoning) is ¬f₁ ∧ f₂, on which the rate jumps from 0 to slope.

def AlbrightHayes2003.cell_bredge : AHWugCell

A concrete AHWugCell witness — the wug stem bredge (regulars-only IOR) presented as a novel form. Used as the discriminator-corollary witness below.

Equations

• AlbrightHayes2003.cell_bredge = { stem := AlbrightHayes2003.stem_bredge, attestation := Morphology.WugTest.Attestation.novel, withinIORForRegular := True }

theorem AlbrightHayes2003.ah_excludes_singleDefaultRule (slope : ℝ) (hSlope : 0 < slope) : ¬NovelRegularsInvariantInIOR (ahRegularRating slope)

A&H rules out the single-default-rule dual-mechanism prediction (the [PP88] family). Wired through Morphology/WugTest.lean's novelGradient_inconsistent_with_invariance at F := Bool: the empirical fact that novel regulars show an IOR gradient is structurally incompatible with the single-rule prediction that novel regulars are invariant in phonological context. Any account in the latter family is ruled out by structural impossibility, not just empirical fit.

NB: this discriminator only captures A&H's anti-dual-mechanism prong. A&H also argue against pure analogy via §4.3.2 ("Failure of the analogical model to locate islands of reliability"); the structured-vs-variegated similarity contrast that drives the anti-analogy prong is not formalised here. See [BM83] for the analogical tradition A&H argue against.