Cartner, Kogan, Webster, Wagers & Sichel (2026)

@cite{cartner-et-al-2026}

Subject islands do not reduce to construction-specific discourse function. Cognition 271, 106467.

Core Result

Three acceptability judgment experiments test whether subject islands arise from an information-structural clash (the Focus Background Constraint of @cite{abeille-et-al-2020}) or from an abstract syntactic constraint on movement. Using a super-additive factorial design (@cite{sprouse-2007}, @cite{sprouse-et-al-2012}), the paper isolates subject island effects across wh-questions, relative clauses, and topicalization — three constructions that share the filler-gap mechanism but differ in the IS profile of the filler.

Finding: Subject island effects are present in all three constructions, with remarkably invariant magnitude. This falsifies the FBC (and its revised formulation in @cite{winckel-et-al-2025}), which predict island effects only for wh-questions. The paper explicitly notes (§8) that the results do NOT falsify direct backgroundedness approaches (@cite{cuneo-goldberg-2023}), only the constructional IS profile account.

Formalization

1. IS profiles per construction, with structural uniformity/variance theorems
2. Original FBC (@cite{abeille-et-al-2020}) and revised FBC (@cite{winckel-et-al-2025}) as predicates over IS profiles
3. Both FBCs' predictions derived, then falsified by experimental DD scores
4. Explicit distinction from direct backgroundedness (BCI), which is NOT falsified (connecting to BackgroundedIslands.lean)
5. Cross-constructional invariance of the island effect
6. Bridge: subject islands have syntactic source
7. End-to-end argument chain

inductive FGDConstruction : Type

The three canonical filler-gap dependency constructions in English. Each shares the abstract mechanism of movement (a filler displaced from a gap) but differs in information-structural profile (@cite{abeille-et-al-2020}).

The distinction matters for testing whether island effects are construction-specific (as @cite{abeille-et-al-2020} claim) or construction-general (as @cite{cartner-et-al-2026} argue).

• whQuestion : FGDConstruction
• relativeClause : FGDConstruction
• topicalization : FGDConstruction

@[implicit_reducible]

instance instDecidableEqFGDConstruction : DecidableEq FGDConstruction

Equations

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

@[implicit_reducible]

instance instReprFGDConstruction : Repr FGDConstruction

Equations

• instReprFGDConstruction = { reprPrec := instReprFGDConstruction.repr }

def instReprFGDConstruction.repr : FGDConstruction → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• instReprFGDConstruction.repr FGDConstruction.whQuestion prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "FGDConstruction.whQuestion")).group prec✝

inductive ExtractionPosition : Type

Extraction position within the embedded clause. The subject/object asymmetry is the core empirical target of subject island research (@cite{ross-1967}, @cite{chomsky-1973}).

• subject : ExtractionPosition
• object : ExtractionPosition

@[implicit_reducible]

instance instDecidableEqExtractionPosition : DecidableEq ExtractionPosition

Equations

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

def instReprExtractionPosition.repr : ExtractionPosition → ℕ → Std.Format

Equations

• instReprExtractionPosition.repr ExtractionPosition.subject prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "ExtractionPosition.subject")).group prec✝
• instReprExtractionPosition.repr ExtractionPosition.object prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "ExtractionPosition.object")).group prec✝

@[implicit_reducible]

instance instReprExtractionPosition : Repr ExtractionPosition

Equations

• instReprExtractionPosition = { reprPrec := instReprExtractionPosition.repr }

Each filler-gap construction assigns distinct IS roles to its filler (the displaced element) and its extraction domain. These profiles determine whether the FBC predicts an IS clash.

The Krifka decomposition forces these into TWO axes: filler focus marking (a focus-axis fact) and domain givenness (a givenness-axis fact). WHQ fillers are focused (at-issue, introducing new information); RC and TOP fillers are not (RC heads are presupposed, topics are discourse-old). All three subjects are given/backgrounded. Pre-Krifka versions of this file collapsed both into one DiscourseStatus → DiscourseStatus map and had to filter the .focused case for the domain.

def CartnerEtAl2026.fillerFocus : FGDConstruction → Features.InformationStructure.FocusMark

