Skip to content

test(interval): exercise nested branch scheduling - #9226

Merged
kim-em merged 3 commits into
mainfrom
agent/interval-nested-tree
Aug 14, 2026
Merged

test(interval): exercise nested branch scheduling#9226
kim-em merged 3 commits into
mainfrom
agent/interval-nested-tree

Conversation

@kim-em

@kim-em kim-em commented Aug 11, 2026

Copy link
Copy Markdown
Owner

Summary

  • add a live Mathlib-free two-level branch tree
  • use the branch side to fork different child policy states
  • pin distinct depth-first and breadth-first frontiers after the nested split
  • verify both orders settle to the same retained tree with three target leaves

The second source is deliberately irrelevant to the exponential target: this isolates scheduling/accounting behavior and does not claim a useful subdivision benchmark.

Exact reconciliation

  • base: 37bda079c4c9974da49c9e8a8559a66d2e671b45 (post-feat(interval): replay pinned exponential tail #9261 main)
  • head: 927427ad931b605bf6c3009b7efe0acc0bc4b82c
  • preserves the PNT log-table, nested-log, and exponential-tail experiments and all prior interval content
  • proof-only Lake freshness exemption is pinned to exact resolved lakefile.lean blob a869c195af5b211b96e848d4f11754abb64ebcc8

Verification

  • lake build HexInterval.NestedBranchConformance HexInterval.Experiment.BranchProof HexIntervalMathlib.ReluConformance HexIntervalMathlib.PntLogTableConformance HexIntervalMathlib.PntNestedLogConformance HexIntervalMathlib.PntExpTailConformance HexInterval.SinTenIntervalConformance HexIntervalMathlib.SinTenConformance HexIntervalMathlib.SinTenIntervalConformance (2253 jobs)
  • copyright, file-line, DAG, trust-surface, Phase 4, factor-freshness, PNT-inventory, and diff checks
  • no added native_decide, axiom, sorry, admit, unsafe, or implemented_by
  • fresh exact-head Opus review and exact-head CI required before merge readiness

@kim-em
kim-em force-pushed the agent/interval-branch-proof branch from ddf6c69 to 47bff5d Compare August 11, 2026 18:10
@kim-em
kim-em force-pushed the agent/interval-nested-tree branch from a474872 to 0e6f619 Compare August 11, 2026 18:10
@kim-em
kim-em force-pushed the agent/interval-nested-tree branch from 0e6f619 to b4e0336 Compare August 11, 2026 18:25
@kim-em
kim-em force-pushed the agent/interval-branch-proof branch from e20ae06 to ea2e5e0 Compare August 11, 2026 19:41
@kim-em
kim-em force-pushed the agent/interval-nested-tree branch from b4e0336 to e3ab6dc Compare August 11, 2026 19:41
@kim-em
kim-em force-pushed the agent/interval-branch-proof branch from ea2e5e0 to 99c058f Compare August 14, 2026 19:07
@kim-em
kim-em changed the base branch from agent/interval-branch-proof to main August 14, 2026 20:08
@kim-em
kim-em force-pushed the agent/interval-nested-tree branch from e3ab6dc to 927427a Compare August 14, 2026 20:08
@kim-em
kim-em merged commit 591a331 into main Aug 14, 2026
1 check passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant