feat(Query): add query complexity framework#376

Closed

kim-em wants to merge 15 commits intoleanprover:mainfrom

kim-em:feat/tickm-complexity-demo

Commits on Mar 3, 2026

feat(Query): add query complexity framework with sorting lower bounds

kim-em
and
claude
committed
feat(Query): prove sorting lower bound and decision tree depth lemma

kim-em
and
claude
committed
fix(Query): suppress unusedArguments lint for OracleQueryTree

kim-em
and
claude
committed
fix(Query): correct author name spelling

kim-em
and
claude
committed
feat(Query): generalize decision tree depth lemma to Fintype R

kim-em
and
claude
committed
feat(Query): relax LowerBound from size x = n to size x ≤ n

kim-em
and
claude
committed
proof cleanup
kim-em
committed
proof cleanup: deduplicate queryTree_correct, inline hsplit

kim-em
and
claude
committed
proof cleanup: use grind in id_run proofs, inline set σ

kim-em
and
claude
committed
refactor: use named arguments in queryTree_correct

kim-em
and
claude
committed
refactor: add triple_mono, DRY queryTree_correct

kim-em
and
claude
committed

Commits on Mar 4, 2026