Focus marking of the filler in each construction. @cite{abeille-et-al-2020}, §2; @cite{winckel-et-al-2025}.

Equations

• CartnerEtAl2026.fillerFocus FGDConstruction.whQuestion = Features.InformationStructure.FocusMark.focused
• CartnerEtAl2026.fillerFocus FGDConstruction.relativeClause = Features.InformationStructure.FocusMark.nonFocused
• CartnerEtAl2026.fillerFocus FGDConstruction.topicalization = Features.InformationStructure.FocusMark.nonFocused

def CartnerEtAl2026.subjectGivenness : FGDConstruction → Features.BinaryGivenness

Givenness of the extraction domain (subject position). Subjects are typically given/backgrounded across all three constructions.

Equations

• CartnerEtAl2026.subjectGivenness FGDConstruction.whQuestion = Features.BinaryGivenness.given
• CartnerEtAl2026.subjectGivenness FGDConstruction.relativeClause = Features.BinaryGivenness.given
• CartnerEtAl2026.subjectGivenness FGDConstruction.topicalization = Features.BinaryGivenness.given

theorem CartnerEtAl2026.subjectGivenness_uniform : subjectGivenness FGDConstruction.whQuestion = subjectGivenness FGDConstruction.relativeClause ∧ subjectGivenness FGDConstruction.relativeClause = subjectGivenness FGDConstruction.topicalization

Subjects have uniform givenness across all constructions. This uniformity is what makes the cross-constructional comparison informative: the extraction domain is held constant while the filler's focus marking varies.

theorem CartnerEtAl2026.fillerFocus_varies : fillerFocus FGDConstruction.whQuestion ≠ fillerFocus FGDConstruction.relativeClause ∧ fillerFocus FGDConstruction.whQuestion ≠ fillerFocus FGDConstruction.topicalization

Fillers differ in focus marking across constructions. WHQ fillers are focused; RC and TOP fillers are not. This is the variable that the FBC claims should modulate island effects.

def CartnerEtAl2026.fbcPredictsIsland (c : FGDConstruction) : Prop

The FBC (constraint (8) of @cite{abeille-et-al-2020}):

"A focused element should not be part of a backgrounded constituent."

A violation occurs when a focused filler is extracted from a backgrounded domain. This is exactly extractionISClash from Core/InformationStructure.lean, which unifies this constraint with @cite{erteschik-shir-1973}'s Dominance Condition on Extraction.

Equations

• CartnerEtAl2026.fbcPredictsIsland c = Semantics.Focus.Comparability.extractionISClash (CartnerEtAl2026.fillerFocus c) (CartnerEtAl2026.subjectGivenness c)

@[implicit_reducible]

instance CartnerEtAl2026.instDecidableFbcPredictsIsland (c : FGDConstruction) : Decidable (fbcPredictsIsland c)

Equations

• CartnerEtAl2026.instDecidableFbcPredictsIsland c = CartnerEtAl2026.instDecidableFbcPredictsIsland._aux_1 c

def CartnerEtAl2026.subjectFocus : FGDConstruction → Features.InformationStructure.FocusMark

Focus marking of the subject (governor) in each construction. Across all three constructions in @cite{cartner-et-al-2026}'s materials, subjects are non-focused — the experimental design holds the governor's focus marking constant while varying the filler's.

Equations

• CartnerEtAl2026.subjectFocus FGDConstruction.whQuestion = Features.InformationStructure.FocusMark.nonFocused
• CartnerEtAl2026.subjectFocus FGDConstruction.relativeClause = Features.InformationStructure.FocusMark.nonFocused
• CartnerEtAl2026.subjectFocus FGDConstruction.topicalization = Features.InformationStructure.FocusMark.nonFocused

def CartnerEtAl2026.fbcRevisedViolation (filler governor : Features.InformationStructure.FocusMark) : Prop

The revised FBC (formulation (11) of @cite{winckel-et-al-2025}):

"An extracted element should not be more focused than its (non-local)
governor."

