Gradability Typology Bridge #
@cite{kennedy-2007}
Per-entry verification that the string-based typology data in Data.lean
matches the Fragment entries in Fragments/English/Predicates/Adjectival.lean
and the LicensingPipeline predictions from Core/Scale.lean.
Bridge Structure #
For each adjective with both a Data.lean typology entry and a Fragment
entry, we verify:
- Form match:
tallTypology.adjective = tall.form - Scale-type consistency:
tallTypology.scaleType = tall.scaleType - Licensing agreement:
LicensingPipeline.isLicensed tall.scaleTypematches the degree modifier compatibility from Data.lean
"tall" typology datum matches Fragment form.
"full" typology datum matches Fragment form.
"wet" typology datum matches Fragment form.
With AdjectiveTypologyDatum.scaleType : Boundedness (refactored
from the prior Bool-pair encoding in 0.230.437), the consistency
theorems can now state full Boundedness equality between the
typology data and the Fragment annotation, rather than just
projecting both onto .hasMax.
"tall" (open): Data scaleType matches Fragment scaleType.
"full" (closed): Data scaleType matches Fragment scaleType.
"wet" (lower-bounded): Data scaleType matches Fragment scaleType.
"straight" (closed): Data scaleType matches Fragment scaleType.
"bent" (lower-bounded): Data scaleType matches Fragment scaleType.
"tall" (open scale): pipeline blocked = "completely" doesn't work with RGA.
"full" (closed scale): pipeline licensed = "completely" works with AGA-max.
"tall": typology's naturalWithCompletely matches pipeline prediction.
"full": typology's naturalWithCompletely matches pipeline prediction.
"tall" (open): threshold shifts with comparison class. Open-scale adjectives are context-sensitive.
"full" (closed): threshold does NOT shift. Closed-scale adjectives are absolute.