Repository navigation
feat(testing): prove three queries necessary for one-sided linearity testing #1811
Description
Worker codex-roadmap-learning-20261030 claims this bounded ROADMAP property-testing lower-bound milestone on branch feat/testing-linearity-lower-20261030 in the isolated learning lane. Fresh issue/PR search found no overlapping owner; #890 M4 and #1573 are excluded, and #1804 remains available separately for independent review/fixes.
Target: in the existing adaptive DecisionTree and finitely supported RandomizedDecisionTree models, any tester with perfect completeness on every parity that rejects some normalized table f with f 0 = false with positive probability needs at least three worst-case queries. Prove the deterministic core: a depth-at-most-two tree accepting every parity accepts every normalized table. Reusable prerequisite: any normalized table's answers at two queried points agree with some parity; retain the zero-point and repeated-query constraints. No new tester/distance/probability model is introduced. This is an elementary original interpolation/indistinguishability proof, not a new claim about two-sided testing or native running time.
Acceptance: documented interpolation and query lower-bound API; arbitrary finite-coordinate types and adaptive trees, then existing finite-simplex randomized trees; concrete two-bit conjunction (distance at least 1/4 from every parity), an explicit three-query tree accepting all parities while rejecting that conjunction, and zero/repeated-point edge checks. Run all six gates, hygiene/import checks, assess curated abstracts, and request outside-author-fleet exact-head review. Existing definitions considered: parityOn, Boolean-ring addition, hammingDist, DecisionTree.eval/queries/depth, and RandomizedDecisionTree.errorProb/depth; reuse them directly.
This milestone complements #1797/#1804's BLR execution/amplification. It leaves native learner runtimes, tolerant/distribution testing, broader access models and two-sided lower bounds open. It is not proposed as a curated headline. AI assistance: OpenAI Codex implements and validates the contribution.
Activity
SamuelSchlesinger commentedon Oct 30, 2026
active— workercodex-roadmap-learning-20261030claims the scope above onfeat/testing-linearity-lower-20261030. Next: prove the two-point parity extension lemma, then transfer it through queried-path agreement to adaptive deterministic and randomized lower bounds. The #1804 branch remains pushed and recoverable; requested fixes there take priority.SamuelSchlesinger commentedon Oct 30, 2026
active—codex-roadmap-learning-20261030: the proved scope is stronger than the initial finite-model target. Two-point parity extension works for arbitrary coordinate types, and the main probability theorem uses an arbitrary PMF on trees with no finite-support assumption. A rejecting run must query at least three distinct points; the existing finite-simplex model gets the worst-case-depth corollary. A fair mixture of immediate acceptance and a three-query check rejects conjunction with probability exactly 1/2, so the probability hypotheses are checked without claiming an expected-depth lower bound. Focused Lean checks pass; full validation and PR submission are next.SamuelSchlesinger commentedon Oct 30, 2026
awaiting review— workercodex-roadmap-learning-20261030submits PR #1815. The PR owns exact-revision validation and the scope/semantics record; all six local gates and hygiene pass. Please arrange outside-author-fleet review of the new public statements. This bounded lower-bound milestone leaves native learner runtimes and broader testing objectives open.SamuelSchlesinger commentedon Oct 30, 2026
awaiting review—codex-roadmap-learning-20261030completed the main/aggregate restack of PR #1815. Its restack record links validation and independent delta coverage; reviewed mathematics and tests are unchanged. Root/LogSq owns hosted checks and integration.feat(testing): prove the adaptive one-sided linearity query lower bou…