@cite{winckel-et-al-2025} state this as gradient (greater focus difference → more degraded dependency), but in @cite{cartner-et-al-2026}'s materials both filler and governor are coded as binary focus marks (FocusMark), so the gradient version reduces to: filler is focused AND governor is not. Modelling the gradient case requires a richer focus-prominence type than the binary FocusMark; deferred.

Equations

• CartnerEtAl2026.fbcRevisedViolation filler governor = (filler = Features.InformationStructure.FocusMark.focused ∧ governor = Features.InformationStructure.FocusMark.nonFocused)

@[implicit_reducible]

instance CartnerEtAl2026.instDecidableFbcRevisedViolation (a b : Features.InformationStructure.FocusMark) : Decidable (fbcRevisedViolation a b)

Equations

• CartnerEtAl2026.instDecidableFbcRevisedViolation a b = CartnerEtAl2026.instDecidableFbcRevisedViolation._aux_1 a b

def CartnerEtAl2026.fbcRevisedPredictsIsland (c : FGDConstruction) : Prop

Revised FBC predicts a subject island effect for a given construction iff the filler is more focused than the subject governor.

Equations

• CartnerEtAl2026.fbcRevisedPredictsIsland c = CartnerEtAl2026.fbcRevisedViolation (CartnerEtAl2026.fillerFocus c) (CartnerEtAl2026.subjectFocus c)

@[implicit_reducible]

instance CartnerEtAl2026.instDecidableFbcRevisedPredictsIsland (c : FGDConstruction) : Decidable (fbcRevisedPredictsIsland c)

Equations

• CartnerEtAl2026.instDecidableFbcRevisedPredictsIsland c = CartnerEtAl2026.instDecidableFbcRevisedPredictsIsland._aux_1 c

theorem CartnerEtAl2026.fbc_predicts_whq_island : fbcPredictsIsland FGDConstruction.whQuestion

The FBC predicts a subject island effect for wh-questions: the wh-phrase is focused, the subject is backgrounded → clash.

theorem CartnerEtAl2026.fbc_predicts_no_rc_island : ¬fbcPredictsIsland FGDConstruction.relativeClause

The FBC predicts NO subject island effect for relative clauses.

theorem CartnerEtAl2026.fbc_predicts_no_top_island : ¬fbcPredictsIsland FGDConstruction.topicalization

The FBC predicts NO subject island effect for topicalization.

theorem CartnerEtAl2026.both_fbcs_same_predictions : (fbcPredictsIsland FGDConstruction.whQuestion ↔ fbcRevisedPredictsIsland FGDConstruction.whQuestion) ∧ (fbcPredictsIsland FGDConstruction.relativeClause ↔ fbcRevisedPredictsIsland FGDConstruction.relativeClause) ∧ (fbcPredictsIsland FGDConstruction.topicalization ↔ fbcRevisedPredictsIsland FGDConstruction.topicalization)

The revised FBC makes the same predictions as the original.

theorem CartnerEtAl2026.fbc_predicts_construction_dependence : fbcPredictsIsland FGDConstruction.whQuestion ∧ ¬fbcPredictsIsland FGDConstruction.relativeClause ∧ ¬fbcPredictsIsland FGDConstruction.topicalization

Both FBCs predict construction-dependent island effects: only WHQs should show subject islands.

structure CartnerEtAl2026.DDScore : Type

A super-additive DD (Differences-in-Differences) score. Isolates the island effect by factoring out independent costs of DP complexity and extraction. DD > 0 indicates a super-additive penalty — the hallmark of an island effect.

Scores are z-scored by participant, rounded to ×100 integer encoding.

• construction : FGDConstruction
• position : ExtractionPosition
• dd : ℤ

  DD score × 100 (z-scored). Positive = super-additive penalty.

• citation : String

def CartnerEtAl2026.instReprDDScore.repr : DDScore → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance CartnerEtAl2026.instReprDDScore : Repr DDScore

Equations

• CartnerEtAl2026.instReprDDScore = { reprPrec := CartnerEtAl2026.instReprDDScore.repr }

def CartnerEtAl2026.whqSubjectDD : DDScore

Experiment 1: Wh-questions (Fig. 1, n = 72). Three-way interaction β = −0.94, 95%CrI = (−1.54, −0.32), Pr(β < 0) = 0.99.

