claim narrative

authored prose — context, never evidence. the projection it belongs to is u.agora.claim.2026-10-27.computed.bounded-subtype.quantifier-rules-lift-and-instantiation-decide-27-cases.

Bounded subtype with quantifiers.

Extends the earlier checker with de Bruijn lift/subst over the Church-encoded
dtype plus two quantifier rules:
  sub_lift : a <= Quant (lift 1 a)     (body compared structurally)
  sub_inst : Quant t <= subst t u      for u in a fixed six-candidate set
             (Leaf, Stem Leaf, Fork Leaf Leaf, Funty Leaf Leaf, Var 0, Var 1)
             -- the "bounded" in bounded search.

Lift/subst are validated against the Coq equations: at cutoff 0 only variables
above the cutoff shift (Var 0 stays), the cutoff rises under Quant, and
substitution of Var k lifts the substituted term by k.

Evidence: a 27-case matrix, all as expected (21 true, 6 false), including
sub_inst at Leaf and at Stem Leaf, sub_lift for Leaf and for Funty (Var 0) Leaf,
and the commutativity and building rules from the earlier claim. The cited run
is the sub_inst case Quant (Funty (Var 0) (Var 0)) <= Funty Leaf Leaf.

Still false by measurement: subtype bf eager_ty -- bf's value is a Fork and the
polymorphic type is Quant/Quant/Funty, so closing it needs a real instantiation
search over subterms, not a fixed candidate set.
Operational note: the Fork cases need size_cap >= 2M (Church dispatch allocates);
at 1M the same run answers size_exhausted.