@cite{kwon-lee-2026}: Accessibility Markers in Korean

@cite{ariel-2001} @cite{carminati-2002} @cite{kweon-2011} @cite{contemori-di-domenico-2021} @cite{zhang-kwon-2022} @cite{choe-2021}

Three experiments test @cite{ariel-2001}'s Accessibility Theory in Korean — a discourse-oriented language without verbal/gender agreement — using null pronouns, overt kyay, and full NPs. The Experiment 3 antecedent-choice data (71% / 43% / 35% subject bias) instantiates the universal accessibility ordering at three points; the relative ordering holds cross-linguistically while the spread is language-specific.

KoreanRefForm is the 3-element domain tested. It carries a LinearOrder lifted from AccessibilityLevel.rank, so the central claim "subject bias increases in accessibility" appears as one StrictMono lemma (subjectBias_strictMono) rather than per-pair inequalities. Bridges to @cite{kehler-rohde-2013} (topichood), @cite{carminati-2002} (PAH alternative), and Ariel's AccessibilityAssessment are provided.

inductive KwonLee2026.KoreanRefForm : Type

The three Korean referential forms tested across the experiments. Each instantiates a different point on @cite{ariel-2001}'s Accessibility Marking Scale.

• nullPro : KoreanRefForm

  Null pronoun (pro): no phonological exponent.

• overt : KoreanRefForm

  Overt colloquial 3sg pronoun kyay (걔), gender-neutral, derived from ku ai ('that child').

• fullNP : KoreanRefForm

  Full NP — demonstrative + noun (e.g., ku chinkwu 'that friend').

@[implicit_reducible]

instance KwonLee2026.instDecidableEqKoreanRefForm : DecidableEq KoreanRefForm

Equations

• KwonLee2026.instDecidableEqKoreanRefForm x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance KwonLee2026.instReprKoreanRefForm : Repr KoreanRefForm

Equations

• KwonLee2026.instReprKoreanRefForm = { reprPrec := KwonLee2026.instReprKoreanRefForm.repr }

def KwonLee2026.instReprKoreanRefForm.repr : KoreanRefForm → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance KwonLee2026.instBEqKoreanRefForm : BEq KoreanRefForm

Equations

• KwonLee2026.instBEqKoreanRefForm = { beq := KwonLee2026.instBEqKoreanRefForm.beq }

def KwonLee2026.instBEqKoreanRefForm.beq : KoreanRefForm → KoreanRefForm → Bool

Equations

• KwonLee2026.instBEqKoreanRefForm.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def KwonLee2026.KoreanRefForm.toAccessibility : KoreanRefForm → Features.AccessibilityLevel

Map each Korean form to its position on @cite{ariel-2001}'s 18-level scale.

kyay maps to unstressedPron rather than distalDem because, although historically derived from a demonstrative, it functions synchronically as a 3rd-person pronoun in spoken Korean and lacks the deictic force of a true demonstrative (@cite{kwon-lee-2026} §5).

The full-NP condition uses demonstrative + noun rather than a bare name or definite description, because Korean lacks definite articles.

Equations

• KwonLee2026.KoreanRefForm.nullPro.toAccessibility = Features.AccessibilityLevel.zero
• KwonLee2026.KoreanRefForm.overt.toAccessibility = Features.AccessibilityLevel.unstressedPron
• KwonLee2026.KoreanRefForm.fullNP.toAccessibility = Features.AccessibilityLevel.distalDemNP

@[simp]

theorem KwonLee2026.nullPro_toAccessibility : KoreanRefForm.nullPro.toAccessibility = Features.AccessibilityLevel.zero

@[simp]

theorem KwonLee2026.overt_toAccessibility : KoreanRefForm.overt.toAccessibility = Features.AccessibilityLevel.unstressedPron

@[simp]

theorem KwonLee2026.fullNP_toAccessibility : KoreanRefForm.fullNP.toAccessibility = Features.AccessibilityLevel.distalDemNP

def KwonLee2026.KoreanRefForm.rank (f : KoreanRefForm) : ℕ

The accessibility rank of a Korean form (the rank of its AccessibilityLevel image), used to lift the universal accessibility ordering onto KoreanRefForm.

Equations

• f.rank = f.toAccessibility.rank

@[implicit_reducible]

instance KwonLee2026.instLinearOrderKoreanRefForm : LinearOrder KoreanRefForm

KoreanRefForm inherits a LinearOrder from @cite{ariel-2001}'s accessibility scale via the rank pullback. The induced order is fullNP < overt < nullPro — more accessible forms are larger. This lets every monotonicity claim about Korean forms be expressed as a single StrictMono lemma rather than per-pair inequalities.

Equations

• KwonLee2026.instLinearOrderKoreanRefForm = LinearOrder.lift' KwonLee2026.KoreanRefForm.rank KwonLee2026.instLinearOrderKoreanRefForm._proof_1

theorem KwonLee2026.fullNP_lt_overt : KoreanRefForm.fullNP < KoreanRefForm.overt

The order is fullNP < overt < nullPro (more accessible = larger).

theorem KwonLee2026.overt_lt_nullPro : KoreanRefForm.overt < KoreanRefForm.nullPro

def KwonLee2026.KoreanRefForm.surface : KoreanRefForm → Option String

Bridge to the Korean fragment: the overt form's surface realization is the colloquial pronoun gyae (Yale: kyay) in Fragments.Korean.Pronouns. Derived from the fragment field — not duplicated.

Equations

• KwonLee2026.KoreanRefForm.nullPro.surface = none
• KwonLee2026.KoreanRefForm.overt.surface = some Fragments.Korean.Pronouns.gyae.form
• KwonLee2026.KoreanRefForm.fullNP.surface = some "ku chinkwu"

@[simp]

theorem KwonLee2026.nullPro_surface : KoreanRefForm.nullPro.surface = none

@[simp]

theorem KwonLee2026.overt_surface : KoreanRefForm.overt.surface = some Fragments.Korean.Pronouns.gyae.form

@[simp]

theorem KwonLee2026.fullNP_surface : KoreanRefForm.fullNP.surface = some "ku chinkwu"

theorem KwonLee2026.attenuation_strictMono : StrictMono fun (f : KoreanRefForm) => f.toAccessibility.attenuation

Attenuation (phonological reduction) is strictly increasing in the accessibility order on Korean forms: more accessible forms are more reduced. (Subsumes the previous per-pair attenuation theorems via StrictMono.lt_iff_lt.)

theorem KwonLee2026.informativity_antitone : Antitone fun (f : KoreanRefForm) => f.toAccessibility.informativity

Informativity is antitone in accessibility: more accessible forms are less informative (≤, not <, because @cite{ariel-2001}'s scale collapses distalDemNP and unstressedPron at informativity 1).

structure KwonLee2026.AntecedentChoice : Type

Antecedent-choice rates, from Figure 3 of @cite{kwon-lee-2026}. Globally ambiguous discourse contexts (two same-gender personal names), so neither semantic plausibility nor gender cues disambiguate. Form alone drives interpretation.

• form : KoreanRefForm
• subjectPercent : ℕ

  Percentage choosing the subject antecedent (0–100).

• objectPercent : ℕ

  Percentage choosing the object antecedent (0–100).

@[implicit_reducible]

instance KwonLee2026.instReprAntecedentChoice : Repr AntecedentChoice

Equations

• KwonLee2026.instReprAntecedentChoice = { reprPrec := KwonLee2026.instReprAntecedentChoice.repr }

def KwonLee2026.instReprAntecedentChoice.repr : AntecedentChoice → ℕ → Std.Format

Equations

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

def KwonLee2026.exp3_pro : AntecedentChoice

Exp 3, pro: 70.6% subject, 29.4% object.

Equations

• KwonLee2026.exp3_pro = { form := KwonLee2026.KoreanRefForm.nullPro, subjectPercent := 71, objectPercent := 29 }

def KwonLee2026.exp3_overt : AntecedentChoice

Exp 3, kyay: 42.8% subject, 57.2% object.

Equations

• KwonLee2026.exp3_overt = { form := KwonLee2026.KoreanRefForm.overt, subjectPercent := 43, objectPercent := 57 }

def KwonLee2026.exp3_fullNP : AntecedentChoice

Exp 3, full NP: 35.3% subject, 64.7% object.

Equations

• KwonLee2026.exp3_fullNP = { form := KwonLee2026.KoreanRefForm.fullNP, subjectPercent := 35, objectPercent := 65 }

def KwonLee2026.subjectBias : KoreanRefForm → ℕ

Subject-antecedent bias for each Korean form, derived from the Exp 3 records. Defined as a function so the central monotonicity claim can be expressed as StrictMono.

Equations

• KwonLee2026.subjectBias KwonLee2026.KoreanRefForm.nullPro = KwonLee2026.exp3_pro.subjectPercent
• KwonLee2026.subjectBias KwonLee2026.KoreanRefForm.overt = KwonLee2026.exp3_overt.subjectPercent
• KwonLee2026.subjectBias KwonLee2026.KoreanRefForm.fullNP = KwonLee2026.exp3_fullNP.subjectPercent

def KwonLee2026.objectBias : KoreanRefForm → ℕ

Object-antecedent bias for each Korean form.

Equations

• KwonLee2026.objectBias KwonLee2026.KoreanRefForm.nullPro = KwonLee2026.exp3_pro.objectPercent
• KwonLee2026.objectBias KwonLee2026.KoreanRefForm.overt = KwonLee2026.exp3_overt.objectPercent
• KwonLee2026.objectBias KwonLee2026.KoreanRefForm.fullNP = KwonLee2026.exp3_fullNP.objectPercent

theorem KwonLee2026.exp3_partitions (f : KoreanRefForm) : subjectBias f + objectBias f = 100

The Exp 3 task forces a binary subject/object choice, so for each form the two percentages sum to 100.

theorem KwonLee2026.subjectBias_strictMono : StrictMono subjectBias

Central claim of @cite{kwon-lee-2026}: subject-antecedent bias is strictly monotone in accessibility — more accessible (higher-rank) forms attract subject antecedents more strongly. This single StrictMono lemma subsumes per-pair claims like subjectBias .nullPro > subjectBias .overt (which follow via StrictMono.lt_iff_lt applied to fullNP_lt_overt/overt_lt_nullPro).

Form–function correlation in one line: more accessible form ↔ more accessible antecedent.

theorem KwonLee2026.objectBias_strictAnti : StrictAnti objectBias

Mirror image: object-antecedent bias is antitone in accessibility. Full NPs are the most object-biased; null pronouns the least.

theorem KwonLee2026.three_way_split : Function.Injective subjectBias

Three-way distinction: corollary of subjectBias_strictMono — the three forms have three distinct subject-bias values. Rules out the alternative that Korean has only a binary null/non-null contrast (which @cite{kweon-2011} suggested for the older overt pronoun ku/kunye).

def KwonLee2026.exp3_naturalness : KoreanRefForm → ℚ

Naturalness ratings (Table 5) on the 1–7 Likert scale. The three forms are essentially identical (5.3, 5.3, 5.4; n.s.). When the form is coindexed with its preferred antecedent, all three are equally natural. The accessibility distinction surfaces in interpretation (antecedent choice), not in raw acceptability.

Equations

• KwonLee2026.exp3_naturalness KwonLee2026.KoreanRefForm.nullPro = 53 / 10
• KwonLee2026.exp3_naturalness KwonLee2026.KoreanRefForm.overt = 53 / 10
• KwonLee2026.exp3_naturalness KwonLee2026.KoreanRefForm.fullNP = 54 / 10

theorem KwonLee2026.naturalness_pro_overt_equal : exp3_naturalness KoreanRefForm.nullPro = exp3_naturalness KoreanRefForm.overt

theorem KwonLee2026.naturalness_fullNP_close_to_pro : exp3_naturalness KoreanRefForm.fullNP - exp3_naturalness KoreanRefForm.nullPro ≤ 2 / 10

def KwonLee2026.exp1_naturalness : KoreanRefForm → ℚ

Exp 1 naturalness ratings (Table 1) on the 1–7 Likert scale. With only one available antecedent, the highest-accessibility marker (null pro) is the most natural. The overt pronoun and full NP do not differ significantly (β = 0.19, n.s.).

Equations

• KwonLee2026.exp1_naturalness KwonLee2026.KoreanRefForm.nullPro = 641 / 100
• KwonLee2026.exp1_naturalness KwonLee2026.KoreanRefForm.overt = 618 / 100
• KwonLee2026.exp1_naturalness KwonLee2026.KoreanRefForm.fullNP = 623 / 100

theorem KwonLee2026.exp1_null_most_natural : exp1_naturalness KoreanRefForm.nullPro > exp1_naturalness KoreanRefForm.overt ∧ exp1_naturalness KoreanRefForm.nullPro > exp1_naturalness KoreanRefForm.fullNP

Null is most natural with a single highly-accessible antecedent. Predicted by Accessibility Theory: when only one referent is salient, its mental representation is maximally accessible, so the maximally reduced form is the felicitous choice.

theorem KwonLee2026.exp1_overt_fullNP_close : exp1_naturalness KoreanRefForm.fullNP - exp1_naturalness KoreanRefForm.overt ≤ 1 / 10

The overt-vs-full-NP boundary is gradient in single-antecedent contexts. The two forms do not differ significantly in Exp 1 — the accessibility distinction collapses when only one antecedent is available. @cite{kwon-lee-2026} interpret this as evidence that adjacent markers on the scale need not exhibit categorical distinctions across all contexts (consistent with @cite{ariel-2001}). For the concrete values, full NP is rated slightly higher than overt by less than 0.1 Likert points.

structure KwonLee2026.ComprehensionAccuracy : Type

Exp 2: comprehension accuracy when contextual gender bias points to a particular antecedent. The accuracy gap across contexts is the diagnostic of accessibility sensitivity.

Subject-biased contexts: gender cue points to subject; null pronoun accuracy is near-ceiling (92.9%) because the form-cue (null → subject) aligns with the gender cue.

Object-biased contexts: gender cue points to object, contradicting the form-cue for null. Accuracy drops to 60.3% — null pronouns resist the contextual override. Other forms show no asymmetry.

• form : KoreanRefForm
• subjectBiasedAccuracy : ℕ

  Accuracy in subject-biased context (%).

• objectBiasedAccuracy : ℕ

  Accuracy in object-biased context (%).

def KwonLee2026.instReprComprehensionAccuracy.repr : ComprehensionAccuracy → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance KwonLee2026.instReprComprehensionAccuracy : Repr ComprehensionAccuracy

Equations

• KwonLee2026.instReprComprehensionAccuracy = { reprPrec := KwonLee2026.instReprComprehensionAccuracy.repr }

def KwonLee2026.exp2_pro : ComprehensionAccuracy

Figure 1 of @cite{kwon-lee-2026}.

Equations

• KwonLee2026.exp2_pro = { form := KwonLee2026.KoreanRefForm.nullPro, subjectBiasedAccuracy := 93, objectBiasedAccuracy := 60 }

def KwonLee2026.exp2_overt : ComprehensionAccuracy

Equations

• KwonLee2026.exp2_overt = { form := KwonLee2026.KoreanRefForm.overt, subjectBiasedAccuracy := 81, objectBiasedAccuracy := 78 }

def KwonLee2026.exp2_fullNP : ComprehensionAccuracy

Equations

• KwonLee2026.exp2_fullNP = { form := KwonLee2026.KoreanRefForm.fullNP, subjectBiasedAccuracy := 79, objectBiasedAccuracy := 80 }

def KwonLee2026.ComprehensionAccuracy.contextSensitivity (c : ComprehensionAccuracy) : ℕ

The accuracy gap between subject-biased and object-biased contexts, a measure of how strongly the form's interpretive bias resists the gender-cue override.

Equations

• c.contextSensitivity = max c.subjectBiasedAccuracy c.objectBiasedAccuracy - min c.subjectBiasedAccuracy c.objectBiasedAccuracy

theorem KwonLee2026.exp2_pro_strongly_context_sensitive : exp2_pro.contextSensitivity > 30

Null pronouns drop ~33 accuracy points when the context bias contradicts their default subject-antecedent preference (Figure 1). Direct evidence that null pronouns encode strong subject-antecedent expectations even in the comprehension component.

theorem KwonLee2026.exp2_overt_context_insensitive : exp2_overt.contextSensitivity ≤ 5

Overt pronouns show essentially no asymmetry across context biases.

theorem KwonLee2026.exp2_fullNP_context_insensitive : exp2_fullNP.contextSensitivity ≤ 5

Full NPs show essentially no asymmetry across context biases.

theorem KwonLee2026.exp2_pro_more_sensitive_than_overt : exp2_pro.contextSensitivity > exp2_overt.contextSensitivity

Null is strictly more context-sensitive than overt — exceeding it by over 25 percentage points.

theorem KwonLee2026.exp2_pro_more_sensitive_than_fullNP : exp2_pro.contextSensitivity > exp2_fullNP.contextSensitivity

Null is strictly more context-sensitive than full NP.

structure KwonLee2026.Exp2Naturalness : Type

Naturalness ratings on the 1–7 Likert scale for Exp 2, broken out by context bias. The naturalness data mirrors the comprehension accuracy data: only null pronouns show an asymmetry between subject-biased (4.58) and object-biased (3.94) contexts.

This dual confirmation — same asymmetry in two independent dependent measures (interpretation accuracy AND felicity judgment) — is the paper's strongest evidence that null pronouns carry an interpretive bias that goes beyond mere preference.

• form : KoreanRefForm
• subjectBiased : ℚ

  Naturalness in subject-biased context (1–7 Likert).

• objectBiased : ℚ

  Naturalness in object-biased context (1–7 Likert).

@[implicit_reducible]

instance KwonLee2026.instReprExp2Naturalness : Repr Exp2Naturalness

Equations

• KwonLee2026.instReprExp2Naturalness = { reprPrec := KwonLee2026.instReprExp2Naturalness.repr }

def KwonLee2026.instReprExp2Naturalness.repr : Exp2Naturalness → ℕ → Std.Format

Equations

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

def KwonLee2026.exp2nat_pro : Exp2Naturalness

Figure 2 of @cite{kwon-lee-2026}.

Equations

• KwonLee2026.exp2nat_pro = { form := KwonLee2026.KoreanRefForm.nullPro, subjectBiased := 458 / 100, objectBiased := 394 / 100 }

def KwonLee2026.exp2nat_overt : Exp2Naturalness

Equations

• KwonLee2026.exp2nat_overt = { form := KwonLee2026.KoreanRefForm.overt, subjectBiased := 462 / 100, objectBiased := 442 / 100 }

def KwonLee2026.exp2nat_fullNP : Exp2Naturalness

Equations

• KwonLee2026.exp2nat_fullNP = { form := KwonLee2026.KoreanRefForm.fullNP, subjectBiased := 433 / 100, objectBiased := 456 / 100 }

def KwonLee2026.Exp2Naturalness.contextSensitivity (n : Exp2Naturalness) : ℚ

Equations

• n.contextSensitivity = max n.subjectBiased n.objectBiased - min n.subjectBiased n.objectBiased

theorem KwonLee2026.exp2_naturalness_pro_strongly_asymmetric : exp2nat_pro.contextSensitivity > 1 / 2

Naturalness mirrors comprehension: only the null pronoun shows a large naturalness asymmetry across context biases (>0.50 Likert points, β = −1.06, p = .028 in the paper). The overt and full NP forms show no significant asymmetry.

theorem KwonLee2026.exp2_naturalness_overt_close : exp2nat_overt.contextSensitivity ≤ 1 / 4

theorem KwonLee2026.exp2_naturalness_fullNP_close : exp2nat_fullNP.contextSensitivity ≤ 1 / 4

theorem KwonLee2026.exp2_dual_measures_converge_accuracy : exp2_pro.contextSensitivity > exp2_overt.contextSensitivity

The two Exp 2 dependent measures (accuracy and naturalness) agree on the same asymmetry pattern: null is the only form whose felicity drops when context conflicts with its interpretive bias. This converging evidence is the cornerstone of the paper's argument.

theorem KwonLee2026.exp2_dual_measures_converge_naturalness : exp2nat_pro.contextSensitivity > exp2nat_overt.contextSensitivity

@[reducible, inline]

abbrev KwonLee2026.correctTrial_naturalness : ℚ

Naturalness ratings cross-tabulated with comprehension correctness (paper §3.2.2, p. 16): trials where participants chose the intended antecedent received higher naturalness ratings (M = 4.40) than trials where they chose the unintended antecedent (M = 4.05). Effect: β = 0.38, SE = 0.13, z = 3.05, p = .002.

This is the paper's most direct evidence that the form-function correlation is psychologically real (not just an experimental artifact): listeners who heard a form and computed an antecedent that didn't match the speaker's intent also perceived the sentence as less natural. The two measures co-vary at the trial level.

Equations

• KwonLee2026.correctTrial_naturalness = 440 / 100

@[reducible, inline]

abbrev KwonLee2026.incorrectTrial_naturalness : ℚ

Equations

• KwonLee2026.incorrectTrial_naturalness = 405 / 100

theorem KwonLee2026.correct_trials_more_natural : correctTrial_naturalness > incorrectTrial_naturalness

Form-function correlation is psychologically real: when the listener's chosen antecedent matches the speaker's intent (correct trial), the sentence is rated more natural than when it doesn't. This validates the form-function link as more than an experimental artifact — it tracks the listener's online interpretive process.

theorem KwonLee2026.naturalness_accuracy_gap_substantial : correctTrial_naturalness - incorrectTrial_naturalness ≥ 3 / 10

The gap is non-trivial (≈ 0.35 Likert points), within the range where the paper reports significance (β = 0.38).

structure KwonLee2026.CrossLingProfile : Type

A language's calibration of @cite{ariel-2001}'s accessibility scale: the empirical subject-antecedent bias of each referential form in a globally ambiguous two-antecedent context.

This is the structure that lets us compare how different languages instantiate the same universal ordering. The relative ordering (null > overt > [full NP]) is preserved, but the spread varies.

• language : String
• nullSubjectPercent : ℕ

  P(subject antecedent | null pronoun), as a percentage 0–100.

• overtSubjectPercent : Option ℕ

  P(subject antecedent | overt pronoun). none if the language was not tested with overt pronouns or has no overt 3sg pronoun.

• fullNPSubjectPercent : Option ℕ

  P(subject antecedent | full NP). none if not tested.

def KwonLee2026.instReprCrossLingProfile.repr : CrossLingProfile → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance KwonLee2026.instReprCrossLingProfile : Repr CrossLingProfile

Equations

• KwonLee2026.instReprCrossLingProfile = { reprPrec := KwonLee2026.instReprCrossLingProfile.repr }

def KwonLee2026.italian : CrossLingProfile

Italian, @cite{carminati-2002}: null = 80.72%, overt = 100% − 83.33% = 16.67%. The cleanest division of labor of any language tested (Position of Antecedent Hypothesis).

Equations

• KwonLee2026.italian = { language := "Italian", nullSubjectPercent := 81, overtSubjectPercent := some 17, fullNPSubjectPercent := none }

def KwonLee2026.spanish : CrossLingProfile

Spanish, @cite{contemori-di-domenico-2021}: null = 62%, overt = 100% − 58% = 42%. Weaker division of labor than Italian.

Equations

• KwonLee2026.spanish = { language := "Spanish", nullSubjectPercent := 62, overtSubjectPercent := some 42, fullNPSubjectPercent := none }

def KwonLee2026.chinese : CrossLingProfile

Chinese, @cite{zhang-kwon-2022}: null = 84%, overt = 65.3%. Both pronoun types show subject bias; the overt form does not flip to object bias as in Italian.

Equations

• KwonLee2026.chinese = { language := "Chinese", nullSubjectPercent := 84, overtSubjectPercent := some 65, fullNPSubjectPercent := none }

def KwonLee2026.korean : CrossLingProfile

Korean (this paper's Exp 3, overt = colloquial kyay). The first cross-linguistic dataset that includes full NPs alongside null and overt pronouns.

Equations

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

def KwonLee2026.korean_kweon : CrossLingProfile

Korean (@cite{kweon-2011}, overt = literary ku/kunye). 12-item questionnaire study; null = 81.1%, overt = 31.4% subject (so 68.6% object). Resembles Italian's clean division of labor — Kweon interpreted this as supporting Carminati's PAH.

Equations

• KwonLee2026.korean_kweon = { language := "Korean (Kweon 2011, ku/kunye)", nullSubjectPercent := 81, overtSubjectPercent := some 31, fullNPSubjectPercent := none }

def KwonLee2026.korean_choe : CrossLingProfile

Korean (@cite{choe-2021}, overt = literary ku/kunye). 40-target / 24-filler study; null = 91%, overt = 73% subject. Both forms subject-biased; little division of labor. Diverges sharply from Kweon. The paper attributes the discrepancy to methodological differences (filler ratio, ambiguity verification).

Equations

• KwonLee2026.korean_choe = { language := "Korean (Choe 2021, ku/kunye)", nullSubjectPercent := 91, overtSubjectPercent := some 73, fullNPSubjectPercent := none }

def KwonLee2026.allProfiles : List CrossLingProfile

Equations

• KwonLee2026.allProfiles = [KwonLee2026.italian, KwonLee2026.spanish, KwonLee2026.chinese, KwonLee2026.korean, KwonLee2026.korean_kweon, KwonLee2026.korean_choe]

def KwonLee2026.koreanProfiles : List CrossLingProfile

All Korean profiles.

Equations

• KwonLee2026.koreanProfiles = [KwonLee2026.korean, KwonLee2026.korean_kweon, KwonLee2026.korean_choe]

theorem KwonLee2026.null_dominates_overt_universally (p : CrossLingProfile) : p ∈ allProfiles → ∀ (o : ℕ), p.overtSubjectPercent = some o → p.nullSubjectPercent ≥ o

Universal ordering preserved: in every language tested, null pronouns are at least as subject-biased as overt pronouns. This is the universal claim of @cite{ariel-2001}: the relative ordering holds even when the magnitudes vary.

def KwonLee2026.CrossLingProfile.nullOvertSpread (p : CrossLingProfile) : ℕ

Cross-linguistic granularity varies: Italian shows ≥60-point spread between null and overt; Spanish 20; Chinese 19; Korean 28. The same theory accounts for all four, with language-specific calibration of the spread.

Equations

• p.nullOvertSpread = match p.overtSubjectPercent with | some o => p.nullSubjectPercent - o | none => 0

theorem KwonLee2026.italian_widest_spread : italian.nullOvertSpread > spanish.nullOvertSpread ∧ italian.nullOvertSpread > chinese.nullOvertSpread ∧ italian.nullOvertSpread > korean.nullOvertSpread

Korean is the only language tested with full NPs: a unique methodological contribution of @cite{kwon-lee-2026}. The full-NP bias (35% subject ↔ 65% object) extends Accessibility Theory's test set to a wider range of forms than prior cross-linguistic work.

theorem KwonLee2026.korean_includes_fullNP : korean.fullNPSubjectPercent.isSome = true

theorem KwonLee2026.italian_omits_fullNP : italian.fullNPSubjectPercent.isNone = true

theorem KwonLee2026.spanish_omits_fullNP : spanish.fullNPSubjectPercent.isNone = true

theorem KwonLee2026.chinese_omits_fullNP : chinese.fullNPSubjectPercent.isNone = true

theorem KwonLee2026.all_korean_null_subject_biased (p : CrossLingProfile) : p ∈ koreanProfiles → p.nullSubjectPercent > 50

Robust within-Korean finding: every Korean study agrees that null pronouns are subject-biased. The variation is entirely in the strength of the bias (and in the overt-pronoun behavior).

The Kweon vs Choe disagreement is one of the paper's framing motivations. Kweon (small item set) shows clean object-bias for overt (~31% subject); Choe (unusually low filler ratio) shows subject-bias (73%). These cannot both be representative of the same underlying competence. The paper attributes the gap to methodological factors.

theorem KwonLee2026.kweon_overt_subject_31 : korean_kweon.overtSubjectPercent = some 31

theorem KwonLee2026.choe_overt_subject_73 : korean_choe.overtSubjectPercent = some 73

theorem KwonLee2026.kweon_choe_gap_large : 73 - 31 > 40

The Kweon-Choe gap exceeds 40 percentage points.

theorem KwonLee2026.kwonlee_overt_subject_43 : korean.overtSubjectPercent = some 43

@cite{kwon-lee-2026}'s Exp 3 finding (43% subject for kyay) lies between Kweon (31%) and Choe (73%). The paper takes this as suggesting Kweon was directionally correct (overt is object-biased in Korean) but that the magnitude depends on the form: kyay is less rigidly object-biased than ku/kunye, consistent with kyay's higher position on the accessibility scale (closer to null).

theorem KwonLee2026.korean_relative_ordering_invariant (p : CrossLingProfile) : p ∈ koreanProfiles → ∀ (o : ℕ), p.overtSubjectPercent = some o → p.nullSubjectPercent > o

The relative ordering (null > overt) holds for every Korean study, despite the disagreement on magnitudes. This is exactly @cite{ariel-2001}'s universal: the ordering is invariant; the spread is methodologically/contextually labile.

def KwonLee2026.KoreanRefForm.accessibilityDistance (a b : KoreanRefForm) : ℕ

Distance between two forms on @cite{ariel-2001}'s accessibility scale, measured as the absolute difference of their ranks. Larger distance = further apart on the universal ordering.

Equations

• a.accessibilityDistance b = max a.toAccessibility.rank b.toAccessibility.rank - min a.toAccessibility.rank b.toAccessibility.rank

def KwonLee2026.biasSpread (a b : AntecedentChoice) : ℕ

Subject-bias spread between two forms in Exp 3 (absolute difference of subject-choice percentages). Larger spread = stronger empirical distinction between the two forms.

Equations

• KwonLee2026.biasSpread a b = max a.subjectPercent b.subjectPercent - min a.subjectPercent b.subjectPercent

theorem KwonLee2026.accessibilityDistance_pro_fullNP_max_vs_pro_overt : KoreanRefForm.nullPro.accessibilityDistance KoreanRefForm.fullNP > KoreanRefForm.nullPro.accessibilityDistance KoreanRefForm.overt

Triangle-inequality-like prediction: the extreme pair (null vs full NP) has the largest accessibility distance and the largest empirical bias spread. This is a derived prediction of @cite{ariel-2001}'s ordinal scale — it follows from the rank ordering of the three forms, not from any data-fitting. The four sub-theorems below state each pairwise comparison separately.

theorem KwonLee2026.accessibilityDistance_pro_fullNP_max_vs_overt_fullNP : KoreanRefForm.nullPro.accessibilityDistance KoreanRefForm.fullNP > KoreanRefForm.overt.accessibilityDistance KoreanRefForm.fullNP

theorem KwonLee2026.biasSpread_pro_fullNP_max_vs_pro_overt : biasSpread exp3_pro exp3_fullNP > biasSpread exp3_pro exp3_overt

theorem KwonLee2026.biasSpread_pro_fullNP_max_vs_overt_fullNP : biasSpread exp3_pro exp3_fullNP > biasSpread exp3_overt exp3_fullNP

Non-uniform calibration — the paper's deepest empirical finding (Discussion): the null↔overt step (3 ranks → 28-point bias spread) is much steeper than the overt↔full-NP step (6 ranks → 8-point spread). Korean's accessibility scale has a steep cliff at the null/non-null boundary and a shallow slope among non-null forms. Exactly what @cite{ariel-2001} predicts (§4.2) about language-specific calibration: only the ordering is universal, not the magnitudes.

theorem KwonLee2026.null_overt_distance_lt_overt_fullNP_distance : KoreanRefForm.nullPro.accessibilityDistance KoreanRefForm.overt < KoreanRefForm.overt.accessibilityDistance KoreanRefForm.fullNP

The accessibility-distance step from null to overt (3 ranks) is smaller than from overt to full NP (6 ranks).

theorem KwonLee2026.null_overt_spread_gt_overt_fullNP_spread : biasSpread exp3_pro exp3_overt > biasSpread exp3_overt exp3_fullNP

Yet the empirical bias spread shows the opposite pattern: the smaller-distance pair (null↔overt) has the larger bias spread. The scale is calibrated non-uniformly in Korean.

theorem KwonLee2026.null_overt_spread_large : biasSpread exp3_pro exp3_overt > 25

The null↔overt spread is large (>25 points) — the "cliff" at the null/non-null boundary.

theorem KwonLee2026.overt_fullNP_spread_small : biasSpread exp3_overt exp3_fullNP < 15

The overt↔fullNP spread is small (<15 points) — the "shallow slope" among non-null forms.

def KwonLee2026.koreanSubjectTopichood : KehlerRohde2013.TopichoodLevel

@cite{kehler-rohde-2013} decompose pronoun interpretation as:

P(referent | pronoun) ∝ P(pronoun | referent) × P(referent)

The production component P(pronoun | referent) is conditioned by topichood — speakers use reduced forms for topical referents. The Korean data slot directly into this framework: the canonical Korean topic position is the (typically subject-marked) sentence-initial position, so subjects have high topichood and license null forms.

The cross-linguistic variation in spread (§ 5) reflects how strongly each language's null form encodes topichood relative to other forms.

Equations

• KwonLee2026.koreanSubjectTopichood = KehlerRohde2013.topichood UD.Voice.Act true

theorem KwonLee2026.subject_default_topichood : koreanSubjectTopichood = KehlerRohde2013.TopichoodLevel.default_

Korean subjects are the default topichood level (subject of an active clause). Null pronouns mark high accessibility, which @cite{kehler-rohde-2013} derive from high topichood.

inductive KwonLee2026.SyntacticPosition : Type

Carminati's Position of Antecedent Hypothesis (@cite{carminati-2002}): null pronouns prefer antecedents in syntactically prominent positions (canonically Spec-IP, the preverbal subject position); overt pronouns prefer non-prominent positions.

PAH is a structural theory: prominence is determined by syntactic position, not by discourse accessibility. This contrasts with Accessibility Theory's cognitive/discourse-based prominence. In configurational SVO languages where subject = Spec-IP, the two theories make identical predictions; they diverge in topic-prominent languages where the topic position is structurally distinct from Spec-IP.

@cite{kwon-lee-2026} fn. 1 takes the position that PAH and AT are compatible — PAH being a structural special case that happens to coincide with AT in canonical configurations.

• specIP : SyntacticPosition

  Spec-IP: preverbal subject position. PAH's "prominent" position.

• lowerIP : SyntacticPosition

  Below Spec-IP: object, complement, adjunct positions.

@[implicit_reducible]

instance KwonLee2026.instDecidableEqSyntacticPosition : DecidableEq SyntacticPosition

Equations

• KwonLee2026.instDecidableEqSyntacticPosition x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def KwonLee2026.instReprSyntacticPosition.repr : SyntacticPosition → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance KwonLee2026.instReprSyntacticPosition : Repr SyntacticPosition

Equations

• KwonLee2026.instReprSyntacticPosition = { reprPrec := KwonLee2026.instReprSyntacticPosition.repr }

@[implicit_reducible]

instance KwonLee2026.instBEqSyntacticPosition : BEq SyntacticPosition

Equations

• KwonLee2026.instBEqSyntacticPosition = { beq := KwonLee2026.instBEqSyntacticPosition.beq }

def KwonLee2026.instBEqSyntacticPosition.beq : SyntacticPosition → SyntacticPosition → Bool

Equations

• KwonLee2026.instBEqSyntacticPosition.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def KwonLee2026.KoreanRefForm.pahPosition : KoreanRefForm → Option SyntacticPosition

The PAH-predicted antecedent position for each Korean form. Null prefers Spec-IP; overt avoids it (overt → non-Spec-IP). The PAH does not directly address full NPs (it was formulated for the null/overt pronoun contrast in Italian).

Equations

• KwonLee2026.KoreanRefForm.nullPro.pahPosition = some KwonLee2026.SyntacticPosition.specIP
• KwonLee2026.KoreanRefForm.overt.pahPosition = some KwonLee2026.SyntacticPosition.lowerIP
• KwonLee2026.KoreanRefForm.fullNP.pahPosition = none

@[simp]

theorem KwonLee2026.nullPro_pahPosition : KoreanRefForm.nullPro.pahPosition = some SyntacticPosition.specIP

@[simp]

theorem KwonLee2026.overt_pahPosition : KoreanRefForm.overt.pahPosition = some SyntacticPosition.lowerIP

@[simp]

theorem KwonLee2026.fullNP_pahPosition : KoreanRefForm.fullNP.pahPosition = none

theorem KwonLee2026.pah_at_converge_for_canonical_korean : KoreanRefForm.nullPro.pahPosition = some SyntacticPosition.specIP

Convergence theorem: PAH and AT make the same prediction for null pronouns in canonical Korean SVO — both predict the subject antecedent (subject = Spec-IP in the experimental stimuli). This is why @cite{kwon-lee-2026}'s Exp 3 data cannot distinguish the two theories.

theorem KwonLee2026.pah_at_diverge_in_topic_fronting : KoreanRefForm.nullPro.pahPosition = some SyntacticPosition.specIP

Divergence point: in a topic-prominent configuration (e.g., a sentence with a topicalized object in sentence-initial position), the topic is NOT in Spec-IP. PAH would still predict null → Spec-IP (= the in-situ subject), while AT would predict null → topic (= the most-accessible referent regardless of structural position).

The Korean experiments cannot test this because all stimuli used canonical SVO order. Disambiguating PAH from AT requires testing topicalization configurations — an empirical extension explicitly flagged by @cite{kwon-lee-2026} (Discussion).

theorem KwonLee2026.pah_silent_on_fullNP : KoreanRefForm.fullNP.pahPosition = none

PAH does not address full NPs — it was formulated for pronouns only. AT, by contrast, places full NPs at the bottom of the accessibility scale and predicts the inverse bias (object antecedent). The Exp 3 full-NP finding (35% subject ↔ 65% object) is therefore predicted by AT alone, not by PAH. The paper's inclusion of full NPs is what lets the data adjudicate between the two theories.

def KwonLee2026.exp1_assessment : Phenomena.Reference.Studies.Ariel2001.AccessibilityAssessment

Exp 1: a single antecedent in same-clause topic position. Maximally accessible — no competition, tight unity, recently mentioned, topical. Predicts the form should not need to disambiguate.

Equations

• KwonLee2026.exp1_assessment = { distance := 0, topicality := 2, competition := 0, unity := 2 }

def KwonLee2026.exp2_3_assessment : Phenomena.Reference.Studies.Ariel2001.AccessibilityAssessment

Exp 2 & 3: two antecedents in same clause. Competition = 1 (one additional candidate). The two experiments differ in whether additional cues (gender in Exp 2) disambiguate, but the accessibility-theoretic competition level is identical.

@cite{ariel-2001}'s AccessibilityAssessment does not have a field for "disambiguating cue", which is the gap that the Exp 2 naturalness × accuracy correlation (§ 4c) helps fill.

Equations

• KwonLee2026.exp2_3_assessment = { distance := 0, topicality := 2, competition := 1, unity := 2 }

theorem KwonLee2026.exp_distance_constant : exp1_assessment.distance = exp2_3_assessment.distance

Distance is held constant across experiments.

theorem KwonLee2026.exp_topicality_constant : exp1_assessment.topicality = exp2_3_assessment.topicality

Topicality is held constant.

theorem KwonLee2026.exp_unity_constant : exp1_assessment.unity = exp2_3_assessment.unity

Unity is held constant.

theorem KwonLee2026.exp_competition_increases : exp1_assessment.competition < exp2_3_assessment.competition

The manipulation isolates competition: across the three experiments, only the competition field varies; distance, topicality, and unity are held constant. This makes the experimental design a clean test of how competition affects form-function visibility.

theorem KwonLee2026.exp1_more_accessible_than_exp23 : exp1_assessment.score > exp2_3_assessment.score

Exp 1 has higher accessibility than Exp 2/3 — the referent is more accessible when there's no competition.

theorem KwonLee2026.form_bias_emerges_under_competition : exp1_naturalness KoreanRefForm.fullNP - exp1_naturalness KoreanRefForm.overt ≤ 1 / 10 ∧ biasSpread exp3_overt exp3_fullNP > 0

Empirical asymmetry consistent with the theory: in the high-accessibility Exp 1 setting (one antecedent), the form-function distinction collapses (exp1_overt_fullNP_close). In the lower-accessibility Exp 3 setting (competition), the distinction emerges as a clean three-way split (accessibility_predicts_subject_bias).

This is captured by the assessment-score difference: form-bias strength is inversely correlated with the per-referent accessibility score, because forms only need to disambiguate when there is ambiguity to resolve.

@cite{ariel-2001}'s three form-function criteria all line up with accessibility for the Korean forms. The criteria don't perfectly pull apart at every adjacent level (informativity collapses distalDemNP and unstressedPron at 1), but the overall pattern holds: the more accessible form is less informative, less rigid, and more attenuated.

theorem KwonLee2026.korean_informativity_fullNP_ge_overt : KoreanRefForm.fullNP.toAccessibility.informativity ≥ KoreanRefForm.overt.toAccessibility.informativity

Informativity: full NP ≥ overt (≥ because Ariel's coarse scale collapses distalDemNP and unstressedPron).

theorem KwonLee2026.korean_informativity_overt_gt_null : KoreanRefForm.overt.toAccessibility.informativity > KoreanRefForm.nullPro.toAccessibility.informativity

Informativity: overt > null.

theorem KwonLee2026.korean_rigidity_fullNP_ge_overt : KoreanRefForm.fullNP.toAccessibility.rigidity ≥ KoreanRefForm.overt.toAccessibility.rigidity

Rigidity: full NP (demonstrative + noun) ≥ overt.

theorem KwonLee2026.korean_attenuation_null_gt_overt : KoreanRefForm.nullPro.toAccessibility.attenuation > KoreanRefForm.overt.toAccessibility.attenuation

Attenuation: null > overt — the null pronoun has no phonological exponent, the overt pronoun has one syllable.

theorem KwonLee2026.korean_attenuation_overt_gt_fullNP : KoreanRefForm.overt.toAccessibility.attenuation > KoreanRefForm.fullNP.toAccessibility.attenuation

Attenuation: overt > full NP — the demonstrative + noun form has more phonological material than a single pronoun.