Left-Nested Conditionals: Bridge

@cite{lassiter-2025}

Connects the LNC empirical data from @cite{cao-white-lassiter-2025} to the conditional marker typology in Fragments/{Language}/Conditionals.lean.

Bridge Structure

1. Marker type verification: the LNC acceptability pattern correlates with marker type — PC-compatible markers (.both) yield acceptable LNCs, HC-only markers (.hcOnly) yield degraded LNCs.
2. Per-datum marker connection: links specific LNC examples to their corresponding Fragment marker entries.

The LNC acceptability pattern correlates with marker type:

• PC-compatible markers (.both) yield acceptable LNCs
• HC-only markers (.hcOnly) yield degraded LNCs

These guards verify that the Fragment marker entries have the expected types, connecting the LNC empirical data to the marker typology.

theorem Phenomena.Conditionals.LeftNested.Bridge.nara_ok_and_pc_compatible : (ex15_japaneseNara.acceptability == "ok") = true ∧ (Fragments.Japanese.Conditionals.nara.markerType == Semantics.Conditionals.ConditionalMarkerType.both) = true

Japanese nara (PC-compatible) yields acceptable LNC.

theorem Phenomena.Conditionals.LeftNested.Bridge.ra_odd_and_hc_only : (ex16_japaneseRa.acceptability == "odd") = true ∧ (Fragments.Japanese.Conditionals.ra.markerType == Semantics.Conditionals.ConditionalMarkerType.hcOnly) = true

Japanese -ra (HC-only) yields degraded LNC.

theorem Phenomena.Conditionals.LeftNested.Bridge.wenn_ok_and_pc_compatible : (ex20_germanWenn.acceptability == "ok") = true ∧ (Fragments.German.Conditionals.wenn.markerType == Semantics.Conditionals.ConditionalMarkerType.both) = true

German wenn (PC-compatible) yields acceptable LNC.

theorem Phenomena.Conditionals.LeftNested.Bridge.falls_marginal_and_hc_only : (ex21_germanFalls.acceptability == "marginal") = true ∧ (Fragments.German.Conditionals.falls.markerType == Semantics.Conditionals.ConditionalMarkerType.hcOnly) = true

German falls (HC-only) yields degraded LNC.