Equations

• CartnerEtAl2026.whqSubjectDD = { construction := FGDConstruction.whQuestion, position := ExtractionPosition.subject, dd := 80, citation := "Cartner et al. 2026, Exp 1, Fig. 1" }

def CartnerEtAl2026.whqObjectDD : DDScore

Equations

• CartnerEtAl2026.whqObjectDD = { construction := FGDConstruction.whQuestion, position := ExtractionPosition.object, dd := 33, citation := "Cartner et al. 2026, Exp 1, Fig. 1" }

def CartnerEtAl2026.rcSubjectDD : DDScore

Experiment 2: Relative clauses (Fig. 2, n = 72). Three-way interaction β = −0.58, 95%CrI = (−1.17, 0), Pr(β < 0) = 0.98.

Equations

• CartnerEtAl2026.rcSubjectDD = { construction := FGDConstruction.relativeClause, position := ExtractionPosition.subject, dd := 50, citation := "Cartner et al. 2026, Exp 2, Fig. 2" }

def CartnerEtAl2026.rcObjectDD : DDScore

Equations

• CartnerEtAl2026.rcObjectDD = { construction := FGDConstruction.relativeClause, position := ExtractionPosition.object, dd := 16, citation := "Cartner et al. 2026, Exp 2, Fig. 2" }

def CartnerEtAl2026.topSubjectDD : DDScore

Experiment 3: Topicalization (Fig. 3, n = 72). Three-way interaction β = −1.24, 95%CrI = (−1.90, −0.59), Pr(β < 0) = 0.99.

Equations

• CartnerEtAl2026.topSubjectDD = { construction := FGDConstruction.topicalization, position := ExtractionPosition.subject, dd := 29, citation := "Cartner et al. 2026, Exp 3, Fig. 3" }

def CartnerEtAl2026.topObjectDD : DDScore

Equations

• CartnerEtAl2026.topObjectDD = { construction := FGDConstruction.topicalization, position := ExtractionPosition.object, dd := -19, citation := "Cartner et al. 2026, Exp 3, Fig. 3" }

theorem CartnerEtAl2026.subject_gt_object_whq : whqSubjectDD.dd > whqObjectDD.dd

Subject sub-extraction cost exceeds object sub-extraction cost in ALL three constructions — not just wh-questions.

theorem CartnerEtAl2026.subject_gt_object_rc : rcSubjectDD.dd > rcObjectDD.dd

theorem CartnerEtAl2026.subject_gt_object_top : topSubjectDD.dd > topObjectDD.dd

def CartnerEtAl2026.islandEffect (c : FGDConstruction) : ℤ

The subject island effect (Subject DD − Object DD) per construction.

Equations

• CartnerEtAl2026.islandEffect FGDConstruction.whQuestion = CartnerEtAl2026.whqSubjectDD.dd - CartnerEtAl2026.whqObjectDD.dd
• CartnerEtAl2026.islandEffect FGDConstruction.relativeClause = CartnerEtAl2026.rcSubjectDD.dd - CartnerEtAl2026.rcObjectDD.dd
• CartnerEtAl2026.islandEffect FGDConstruction.topicalization = CartnerEtAl2026.topSubjectDD.dd - CartnerEtAl2026.topObjectDD.dd

theorem CartnerEtAl2026.island_effect_positive_whq : islandEffect FGDConstruction.whQuestion > 0

The island effect is positive for all three constructions.

theorem CartnerEtAl2026.island_effect_positive_rc : islandEffect FGDConstruction.relativeClause > 0

theorem CartnerEtAl2026.island_effect_positive_top : islandEffect FGDConstruction.topicalization > 0

theorem CartnerEtAl2026.island_effect_invariance : have whq := islandEffect FGDConstruction.whQuestion; have rc := islandEffect FGDConstruction.relativeClause; have top := islandEffect FGDConstruction.topicalization; whq > 0 ∧ rc > 0 ∧ top > 0 ∧ 2 * whq ≤ 3 * rc ∧ 2 * rc ≤ 3 * whq ∧ 2 * whq ≤ 3 * top ∧ 2 * top ≤ 3 * whq ∧ 2 * rc ≤ 3 * top ∧ 2 * top ≤ 3 * rc

