Cross-Bridge Consistency Tests #
Verifies that all bridge files agree on fragment verb classifications. Each verb that appears in multiple bridges gets a single theorem here checking that its vendlerClass, verbIncClass, and levinClass fields yield consistent licensing predictions across all classification paths.
What it catches #
If you change a fragment verb annotation (e.g., eat.vendlerClass
from .accomplishment to .activity), the per-bridge theorems in
each bridge file break individually. But this file additionally
verifies that the cross-cutting invariants hold:
- vendlerClass and verbIncClass agree on telicity
- vendlerClass and levinClass agree on path/telicity
- predictsGRAD and predictsSSR are complementary for the same verb
- All classification paths (VendlerClass, Telicity, MereoTag, Boundedness) converge at the same licensing prediction
Sinc/inc verbs should be accomplishments (telic with incremental theme). CumOnly verbs should be activities (atelic, no theme-event mapping). Intransitives (no verbIncClass) can be any class.
"eat": accomplishment + sinc → telic VP with incremental theme.
"build": accomplishment + sinc → telic VP with incremental theme.
"read": accomplishment + inc → telic VP with incremental (non-strict) theme.
"push": activity + cumOnly → atelic VP, no theme-event mapping.
"kick": activity + no verbIncClass → atelic, no incremental theme.
GRAD (gradual change) is predicted for sinc/inc verbs, which are accomplishments (telic). SSR (subinterval reference) is predicted for states/activities (atelic). These should be complementary: a verb should not predict both GRAD and SSR.
"eat": GRAD ✓, SSR ✗ (accomplishment, sinc).
"build": GRAD ✓, SSR ✗ (accomplishment, sinc).
"read": GRAD ✓, SSR ✗ (accomplishment, inc).
"push": GRAD ✗, SSR ✓ (activity, cumOnly).
"sleep": GRAD ✗, SSR ✓ (state, no incremental theme).
"run": GRAD ✗, SSR ✓ (activity, no incremental theme).
For each shared verb, verify the complete chain from fragment annotation through all classification levels to licensing and diagnostic predictions. Changing any fragment field breaks the entire chain for that verb.
"eat": accomplishment → telic → QUA → closed → licensed → "in X" ✓.
"arrive": achievement → telic → QUA → closed → licensed → "in X" ✓.
"sleep": state → atelic → CUM → open → blocked → "for X" ✓.
"run": activity → atelic → CUM → open → blocked → "for X" ✓.
"see": state → atelic → CUM → open → blocked → "for X" ✓.
"leave": achievement → telic → QUA → closed → licensed → "in X" ✓.
"kill": accomplishment → telic → QUA → closed → licensed → "in X" ✓.
"give": accomplishment → telic → QUA → closed → licensed → "in X" ✓.
"cover": accomplishment → telic → QUA → closed → licensed → "in X" ✓.
"buy": accomplishment → telic → QUA → closed → licensed → "in X" ✓.
"sell": accomplishment → telic → QUA → closed → licensed → "in X" ✓.
"break": accomplishment → telic → QUA → closed → licensed → "in X" ✓.
"tear": accomplishment → telic → QUA → closed → licensed → "in X" ✓.
"burn": accomplishment → telic → QUA → closed → licensed → "in X" ✓.
"destroy": accomplishment → telic → QUA → closed → licensed → "in X" ✓.
"melt": accomplishment → telic → QUA → closed → licensed → "in X" ✓.
"put": achievement → telic → QUA → closed → licensed → "in X" ✓.
"meet": achievement → telic → QUA → closed → licensed → "in X" ✓.
"chase": activity → atelic → CUM → open → blocked → "for X" ✓.
"hit": activity → atelic → CUM → open → blocked → "for X" ✓.
"weigh": state → atelic → CUM → open → blocked → "for X" ✓.
"measure": state → atelic → CUM → open → blocked → "for X" ✓.
"enjoy": state → atelic → CUM → open → blocked → "for X" ✓.
"like": state → atelic → CUM → open → blocked → "for X" ✓.
"hate": state → atelic → CUM → open → blocked → "for X" ✓.
"admire": state → atelic → CUM → open → blocked → "for X" ✓.
"envy": state → atelic → CUM → open → blocked → "for X" ✓.
"respect": state → atelic → CUM → open → blocked → "for X" ✓.
"value": state → atelic → CUM → open → blocked → "for X" ✓.
Motion verbs have both vendlerClass and levinClass annotations. Verify these are consistent: inherently-directed-motion verbs (achievements) have bounded paths, manner-of-motion verbs (activities) have no inherent path.
"arrive": achievement + inherentlyDirectedMotion + bounded path.
"leave": achievement + leave class + source path.
"run": activity + mannerOfMotion + no inherent path.
These tests loop over allVerbs so adding a new verb to the fragment
automatically includes it in the test suite — no per-verb theorem needed.
If a new verb has an inconsistent annotation, native_decide fails.
Pipeline consistency: for any verb with a vendlerClass annotation,
the VendlerClass → Telicity → MereoTag → Boundedness chain must
produce a licensing prediction that agrees with the for/in diagnostic.
Returns true for verbs without vendlerClass (vacuously OK).
Equations
- One or more equations did not get rendered due to their size.
Instances For
Every verb in the fragment passes pipeline consistency.
VendlerClass × VerbIncClass coherence: sinc/inc verbs must be
accomplishments (telic), cumOnly verbs must be activities (atelic).
Returns true for verbs without verbIncClass (vacuously OK).
Equations
- One or more equations did not get rendered due to their size.
Instances For
Every verb in the fragment has coherent VendlerClass × VerbIncClass.
GRAD × SSR complementarity: no verb should predict both gradual
change (sinc/inc) and subinterval reference (state/activity).
Returns true if the verb doesn't predict both.
Equations
Instances For
No verb in the fragment predicts both GRAD and SSR.
Count of verbs with vendlerClass annotations (for coverage tracking). Bump this number when adding new vendlerClass annotations.
Every verb with a degreeAchievementScale also has a vendlerClass, and
the derived vendlerClass from the scale matches the stipulated one.
Adding a new degree achievement verb with inconsistent annotations
will cause native_decide to fail.
For a verb with degreeAchievementScale, check that vendlerClass is present and matches the derived value from the scale.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Every verb with degreeAchievementScale has vendlerClass matching the derived value.
K89's table-14 thematic classes (gradualEffectedPatient /
gradualConsumedPatient / gradualPatient / affectedPatient /
stimulus) refine to K98's VerbIncClass (sinc / inc / cumOnly)
via Krifka1989.K89ThematicClass.toVerbIncClass. The fragment
annotations in Verbal.lean should be consistent with both: e.g.,
eat's K98 verbIncClass = sinc must match K89's eat-an-apple class
(gradualConsumedPatient → toVerbIncClass = sinc). This section
makes the three-layer K89 ↔ K98 ↔ Fragment chain explicit.
eat an apple (K89 §4 gradual-consumed-patient) refines to K98 sinc,
which matches eat's fragment annotation.
write a letter (K89 §4 gradual-effected-patient) refines to K98 sinc,
which matches write's fragment annotation.
read a letter (K89 §4 gradual-patient, lacks UNI-E) refines to
K98 inc, which matches read's fragment annotation (allows
re-reading).
Sections 1–7 verify the Bool-tag pipeline (VendlerClass → Telicity
→ MereoTag → Boundedness → for/in licensing). This section
verifies the propositional propagation chain at the typeclass
level: given [IsSincVerb θ] (which bundles SINC + UP + CumTheta;
declared in Theories/Semantics/Events/Aspect/Incremental.lean),
QUA and CUM propagate through the verb's incremental theme to the
VP via substrate's typeclass-form qua_propagation and
cum_propagation (Theories/Semantics/Events/Aspect/Cumulativity.lean).
These are propositional cousins of §3's full-pipeline tests — same
K89 → K98 chain, but at the substrate level rather than the
Bool-tag level. They fire on any `[IsSincVerb θ]` instance; the
concrete `eatThemeToy` instance in
`Phenomena/TenseAspect/Studies/Krifka1998.lean` §9 proves the
typeclass admits real witnesses.
For any sinc verb θ and any QUA object, the VP is QUA (telic).
Verifies the K89 → K98 propositional chain at the typeclass level:
given [IsSincVerb θ] (bundling SINC + UP + CumTheta), QUA
propagates through the verb's incremental theme to the VP. Direct
invocation of substrate's typeclass-form qua_propagation.
For any verb θ with CumTheta — including cumOnly classes
(push, carry) and the strictly stronger SINC/INC classes
(which auto-derive [IsCumThetaVerb θ] via the upward instances
in Aspect/Incremental.lean / Aspect/Incremental.lean) —
a CUM object yields a CUM VP. K98 §3.3 cum-propagation at maximal
typeclass generality; subsumes the SINC-only case. Direct
invocation of substrate's typeclass-form cum_propagation.