claim narrative

authored prose — context, never evidence. the projection it belongs to is u.agora.claim.2026-10-27.computed.bounded-subtype.commuting-rule-decided-by-a-tree-calculus-checker.

A bounded subtype check, done as a reduction.

dtype is encoded Church-style (seven handlers L S F V FU Q AS), so dispatch is
application and the checker is one tree-calculus program with no host help.
Rules implemented: reflexivity (structural dEq over the encoding), the six
congruence rules (Stem/Fork/Asf/Quant covariant, Funty contravariant), the four
quantifier-commuting rules, closed-quantifier elimination Quant t <= t for
Var-free t, and three building rules (Leaf <= Funty u (Stem u);
Stem u <= Funty v (Fork u v); Fork Leaf u <= Funty v u).

Evidence: a 22-case matrix (16 expected-true instances covering every rule
above, 6 expected-false) evaluates to true in a single run; the cited run is
the commuting instance Quant (Stem Leaf) <= Stem (Quant Leaf), decided by
ordinary application.

NOT included: sub_inst and sub_lift (they need de Bruijn substitution/lifting
plus a depth-bounded instantiation search), so subtype bf eager_ty answers
false by measurement. The quantifier rules are the remaining work.