Cross-constructional invariance: The island effect magnitudes are of similar order across all three constructions (34–48 on the ×100 z-score scale), despite the constructions having distinct IS profiles. Each effect is within 3/2 of every other.

theorem CartnerEtAl2026.fbc_falsified_for_rc : ¬fbcPredictsIsland FGDConstruction.relativeClause ∧ islandEffect FGDConstruction.relativeClause > 0

The FBC is falsified for RCs: It predicts no island effect for relative clauses, but the data shows a robust subject island effect.

theorem CartnerEtAl2026.fbc_falsified_for_top : ¬fbcPredictsIsland FGDConstruction.topicalization ∧ islandEffect FGDConstruction.topicalization > 0

The FBC is falsified for TOPs: It predicts no island effect for topicalization, but the data shows a robust subject island effect.

theorem CartnerEtAl2026.fbc_revised_falsified_for_rc : ¬fbcRevisedPredictsIsland FGDConstruction.relativeClause ∧ islandEffect FGDConstruction.relativeClause > 0

The revised FBC (@cite{winckel-et-al-2025}) is equally falsified.

theorem CartnerEtAl2026.fbc_revised_falsified_for_top : ¬fbcRevisedPredictsIsland FGDConstruction.topicalization ∧ islandEffect FGDConstruction.topicalization > 0

The paper explicitly notes (§8, p.12):

"We note that our results only speak to the FBC, and do not contradict
direct backgroundedness approaches (Cuneo & Goldberg, 2023)."

The constructional IS profile account (FBC) attributes islands to the interaction of the construction's IS profile with the filler's IS status. The direct backgroundedness account (BCI, @cite{cuneo-goldberg-2023}) attributes islands to the degree of backgroundedness of the extraction domain itself, independent of the filler's IS profile.

Since subjects were systematically more backgrounded than objects across all three constructions tested, direct backgroundedness could in principle capture the results. The paper did not manipulate backgroundedness directly, so the BCI remains unfalsified.

This matters for linglib integration: BackgroundedIslands.lean formalizes the direct backgroundedness account (for MoS verbs, via QUD-determined backgroundedness). That formalization is NOT undermined by Cartner et al.'s findings — they target a different theory.

inductive CartnerEtAl2026.DiscourseIslandTheory : Type

Discourse-based island theories distinguished by what drives the prediction: the construction's IS profile (FBC) or the extraction domain's backgroundedness (BCI).

• constructionalISProfile : DiscourseIslandTheory

  Island status depends on IS profile of the construction (filler status interacts with domain status). @cite{abeille-et-al-2020}.

• directBackgroundedness : DiscourseIslandTheory

  Island status depends on the degree of backgroundedness of the extraction domain, independent of construction type. @cite{cuneo-goldberg-2023}.

@[implicit_reducible]

instance CartnerEtAl2026.instDecidableEqDiscourseIslandTheory : DecidableEq DiscourseIslandTheory

Equations

• CartnerEtAl2026.instDecidableEqDiscourseIslandTheory x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def CartnerEtAl2026.instReprDiscourseIslandTheory.repr : DiscourseIslandTheory → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance CartnerEtAl2026.instReprDiscourseIslandTheory : Repr DiscourseIslandTheory

Equations

• CartnerEtAl2026.instReprDiscourseIslandTheory = { reprPrec := CartnerEtAl2026.instReprDiscourseIslandTheory.repr }

def CartnerEtAl2026.cartnerTestsTheory : DiscourseIslandTheory → Bool

Cartner et al.'s experiments test the constructional IS profile account (by varying construction type while holding domain backgroundedness constant), NOT the direct backgroundedness account.

Equations

• CartnerEtAl2026.cartnerTestsTheory CartnerEtAl2026.DiscourseIslandTheory.constructionalISProfile = true
• CartnerEtAl2026.cartnerTestsTheory CartnerEtAl2026.DiscourseIslandTheory.directBackgroundedness = false

theorem CartnerEtAl2026.bci_not_falsified : cartnerTestsTheory DiscourseIslandTheory.directBackgroundedness = false

