Left-Nested Conditionals: Bridge

[Las25] [CWL25]

Connects the LNC data from [CWL25] (Data/Examples/CaoWhiteLassiter2025.json) to the conditional marker typology in Fragments/{Language}/Conditionals.lean.

Main declarations

• markerOf: adapter reading a row's marker feature into the Fragment's ConditionalMarker entry
• acceptable_iff_marker_licenses: a marker-diagnostic row is acceptable iff its marker can mark premise conditionals or non-bare content makes an HC reading available

def Lassiter2025.markerOf (row : Data.Examples.LinguisticExample) : Option Semantics.Conditionals.ConditionalMarker

Marker adapter: the Fragment entry for the row's conditional marker.

Equations

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

def Lassiter2025.bareContent (row : Data.Examples.LinguisticExample) : Bool

Whether the row's inner conditional has bare (non-modal, non-generic) content. Bare content forces the premise-conditional reading, so an HC-only marker cannot rescue the LNC.

Equations

• Lassiter2025.bareContent row = (row.feature? "content" == some "bare")

def Lassiter2025.markerLicenses (row : Data.Examples.LinguisticExample) : Option Bool

The marker typology's prediction for a row: the LNC is licensed iff the marker can mark premise conditionals (.both) or non-bare content makes an HC reading available.

Equations

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

theorem Lassiter2025.acceptable_iff_marker_licenses (row : Data.Examples.LinguisticExample) : row ∈ CaoWhiteLassiter2025.Examples.all → markerOf row ≠ none → (row.judgment = Features.Judgment.acceptable ↔ markerLicenses row = some true)

Transfer equation: every marker-diagnostic row is acceptable iff the marker typology licenses it — PC-compatible nara/wenn yield acceptable bare LNCs, HC-only -ra/falls yield degraded ones, and modal content rescues falls (ex. 22).