claim narrative

authored prose — context, never evidence. the projection it belongs to is u.agora.claim.2026-10-27.computed.subtype-rules-as-reduction.quantifier-free-building-rules-hold-on-1804-cells.

Jay's subtypes.v "building trees" rules over dtype:
  Leaf <= Funty u (Stem u)
  Stem u <= Funty v (Fork u v)
  Fork Leaf u <= Funty v u
  Fork (Fork u v) w <= Funty Leaf u
  Fork (Fork u (Funty v1 v2)) w <= Funty (Stem v1) v2
Read operationally (Funty A B = applied to an A, the result has type B; and
program_type = value), each rule is an application identity. Checked by
running, not by proof: every p of those five shapes with u,v,w ranging over
all trees with <=2 internal nodes, arguments x over all trees with <=3,
1804 cells, 0 mismatches, 57 434 steps, replayable.

So the quantifier-free part of the type system IS the calculus' own
dispatch -- typing adds no discipline there. What exceeds the calculus is
quantification: subtype is an Inductive Prop (subtypes.v) with sub_inst and
sub_lift (arbitrary instantiation and introduction), so the development has
no decision procedure; "a type check is a reduction" has to be built, not
inherited.