M13.0: exact value-jump labeling as the stepwise production default (release 1.1.0) - #3
Merged
Conversation
…+ partial fix Session 24 checkpoint (diagnosis complete, fix staged and UNVALIDATED; see workspace reports/sessions/2026-07-17-session-24.md execution log). - 3 strict-xfail reproducer gates (Rifki-2/18/17 exact-path cold soundness). - Trace harness: shared labeling/trace.h + merge/pool instrumentation (KAYROS_TRACE_MERGE: LAM-POP/LAM-WITNESS/MERGE-*/POOL-ADD/POOL-EXIT). - 4 M13.0 unit specs in test_goc_pwl_stepwise.py (3 red: plateau-inner attained value, increasing-inner choice preservation, operator+ attained pairing; 1 green guard). - PARTIAL fix staged in pwl_function.cpp (Compose constant-inner branch, vertical-aware evaluation at y0). NOT rebuilt, NOT validated; do not run certification from this commit. Root cause (checker-refereed): backward-label durations lose mandatory forward waiting through Compose's plateau-inner rule when f carries the same-arc vertical at the plateau value; an under-estimated dominator then erases the witness label at the Exact level (Rifki-2: dominator claims ~1959 where checker-exact is ~12703; certificate closes 73 above optimum). Fix design: extension identity D_next = (D - Id) o dep + Id, data-gated on vertical presence, plus the three vertical-pairing repairs. Co-Authored-By: Claude Fable 5 <[email protected]> Claude-Session: https://claude.ai/code/session_01886h5TXRnC3nN9vyknfmpS
Layer 1, extension arithmetic: on step-carrying arcs (any vertical in dep/tau/D; only ever true on the exact path) the extension uses the elapsed-time identity D_lv = (D - Id) o dep + Id instead of (D + tau) o dep. The legacy composite erased position-dependent mandatory waiting through dep plateaus at same-arc vertical values (checker referee: backward label claimed ~1959 where the true suffix duration is ~12703). Companions: Compose constant-inner branch evaluates verticals at y0 attained/min-aware; Compose increasing-inner preserves CHOICE verticals (span + kind + representative) instead of collapsing to a point; operator+ pairs vertical endpoints attained-with-attained via sweep_endpoints (like operator*). Layer 2, solution pool: keyed by PATH on the exact path (marker: KAYROS_STEP_EXACT + verticals in forward dep) so a checker-cheaper route ordering can no longer be shadowed forever by a bound-cheaper ordering of the same vertex set (Rifki-17: true-2957 ordering shadowed by true-2975). Mollified/jump-free runs keep the legacy set-keyed pool bit-identically. Layer 3, operator+/operator* advance logic: at a shared right boundary, hold the other operand while the next piece is STACKED there (vertical or zero-width point). The old hold-back only applied when the current piece was non-vertical, so a stack of swept choice verticals lost its tail at operand exhaustion (Rifki-17 witness label kept one of eight departure choices and over-estimated its duration by ~1100). Trace harness: EXT-PARENT/EXT-DUMP piece dumps (KAYROS_TRACE_DUMP), arc dumps and step_pool print on KAYROS_TRACE_MERGE. Unit specs: 5 new tests in test_goc_pwl_stepwise.py, all green (27/27). Reproducers on this build: Rifki-2 cold == warm == 7378 (was 7451), Rifki-17 cold == warm == 21319 (was 21330/21331), Rifki-18 UB reaches the true 7127 with honest TL at 300 s locally (certification at larger TL under validation). Gates stay strict-xfail until the full battery passes. Co-Authored-By: Claude Fable 5 <[email protected]> Claude-Session: https://claude.ai/code/session_01886h5TXRnC3nN9vyknfmpS
Rifki-2 (7378) and Rifki-17 (21319) are hard certification gates: cold exact certifies the audited truth (== warm, verified this session). Rifki-18 is a hard soundness gate: the fixed build finds the true 7127 as its incumbent but cannot close the tree within local TLs (honest TimeLimitReached; certification budget judged by the g5k sweep), so the gate asserts no-certificate-above-truth + incumbent == truth + bound consistency. Validation on this build: full suite 744 passed / 3 skipped (19m38s); randomized differential fuzz sweeps clean on BOTH arms (exact and default, 6 passed each, cold == warm and no certificate above the ILS cost). Co-Authored-By: Claude Fable 5 <[email protected]> Claude-Session: https://claude.ai/code/session_01886h5TXRnC3nN9vyknfmpS
…ollifier retired; stamp guard lifted Onyr's decision (2026-07-18, on the full validation dossier: sweep 0 unsound / 0 poisoned / 0 disagreements, crossplat 13/13, TL-losses 9/108): the certifier is used as such, no need to keep the mollifier. - solve_duration auto-enables the exact tagged-vertical path per instance (any duplicate-x ATF breakpoint => KAYROS_STEP_EXACT set before payload build and solver construction; the former dev toggle is now an internal flag). Jump-free instances keep the v1.0.0 arithmetic bit-identically. - The M5.7 forward mollifier (_continuize_breakpoints + _JUMP_DELTA) is deleted; _atf_to_travel_time_pieces emits raw breakpoints (bit-identical for jump-free ATFs, true verticals for stepwise). The C++ reverse-side continuize remains, env-gated as before: on stepwise solves the env disables it (exact path); on jump-free solves it keeps the audited reverse-side representation unchanged. - optimality_metadata stamps stepwise certificates like any other (the single-run refusal guarded the retired mollified path). - test_no_optimality_stamp_on_stepwise_atfs becomes test_stepwise_atfs_stamp_after_m130_promotion (stamp asserted present). Batteries on the promoted build: stepwise soundness + lera + fuzz-pinned suites 22 passed (incl. the symmetric gates now running sym+exact). Co-Authored-By: Claude Fable 5 <[email protected]> Claude-Session: https://claude.ai/code/session_01886h5TXRnC3nN9vyknfmpS
NOTICE item 9 closing amendment (three-layer fix, validation ladder, the 1444-run re-certification), README design paragraph rewritten for the exact value-jump path, CHANGELOG 1.1.0 entry, version bumps (pyproject + CITATION.cff). Co-Authored-By: Claude Fable 5 <[email protected]> Claude-Session: https://claude.ai/code/session_01886h5TXRnC3nN9vyknfmpS
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Closes the last soundness caveat of the certification pipeline: on stepwise (value-jump) travel-time functions the exact component now runs a mollifier-free labeling that carries the value jumps exactly as tagged verticals, and single-run stepwise stamping is enabled.
What changed
(D − Id) ∘ dep + Idon step-carrying arcs (the old composite erased position-dependent mandatory waiting through departure plateaus at same-abscissa jumps).PWLFunction::Compose/operator+/operator*carry jump/choice vertical tags with attained-endpoint pairing (stacked-vertical tails and choice spans were dropped or collapsed).KAYROS_STEP_EXACT; forward mollifier_continuize_breakpointsdeleted; single-run stepwise stamp refusal lifted. Non-stepwise instances are bit-identical to 1.0.0.Validation ladder (all green)
🤖 Generated with Claude Code
https://claude.ai/code/session_01886h5TXRnC3nN9vyknfmpS