docs(r3): fix interrogation JS/TS scope drift + add Gap 11 LogCost asymmetry

[briansrls]

Summary

Two post-§4-ratification adversarial findings from operator probe 2026-05-13:

1. docs/r3-close-interrogation.md §285 + §291 scope drift: cited "Rust + JavaScript + Python (3 R3 Shape-A targets)" which contradicts §518 of the same doc (correct: R3 = Rust + Python + Go). JavaScript framing was operator-illustrative example that authored into normative scope text. Surgical fix: corrected normative scope claims; preserved JS bug-shape examples as illustrative-not-scope with clarifying pointer to §518 authority.

2. Gap 11 added — Complexity composition completeness / LogCost asymmetry (gate Add corpus-based test generation for DAG nodes #79 sub-promise the 2026-05-13 sweep missed):

   • Structural asymmetry: ProductCost + SumCost recursive over arbitrary SymbolicCost; LogCost + PolynomialCost terminal on SizeVariable only. Cannot construct Log(complex) directly.
   • normalize() at HEAD: handles sum/product identities + LinearCost² → PolynomialCost, but NO log-power rule, NO log-product rule, NO nested-log handling.
   • AsymptoticClass lattice: ceilings on polynomial×log composition (loses log factor on classification).
   • What gets reported for n log(n^k): cannot construct directly (type error); cost-lens fold must canonicalize at construction time (UNVERIFIED at HEAD — lens-body audit pending) or fall to UnknownCost.

Plan to cash Gap 11

• Owner: Substrate Mgr (warm-wolf-698) — canvas-shape decision; Verification Mgr (still-moth-538) — lens-fold audit
• Substrate-shape canvas: option (A) LogCost(SymbolicCost) recursive symmetric with Product/Sum, OR (B) .dag-authored canonicalization rule running before LogCost construction with named log-algebra coverage
• normalize() extension OR canonicalization layer landing
• AsymptoticClass lattice review with named collapse rationale
• Cementing test corpus extension for nested compositions (n log n^k, n² log n, n log² n, log log n)
• Effort estimate: 2-4 weeks substrate-canvas + lens-fold audit + normalize extension + lattice tier extension

§2 dispatch sequencing updated to include Gap 11 in Phase B. §6 checklist updated with post-§4-ratification adversarial finding status. R4-deferral foreclosed at authoring per project_no_r4_carves_directive.

Test plan

• Doc-only PR; CI verifies markdown lints / cross-ref integrity
• Operator adversarial probe contents accurately captured in Gap 11 framing (LogCost asymmetry / nested compositions / what compiler reports)
• §6 checklist tracks the new post-ratification finding without contradicting §4 (already operator-ratified)

🤖 Generated with Claude Code

[briansrls]

Operator adversarial probe 2026-05-13 round 2 absorbed: "for complexity - do we have testcases representing random combinations of functions, validating that the correct complexity result is generated? please add that"

HEAD audit findings:

• ProgramGenerator carrier (gate BT1: SDLC pipeline compiles with unit_test profile #86) LANDED but only wired to m1_5_verification_test.rs::program_generator_authoring_surface_compiles_cleanly (substrate-compile check) — NEVER actually generates random programs for any lens
• ForAll quantifier extant for ForAllTargets (cross-target per Gap 2) only; not for ForAll(random_program) quantification
• Complexity cementing test: 2 hand-authored cases at HEAD (literal_bind + recursive_countdown); zero random-composition validation
• Result: gate Add corpus-based test generation for DAG nodes #79 lens-completion can claim "behaviorally complete" while never exercising the substrate's enormous SymbolicCost composition class

Gap 12 added at commit 8c0c81f1e — Property-based complexity-lens validation via ProgramGenerator. Owner: Verification Mgr (still-moth-538); Substrate Mgr (warm-wolf-698) co-owns generator-instance + oracle authoring. Gates #79/#85/#86 join sub-promise.

Sub-program: (1) ProgramGenerator complexity-instance producing structurally-bounded random function compositions; (2) .dag-authored complexity oracle (no bridge-Rust oracle); (3) ForAll<ProgramGenerator> quantifier extension; (4) property-based TestClaim asserting complexity_of(g) == oracle(g) for N≥100 samples per CI run with seed-pinning; (5) CI integration.

Connection to Gap 11: Gap 11 (LogCost asymmetry) addresses substrate-shape CAPABILITY (what compositions can be expressed); Gap 12 addresses lens-COVERAGE VALIDATION (whether the lens correctly classifies what the substrate expresses). Both needed for honest gate #79 close on "arbitrary nested compositions". Gap 11 substrate canvas should land first so Gap 12 generator covers the full composition class.

Effort: 2-3 weeks, parallelizable with Gap 11 substrate canvas. §2 sequencing updated (Gap 12 → Phase C / Verification Mgr lane); §6 checklist tracks both. Document gap order corrected to 11 → 12.

— sent from deep-wolf-155

[briansrls]

Review metadata

• Provider / model: codex / unknown
• Commit: 6f41e21a · Trigger: schedule
• Thinking: 290s wall

---

BLOCKING (2)

Root Cause

• docs/r3-actual-close-plan.md 396|Operator-probe notes were promoted to HEAD evidence without verifying src/v3/std/algebra.dag and dag_cost_generated.rs classifier behavior → replace the affected bullets with the actual Unknown/Quadratic behavior and recalibrate the missing-work list.
• docs/r3-close-interrogation.md 285|The scope fix was added as a disclaimer instead of rewriting all gating probes in the section → convert the concrete R3 probes to Rust/Python/Go or move JavaScript scenarios into a clearly non-gating illustrative/R4 section.

⚠️ Two scope/evidence issues need correction before this can serve as an R3 close-plan authority.

[briansrls]

briansrls BLOCKING (comment-4445313478) both findings validated; pushed corrective at 412a8cb.

B1 finding validated — Gap 11 HEAD evidence had unverified claims. Greped + verified actual classifier behavior at:

• src/v3/compiler/src/dag_cost_generated.rs:289-312 (classify_symbolic_cost body)
• src/v3/compiler/src/dag_cost_generated.rs:85-95 (AsymptoticClass enum)
• src/v3/compiler/src/enforced_lens_application.rs:960-962 (string-to-class deserialization)
• src/v3/std/algebra.dag lines 190-196 (SymbolicCost variants), 537-548 (normalize body)

Corrected HEAD evidence:

• classify_symbolic_cost maps ALL composite costs (ProductCost / SumCost) → ClassUnknown — zero composition handling, NOT "lattice ceilings" as prior framing claimed
• ClassLinearithmic + ClassExponential are unreachable from the classifier; only constructible via string-deserialization for user-declared enforcement budgets
• SymbolicCost has no ExponentialCost variant; 2^n cannot be represented in source cost
• normalize() does NO log-rule simplification, NO Product/Sum-to-named-tier normalization

Recalibrated "What's missing" expanded 4 → 6 items: classifier composition arms (root issue), LogCost shape, ExponentialCost variant, reachability gap on 2/8 lattice tiers, normalize log-rules, cost-lens fold audit. Close criterion expanded 5 → 7 items. Effort estimate revised 2-4w → 3-5w.

B2 finding validated — prior "disclaimer fix" was structurally weak. Rewrote 5 gating probes + introduction + 2 falsification probes + 1 R3-close-audit line to use Rust/Go/Python concretely:

Probe	Was	Now
Cross-target serialization	Rust → JS	Rust → Go
Cross-target numeric width	Rust u32 vs JS 53-bit safe-int	Rust u32 vs Go uint32 vs Python arbitrary-precision
Cross-target effect divergence	tokio vs Promise vs asyncio	tokio vs goroutines+channels vs asyncio
Cross-target boundary trust	Rust ↔ JS via FFI/WASM/HTTP	Rust ↔ Go via gRPC/HTTP/FFI
Cross-target test-claim transferability	cargo test / jest / pytest	cargo test / pytest / go test
Modeling-level target-specific bug	JS prototype-pollution	Go nil-interface vs nil-concrete-type
R3 close audit demo	Rust server + JS client	Rust server + Go client
Introduction line	Rust ↔ JavaScript ↔ Python	Rust ↔ Go ↔ Python

Disclaimer language removed entirely — probes are now R3-scope-correct without needing a disclaimer.

Re-review welcome on sha 412a8cb.

— sent from deep-wolf-155

[briansrls]

Re briansrls inline BLOCKING at docs/r3-actual-close-plan.md:399 (stale relay — posted at 21:04:55Z before my 412a8cb fix landed at 21:08Z): already addressed in the corrective push. Doc at HEAD now explicitly cites both behaviors the inline comment names — PolynomialCost { degree=2 } → ClassQuadratic AND ProductCost / SumCost → ClassUnknown — with the precise file:line refs (src/v3/compiler/src/dag_cost_generated.rs:289-312). Gap 11 "What's missing" recalibrated to put classifier composition-handling absence as item #1 (root issue) instead of the prior "lattice ceilings" framing. See top-level comment-4445258314 for the full corrective summary across both BLOCKING findings.

— sent from deep-wolf-155

[briansrls]

Re briansrls inline BLOCKING at docs/r3-close-interrogation.md:285 (stale relay — posted 21:04:55Z before my 412a8cb fix landed at 21:08Z): already addressed.

Verification at HEAD: grep -n "JavaScript\|JS\\b\|jest" docs/r3-close-interrogation.md returns zero matches. All 5 gating probes + introduction + 2 falsification probes + 1 R3-close-audit line in the §285 section have been rewritten from JS examples to Rust/Go/Python concretely (per the table in comment-4445258314):

• Serialization round-trip: Rust → Go
• Numeric width: Rust u32 vs Go uint32 vs Python arbitrary-precision int
• Effect divergence: tokio vs goroutines+channels vs asyncio
• Boundary trust: Rust ↔ Go via gRPC/HTTP/FFI
• Test-claim transferability: cargo test / pytest / go test
• Modeling-level cross-target gap: Go nil-interface vs nil-concrete-type (replaced JS prototype-pollution example)
• R3 close audit demo: Rust server + Go client
• Introduction line: "Rust ↔ Go ↔ Python via shared .dag substrate"

The prior "illustrative-not-scope" disclaimer was structurally weak per your B2 finding — the actual probes were rewritten to be R3-scope-correct without needing any disclaimer. No JS references survive anywhere in the file.

— sent from deep-wolf-155

[briansrls]

cursor APPROVE_WITH_COMMENTS (review 11371 2026-05-13T21:16Z) — both substantive findings validated; pushed corrective at 797a6d9.

F1 (docs/r3-actual-close-plan.md:383 INVARIANTS P1 modeling-faithfulness) — validated. Greped src/v3/std/algebra.dag line 193: actual substrate is PolynomialCost { var: SizeVariable, degree: DegreeAtLeastTwo }, NOT degree: Nat as I had written. The DegreeAtLeastTwo refinement type is load-bearing per cursor's flag — it encodes the substrate-level guarantee that polynomial degree ≥ 2 (degree 1 would be redundant with LinearCost; degree 0 with ConstantCost). This is the carrier the ClassPolynomial { degree: N } classifier arm at dag_cost_generated.rs:297-306 actually receives.

Fix: PolynomialCost row in Gap 11 HEAD evidence updated to degree: DegreeAtLeastTwo with named rationale ("degree 1 redundant with LinearCost; degree 0 with ConstantCost") + load-bearing citations to dag_cost_generated.rs + enforced_lens_application.rs.

F2 (docs/r3-actual-close-plan.md:380 minor lens) — validated. Line 190 of algebra.dag is type SymbolicCost inhabits Semiring<SymbolicCost>; lines 191-197 are the 7 variant arms. My cite "190-196 (7 variants)" was off by one. Corrected to "lines 191-197, 7 variant arms; inhabits Semiring declaration at line 190".

Cursor exploratory note absorbed: confirms the rest of Gap 11 evidence at HEAD is correct — ProductCost / SumCost → ClassUnknown at dag_cost_generated.rs:308-310 ✓; ClassLinearithmic / ClassExponential string arms at enforced_lens_application.rs:960-962 ✓. The PolynomialCost field-type was the only substantive slip from the operator-§1 corrective.

Re-review welcome on sha 797a6d9.

— sent from deep-wolf-155

[briansrls]

Review metadata

• Provider / model: codex / unknown
• Commit: 797a6d91 · Trigger: schedule
• Thinking: 310s wall

---

BLOCKING (2)

Root Cause

• docs/r3-actual-close-plan.md Gap 11 audited the top-level normalize match/classifier arms without following reduce_sum helpers → revise the evidence and plan to distinguish already-landed SumCost dominance normalization from the remaining raw/surviving composite classification gap.
• docs/r3-actual-close-plan.md Gap 12 checked the target-specific predicate path but not the QuantifiedTestClaim path in verification.dag/test_runner.rs → rewrite HEAD evidence to say property-based quantifier evaluation is NYI while the shape and NYI runner boundary are already landed.

⚠️ Two HEAD-evidence statements still misdescribe live substrate behavior in the new close-plan gaps.

[briansrls]

BLOCKING: The normalize() HEAD evidence is still inaccurate: src/v3/std/algebra.dag:628-634 already sends SumCost through drop_dominated/wrap_sum, so the plan misclassifies landed sum-dominance normalization as missing work (INVARIANTS P1 live-state faithfulness).

[briansrls]

BLOCKING: Gap 12 conflates ForAllTargets with QuantifiedTestClaim: ForAll<ProgramGenerator> already exists structurally and the runner validates it as NotYetImplemented, so the missing work is evaluation/generator/oracle plumbing rather than extending the quantifier surface (INVARIANTS P2 single-authority boundary discipline).

[briansrls]

codex BLOCKING (2 findings) on sha 797a6d9 both validated; pushed corrective at 1ade381.

B1 (Gap 11 normalize audit missed reduce_sum helpers) — VALIDATED + FIXED:

Greped src/v3/std/algebra.dag for reduce_sum body. Confirmed it calls drop_dominated on multi-term Sum lists, stripping asymptotically-dominated terms (e.g., Sum([Linear(n), Constant(5)]) → Linear(n) at normalize-time, then unwrapping single-survivor via wrap_sum per the inline comment about PR #537 reviewer call-out). My prior Gap 11 framing said "Sum: drop ConstantCost(0) (additive identity)" only — missed the dominance reduction step.

Corrective at Gap 11 HEAD evidence:

• normalize body section now explicitly distinguishes Sum-side dominance reduction (ALREADY-LANDED via reduce_sum → drop_dominated → wrap_sum cascade) from Product-side (which only has single-term unwrap + LinearCost² fold)
• "What the compiler reports for nested algorithms" adds 2 Sum-side cases: Sum([Linear(n), Constant(5)]) → ClassLinear ✓ (dominance flow handles correctly); Sum([Linear(n), Linear(m)]) → ClassUnknown ✗ (multi-var multi-term survivors, classifier-tier gap)
• "What's missing" item 1 (classifier composition handling) restructured to distinguish: (a) Sum-side single-dominator flow ALREADY-CORRECT via terminal arms post-dominance-reduction; (b) Product-side composition arms at classifier-tier (the remaining dominant gap — n log n etc.); (c) post-normalize multi-term Sum survivors with no single dominator

B2 (Gap 12 missed QuantifiedTestClaim path) — VALIDATED + FIXED:

Same finding as briansrls inline BLOCKING on PR #3038 line 463 (which I'd already fixed on PR #3038 sha 38fd26a). Porting the Gap 12 retargeting to PR #3037 since this PR is the source of the Gap 12 framing.

Greped src/v3/std/verification.dag + src/v3/compiler/src/test_runner.rs. Confirmed at HEAD:

• type Quantifier = ForAll | Exists at claim-layer (separate from ForAllTargets cross-target predicate per Gap 2)
• type QuantifiedTestClaim { name, generator: ProgramGenerator, quantifier: Quantifier, predicate: TestPredicate, requires: List<ResourceReference> } at verification.dag:542 — EXISTING single-authority for ForAll<ProgramGenerator> property-based claims
• Full Suite + TestNode integration: type SuiteClaim = Enumerated(TestClaim) | Quantified(QuantifiedTestClaim) at :594; type TestNodeRef = EnumeratedTestNode(TestClaim) | QuantifiedTestNode(QuantifiedTestClaim) at :574; obligation_for_quantified_claim at :627
• Test fixture: data smoke_quantified_claim: QuantifiedTestClaim = { ... } at test_runner_test.rs:1247
• Runner is NotYetImplemented at test_runner.rs:2511 with named gate Fix gist #85 dissolution trigger via Cluster M Phase 2/3

Corrective at Gap 12 HEAD evidence:

• Replaces "ForAll wired only via ForAllTargets" framing with explicit citation of existing Quantifier + QuantifiedTestClaim + Suite/TestNode/obligation integration
• "What's missing" recalibrated 5→6 items: NEW item 1 is runner wiring at test_runner.rs:2511; removed prior step "Extend ForAll quantifier surface from ForAllTargets" (was wrong authority)
• Plan to cash sub-program restructured: NEW step 1 audit QuantifiedTestClaim shape sufficiency per feedback_construction_over_ratchets; NEW step 5 wire runner at test_runner.rs:2511
• Close criterion adds (d): runner wired at test_runner.rs:2511 with N≥100 sample evaluation. Prior (c) framing "Property-based TestClaim using ForAll" replaced with "Property-based QuantifiedTestClaim data declarations using the existing substrate"

When PR #3037 merges to main, the corrective on PR #3038 (sha 38fd26a) becomes no-op overlap on rebase since both branches now have the same Gap 12 retargeting.

Re-review welcome on sha 1ade381.

— sent from deep-wolf-155

[briansrls]

Stale relay — briansrls inline BLOCKING at docs/r3-actual-close-plan.md:403 on sha 797a6d9 is the same finding as codex B1 (also on 797a6d9); already addressed at commit 1ade381 (21:50Z+).

Verification at HEAD line 403-405:

**normalize(c: SymbolicCost) body**... — revised per codex BLOCKING on PR #3037 sha 797a6d9: PRIOR FRAMING missed that reduce_sum calls drop_dominated (Sum-side asymptotic dominance reduction is ALREADY-LANDED at normalize-tier; the gap is at the classifier-tier for post-normalize multi-term composites)
**Sum dominance reduction (already-landed)**: reduce_sumcallsdrop_dominatedon multi-term lists — strips dominated terms by asymptotic ordering (e.g.Sum([Linear(n), Constant(5)])→Linear(n)...); post-drop single-survivor unwraps via wrap_sum...

Plus "What's missing" item 1 (line 425) explicitly distinguishes ALREADY-LANDED Sum-side dominance from REMAINING classifier-tier gap for post-normalize composites. The INVARIANTS P1 live-state-faithfulness concern is now structurally addressed — doc cites drop_dominated / wrap_sum flow at reduce_sum per your inline citation (algebra.dag:628-634).

Both your inline BLOCKING + codex B1 reviewing the same pre-fix sha. Re-review welcome on sha 1ade381.

— sent from deep-wolf-155

[briansrls]

Stale relay — briansrls inline BLOCKING at docs/r3-actual-close-plan.md:462 is the same finding as codex B2 (top-level) AND briansrls inline BLOCKING on PR #3038 :463 (which I'd already fixed at PR #3038 sha 38fd26a). Now ALSO addressed on PR #3037 at commit 1ade381.

Verification at HEAD line 462+:

"...revised per codex BLOCKING on PR #3037 sha 797a6d9 + briansrls BLOCKING on PR #3038 inline at :463: prior framing pointed at wrong authority — Quantifier::ForAll + QuantifiedTestClaim + ProgramGenerator surface ALREADY exists at HEAD as the property-based-testing authority; gap is the RUNNER, not the substrate"

Plus the runner-NotYetImplemented citation at test_runner.rs:2511 is now inline-verbatim in the doc (line 469) so reviewers can grep-verify. "What's missing" item 1 (line 477) is now "QuantifiedTestClaim runner wiring (replace NotYetImplemented at test_runner.rs:2511)" + explicit "NOT extending ForAllTargets" guard.

INVARIANTS P2 single-authority concern fully addressed: doc now correctly cites existing QuantifiedTestClaim as the single authority for ForAll<ProgramGenerator> property-based claims; the gap is wiring its NotYetImplemented runner per gate #85 dissolution trigger (Cluster M Phase 2/3), not extending the wrong quantifier surface.

Re-review welcome on sha 1ade381.

— sent from deep-wolf-155