The direct backgroundedness account (BCI) is untouched by these results. This connects to the existing formalization in Theories/Semantics/Focus/BackgroundedIslands.lean, which models QUD-determined backgroundedness for MoS islands — a different phenomenon that these experiments do not address.

def CartnerEtAl2026.predictsInvariance : IslandSource → Bool

An island source predicts construction-invariance iff it attributes the island to a mechanism shared across all filler-gap constructions.

The syntactic account (Subject Condition) attributes subject islands to the abstract movement operation, shared by WHQs, RCs, and TOPs → predicts invariance. The discourse account (FBC) attributes subject islands to an IS clash, which varies by construction → predicts variance.

Equations

• CartnerEtAl2026.predictsInvariance Phenomena.Islands.IslandSource.syntactic = true
• CartnerEtAl2026.predictsInvariance Phenomena.Islands.IslandSource.semantic = true
• CartnerEtAl2026.predictsInvariance Phenomena.Islands.IslandSource.processing = true
• CartnerEtAl2026.predictsInvariance Phenomena.Islands.IslandSource.discourse = false

def CartnerEtAl2026.subjectIslandSource : IslandSource

Subject islands are syntactically sourced: they arise from a structural constraint on movement (Subject Condition / Phase + anti-locality) that is shared across all filler-gap constructions.

Derived from the construction-invariance data (§§6–7): all three FGD types show statistically indistinguishable subject island costs. This matches the syntactic prediction (same constraint → same cost) and falsifies the discourse/FBC prediction (different IS profiles → different costs).

Equations

• CartnerEtAl2026.subjectIslandSource = Phenomena.Islands.IslandSource.syntactic

theorem CartnerEtAl2026.syntactic_predicts_invariance : [subjectIslandSource].all predictsInvariance = true

theorem CartnerEtAl2026.discourse_predicts_variance : predictsInvariance Phenomena.Islands.IslandSource.discourse = false

The discourse source would predict construction-dependent effects — inconsistent with the data.

structure CartnerEtAl2026.SubExtractionCost : Type

Sub-extraction cost relative to full extraction, from the cross- constructional posterior analysis (Section 7, Fig. 5). Values × 100.

These are (sub-extraction cost) − (full extraction cost) for subjects, estimated from ordinal mixed-effects regression posteriors with 95% HPDIs.

• construction : FGDConstruction
• cost : ℕ

  Point estimate × 100

• hpdiLo : ℕ

  95% HPDI lower bound × 100

• hpdiHi : ℕ

  95% HPDI upper bound × 100

• citation : String

@[implicit_reducible]

instance CartnerEtAl2026.instReprSubExtractionCost : Repr SubExtractionCost

Equations

• CartnerEtAl2026.instReprSubExtractionCost = { reprPrec := CartnerEtAl2026.instReprSubExtractionCost.repr }

def CartnerEtAl2026.instReprSubExtractionCost.repr : SubExtractionCost → ℕ → Std.Format

Equations

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

def CartnerEtAl2026.whqSubjectSubExCost : SubExtractionCost

Equations

• CartnerEtAl2026.whqSubjectSubExCost = { construction := FGDConstruction.whQuestion, cost := 132, hpdiLo := 102, hpdiHi := 161, citation := "Cartner et al. 2026, §7" }

def CartnerEtAl2026.rcSubjectSubExCost : SubExtractionCost

Equations

• CartnerEtAl2026.rcSubjectSubExCost = { construction := FGDConstruction.relativeClause, cost := 134, hpdiLo := 104, hpdiHi := 164, citation := "Cartner et al. 2026, §7" }

def CartnerEtAl2026.topSubjectSubExCost : SubExtractionCost

Equations

• CartnerEtAl2026.topSubjectSubExCost = { construction := FGDConstruction.topicalization, cost := 115, hpdiLo := 85, hpdiHi := 145, citation := "Cartner et al. 2026, §7" }

theorem CartnerEtAl2026.all_hpdis_exclude_zero : whqSubjectSubExCost.hpdiLo > 0 ∧ rcSubjectSubExCost.hpdiLo > 0 ∧ topSubjectSubExCost.hpdiLo > 0

All three 95% HPDIs exclude zero — each construction shows a reliable additional sub-extraction cost for subjects.

theorem CartnerEtAl2026.hpdis_overlap : whqSubjectSubExCost.hpdiLo < rcSubjectSubExCost.hpdiHi ∧ rcSubjectSubExCost.hpdiLo < whqSubjectSubExCost.hpdiHi ∧ whqSubjectSubExCost.hpdiLo < topSubjectSubExCost.hpdiHi ∧ topSubjectSubExCost.hpdiLo < whqSubjectSubExCost.hpdiHi ∧ rcSubjectSubExCost.hpdiLo < topSubjectSubExCost.hpdiHi ∧ topSubjectSubExCost.hpdiLo < rcSubjectSubExCost.hpdiHi

The 95% HPDIs largely overlap across constructions, consistent with a single underlying constraint of stable magnitude.

theorem CartnerEtAl2026.argument_chain : subjectGivenness FGDConstruction.whQuestion = subjectGivenness FGDConstruction.relativeClause ∧ subjectGivenness FGDConstruction.relativeClause = subjectGivenness FGDConstruction.topicalization ∧ fillerFocus FGDConstruction.whQuestion ≠ fillerFocus FGDConstruction.relativeClause ∧ fbcPredictsIsland FGDConstruction.whQuestion ∧ ¬fbcPredictsIsland FGDConstruction.relativeClause ∧ ¬fbcPredictsIsland FGDConstruction.topicalization ∧ (fbcPredictsIsland FGDConstruction.whQuestion ↔ fbcRevisedPredictsIsland FGDConstruction.whQuestion) ∧ (fbcPredictsIsland FGDConstruction.relativeClause ↔ fbcRevisedPredictsIsland FGDConstruction.relativeClause) ∧ (fbcPredictsIsland FGDConstruction.topicalization ↔ fbcRevisedPredictsIsland FGDConstruction.topicalization) ∧ islandEffect FGDConstruction.whQuestion > 0 ∧ islandEffect FGDConstruction.relativeClause > 0 ∧ islandEffect FGDConstruction.topicalization > 0 ∧ subjectIslandSource = Phenomena.Islands.IslandSource.syntactic ∧ [subjectIslandSource].all predictsInvariance = true ∧ predictsInvariance Phenomena.Islands.IslandSource.discourse = false ∧ cartnerTestsTheory DiscourseIslandTheory.directBackgroundedness = false

The paper's complete argument in one theorem.

Premises:

• Subjects have uniform IS across constructions (the controlled variable)
• Fillers differ in IS across constructions (the manipulated variable)
• Both FBC formulations predict only WHQs show subject islands
• All three constructions show subject island effects (the data)

Conclusions:

• The FBC is falsified (it predicts construction-dependence; data shows construction-invariance)
• The syntactic account is corroborated (it predicts invariance)
• The direct backgroundedness account (BCI) is not tested

Cartner et al.'s super-additive design (cross-constructional invariance of subject-island costs) and Adger's Angular Locality (graph-theoretic cross-dimensional path failure) reach the same IslandSource.syntactic verdict for subject islands from incompatible foundations:

• Cartner et al.: subjectIslandSource = .syntactic because the invariance pattern is what an abstract syntactic constraint on movement would predict (and what a constructional-IS account would falsify).
• Adger AL: Adger2025.adgerSubjectIslandSource = .syntactic because sub-extraction from within g_subject_island traverses a cross- dimensional path (SynGraph.subject_island_blocks).

Convergence by rfl — both files independently classify subject-island sources as syntactic; the agreement is type-level. The mechanisms remain incompatible (graph-theoretic parthood across dimensions vs construction- invariance over filler-gap dependencies); the convergent verdict is what makes the agreement informative.

theorem CartnerEtAl2026.subject_island_source_converges_with_adger : subjectIslandSource = Adger2025.adgerSubjectIslandSource

Convergence with @cite{adger-2025}: both Cartner et al. (cross- constructional invariance) and Adger AL (cross-dimensional path failure) classify subject-island sources as syntactic.