feat(dynamics): measurable model-strategy risk certificates

[Robby955]

Summary

• add a two-sided, posterior-uniform singular-fraction LIL event and its exact scalar-fraction optimizer, including the arbitrary measurable trajectory lift
• add the continuous model-posterior and countable sleeping-strategy master with separate model and active-strategy KL costs
• derive an ordinary encountered-prefix conditional-risk certificate by normalizing the selected weights and charging twice their finite-TV discrepancy from uniform weights

The reporting time, eligible model posterior, and posterior on the active strategy prefix may be selected from the observed path on the same common event.

Scope

This is confidence allocation over a countable predictable-strategy catalog fixed before observation. It is not coin betting or competition with every legal predictable strategy. The ordinary endpoint concerns conditional risk encountered on the monitored prefix; it is not future, stationary, population, or deployment risk. The exact scalar-fraction optimizer is a mathematical optimum, not an executable selector.

Verification

• ~/.elan/bin/lake -Kjobs=2 build FormalSLT — passed, 4,096 jobs
• all 281 files in examples/*.lean — passed sequentially
• focused measurable model-strategy checker — passed
• public axiom checks — [propext, Classical.choice, Quot.sound]
• repository scans found no sorry, admit, or custom axiom declarations
• git diff --check origin/main...HEAD — passed

Summary by CodeRabbit

• New Features

  • Added exact optimization for singular-fraction PAC-Bayes boundaries, including an attained optimal fraction and dominance guarantees.
  • Added two-sided continuous PAC-Bayes events with absolute prefix-risk and LIL-order guarantees.
  • Added continuous-model support for countable sleeping strategies, measurable trajectories, and predictable-tilt master processes.
  • Added ordinary prefix-risk bounds covering model and strategy complexity, penalties, exposure, and discrepancy terms.
  • Added measurable e-process properties and posterior-selection guarantees.

• Documentation

  • Expanded module documentation and added verification examples covering the new results.

[chatgpt-codex-connector]

Codex Review Summary

This comment shows the latest Codex review activity on this pull request.

Review	Status	Commit	Review trigger
📝 Code Review	✅ Completed 2026-08-30T21:52:24.872848Z	99c067f	PR opened

ℹ️ About Codex in GitHub

Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you

• Open a pull request for review
• Mark a draft as ready
• Comment "@codex review" or "@codex security review".

Codex reacts with 👀 while any review is running, comments if it has suggestions, and reacts with 👍 once all reviews finish with no findings.

[coderabbitai]

No actionable comments were generated in the recent review. 🎉

ℹ️ Recent review info

⚙️ Run configuration

Configuration used: Path: .coderabbit.yaml

Review profile: ASSERTIVE

Plan: Pro Plus

Run ID: 6967b299-f6da-4c02-8bad-27df9f32aa31

📥 Commits

Reviewing files that changed from the base of the PR and between 99c067f and 766d265.

📒 Files selected for processing (1)

• docs/INDEX.md

Included review availability: Your plan provides up to 1 included review per hour; 0 remain after this review.

---

📝 Walkthrough

Walkthrough

Summary

The PR adds exact singular-fraction optimization, continuous sleeping-strategy PAC-Bayes bounds, two-sided event theorems, measurable-trajectory specializations, umbrella imports, documentation updates, and declaration-checking examples.

Changes

PAC-Bayes extensions

Layer / File(s)	Summary
Exact singular-fraction optimizer FormalSLT/AnytimeValid/SingularFractionExactOptimizer.lean	Defines the exact numerator, cutoff, canonical optimizer, optimized boundary, and global minimization theorems.
Continuous sleeping-process foundation FormalSLT/PACBayes/ContinuousCountableSleepingEProcessPACBayes.lean, FormalSLT/StochasticDynamics/ContinuousMeasurableTrajectorySleepingPredictableTiltMasterProcess.lean	Adds continuous model-prior sleeping master processes, e-process properties, posterior bounds, exceptional events, measurability results, and deterministic envelopes.
Ordinary sleeping-strategy risk bounds FormalSLT/StochasticDynamics/ContinuousMeasurableTrajectoryCountableSleepingStrategyOrdinaryRiskPACBayes.lean	Adds weighted trajectory risks, factorized posterior events, exposure normalization, discrepancy bounds, and ordinary-prefix-risk events.
Two-sided exact scalar events FormalSLT/PACBayes/ContinuousTwoSidedSingularFractionBesselPACBayes.lean, FormalSLT/PACBayes/ContinuousTwoSidedSingularFractionExactOptimalPACBayes.lean	Combines original and complemented events, proves exact-boundary comparisons, and applies the attained optimizer.
Measurable-trajectory PAC-Bayes specialization FormalSLT/StochasticDynamics/ContinuousMeasurableTrajectoryTwoSidedSingularFractionBesselPACBayes.lean, FormalSLT/StochasticDynamics/ContinuousMeasurableTrajectoryTwoSidedSingularFractionExactOptimalPACBayes.lean, FormalSLT/StochasticDynamics/ContinuousTrajectoryEmpiricalBernsteinPACBayes.lean	Adds trajectory measurability proofs, boundary rewrites, all-fractions events, and exact-optimal events.
Umbrella wiring and verification FormalSLT/PACBayes.lean, FormalSLT/Sequential.lean, FormalSLT/StochasticDynamics.lean, examples/*, docs/INDEX.md	Updates umbrella imports and documentation, refreshes one declaration source location, and adds declaration and axiom checks for the new APIs.

Estimated code review effort: 5 (Critical) | ~120 minutes

Merge Risk: ⚪ Minimal · up to 766d2

This PR adds formally verified model-strategy risk certificates and related documentation without introducing a supported merge-blocking correctness, security, availability, or deployment risk; it is merge-ready after normal checks and review.

Sequence Diagram(s)

sequenceDiagram
  participant TrajectoryEvent
  participant TwoSidedPACBayes
  participant ExactOptimizer
  TrajectoryEvent->>TwoSidedPACBayes: supply trajectory measurability and adaptation
  TwoSidedPACBayes->>TwoSidedPACBayes: intersect original and complemented events
  TwoSidedPACBayes->>ExactOptimizer: select canonical optimal lambda
  ExactOptimizer-->>TrajectoryEvent: provide exact optimized boundary

Loading

🚥 Pre-merge checks | ✅ 5

✅ Passed checks (5 passed)

Check name	Status	Explanation
Description Check	✅ Passed	Check skipped - CodeRabbit’s high-level summary is enabled.
Title check	✅ Passed	The title clearly summarizes the main change: measurable model-strategy risk certificates for continuous models and sleeping strategies. It is concise and specific.
Docstring Coverage	✅ Passed	No functions found in the changed files to evaluate docstring coverage. Skipping docstring coverage check. Docstring coverage is scoped to functions touched by this diff. Analyzed 0 functions across 0…
Linked Issues check	✅ Passed	Check skipped because no linked issues were found for this pull request.
Out of Scope Changes check	✅ Passed	Check skipped because no linked issues were found for this pull request.

Full details: Docstring Coverage

Explanation

No functions found in the changed files to evaluate docstring coverage. Skipping docstring coverage check. Docstring coverage is scoped to functions touched by this diff. Analyzed 0 functions across 0 files. (1 skipped: 1 unsupported.)

✨ Finishing Touches

🧪 Generate unit tests (beta)

• Create PR with unit tests
• Commit unit tests in branch codex/continuous-countable-trajectory-risk-20260830

---

Thanks for using CodeRabbit! It's free for OSS, and your support helps us grow. If you like it, consider giving us a shout-out.

❤️ Share

• X
• Mastodon
• Reddit
• LinkedIn

_{Comment @coderabbitai help to get the list of available commands.}

[chatgpt-codex-connector]

💡 Codex Review

Here are some automated review suggestions for this pull request.

Reviewed commit: 99c067f8ac

ℹ️ About Codex in GitHub

Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you

• Open a pull request for review
• Mark a draft as ready
• Comment "@codex review".

If Codex has suggestions, it will comment; otherwise it will react with 👍.

Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".

[chatgpt-codex-connector]

Register the decomposition theorems in the checker

Neither this public theorem nor the following integral_continuousTrajectoryCountableSleeping_activeLogValue theorem has a #check or #print axioms entry in examples/CheckContinuousMeasurableTrajectoryCountableSleepingStrategyOrdinaryRiskPACBayes.lean. As a result, example verification does not guard these newly exported score-decomposition bridges against signature or axiom-set regressions; add both declarations to the checker and confirm the sanctioned public axiom set.

AGENTS.md reference: AGENTS.md:L54-L59

Useful? React with 👍 / 👎.