docs: add end-to-end paper draft and literature positioning - #26
Merged
Conversation
… reverse laws The global Crooks, Jarzynski, second-law, and work-distribution relations in Section 5.4 hold for the forward law started from the initial Gibbs state and the reverse law started from the final Gibbs state, matching the Lean theorem statements. Say so explicitly before the central measure identity.
Fix the accent in Étienne Marion's name and complete the Bobbin et al. Digital Discovery entry with the full author list, volume, pages, and DOI (Digital Discovery 3, 264-280, 2024; 10.1039/D3DD00077J).
- Abstract: name the forward and chronology-aligned reverse global laws instead of 'the same global law', and describe the global law as a jump-record law inducing a right-continuous trajectory. - Section 2: state explicitly that all path measures live on the dependent sum of finite jump records, not on a canonical Skorokhod space. - Section 3: add a proof sketch for the telescoping identity behind normalization. - Section 4: add a proof sketch for the renewal-equation uniqueness argument, explain the toReal subscript, and note Mathlib's rightmost-first kernel-composition convention. - Section 5: add the forward/reverse time-mirror schematic, name the transition-then-quench work convention, define withDensity and give the density form of the central identity, restrict 'local' detailed balance to its windowwise meaning, separate the formal beta != 0 theorems from the thermodynamic beta > 0 reading, and explain that the reverse chart is chronology-aligned with W_R = -W by definition. - Section 6: stop Table 1 from breaking declaration names mid-word. - Section 8: soften the positioning statement to a snapshot-bounded 'we did not identify' form (RELATED_WORK.md aligned), and name the AFP Continuous_Time_Markov_Chain theory. - Bibliography: credit the AFP Markov Models entry to Hoelzl and Nipkow (2012) with the accessed snapshot date. - CI: build the manuscript with latexmk+biber in a TeX Live container and upload the PDF; note this in Section 10. - Makefile: fall back to the TeX Live container when latexmk is not installed locally. - Preamble: add emergencystretch, removing the overfull lines in Sections 1 and 8.
Add ContinuousTimeJumpTwoStateInteriorTime.lean: for the symmetric two-state chain over one window of positive duration, the events that a path pinned to the endpoint pair (0,0) sits at state 0, respectively 1, at the interior time T/2 both have positive probability via the finite-dimensional atom formula. Hence the real-time trajectory at the window interior is not almost surely any function of the window's endpoint pair (trajectory_interior_not_ae_endpointFunction). This is the single-window companion of work_not_ae_initialFinalFunction: boundary histories determine driven work, but only complete window paths determine the real-time trajectory.
- state the global Crooks relation as one explicit theorem with its full
hypothesis list, and demote Jarzynski and the average-work second law
to corollaries
- display the record-level time-reversal map and rename the aligned
reverse law to P^glob_{R,align}
- display the first-jump renewal equation and its uniqueness bound in
Section 4.2
- present the measure-level work-distribution Crooks relation before the
atomwise form
- split Section 7's full-path claim into two theorem-backed statements:
window-boundary histories are essential for work, and interior-time
states are not boundary functions (trajectory_interior_not_ae_endpointFunction)
- scope the FullPath carrier statement to single-window and global laws
- rename local Gibbs detailed balance to windowwise Gibbs detailed
balance throughout
- fix the T = 0 edge case in the Table 1 stage-1 label and add the
second-law and work-distribution declarations to stage 6
- cite Lean 4 and Mathlib
…claim strength - Split the artifact statement: core formalization at base commit f96e380, manuscript sources and the interior-time theorem in the artifact commit; release unifies both under one versioned tag and DOI (Sec. 10, ARTIFACT.md, RELATED_WORK.md) - State the diagonal convention k(x,x)=0 so sector densities and the renewal equation are fully defined over unrestricted sums (Sec. 2) - Separate normalized probability from the scaled sector reference in the Table 1 Stage 1 description (Sec. 6) - Weaken 'beyond every boundary history' to the proved general non-determination claim (Sec. 7) - Replace the subscript-R mass-conversion notation with toReal (Sec. 4) - Clarify the 'equivalently' in the Gibbs detailed-balance assumption and cover the M=0 degenerate protocol and finite-window boundedness (Sec. 5) - Audit trajectory_interior_not_ae_endpointFunction in AxiomAudit.lean
- Unify the atomwise Crooks relation notation to the chronology-aligned
reverse law P_{R,align}^{glob} (Sec. 5)
- Restate the interior-time consequence as insufficiency of endpoint-only
records instead of necessity of complete paths (Sec. 7)
- Describe n-jump sectors as records and note that degenerate records are
null under the sector laws (Sec. 2)
- Qualify the embedded jump chain away from absorbing states (Sec. 1)
- Smooth the Gibbs detailed-balance equivalence sentence and add the
record-level time-reversal convention against pointwise reversal (Sec. 5)
- Cite the reverseWork work-distribution declaration matching Eq. (16) in
Table 1, split across lines to fit the cell (Sec. 6)
- Align the CI description with the workflow implementation (Sec. 6)
- Recast the publication paragraph in an academic register (Sec. 9)
…-zero assumption Address the third external review round. - Add pathLawFrom_finiteDimensional_eq_general and pathLawFrom_sampleAt_real_singleton_eq_exp_product_general: sampling at any monotone observation family, not necessarily starting at zero, gives the chronological kernel chain started from the time-t0 marginal, with atoms exp(t0 Q)(x, x0) times the usual matrix-exponential product; audit both (propext, Classical.choice, Quot.sound only) - Cite the general form in Sec. 4.3 and FORMALIZATION.md, so the abstract's every-finite-dimensional-marginal claim is fully machine-checked - Display the reverse protocol's intrinsic switching work in its own chronology and cite reverseWork_eq_neg for W_R = -W (Sec. 5) - Recast the windowwise-vs-local detailed-balance comparison as a naming clarification, not a weaker-condition claim (Sec. 5), and unify RELATED_WORK.md terminology to windowwise Gibbs detailed balance - State the interior-time example with positive-probability and almost-surely wording (Sec. 7)
Apply the physics-reader review: lead the abstract and introduction with the stochastic-thermodynamics payoff, condense the contributions to three physics-facing items, state the inclusive work convention and protocol endpoints explicitly, present normalized Gibbs detailed balance before the division-free Lean form, introduce the chronology-aligned reverse law as P_R^Theta, put the physicists' Crooks form before the withDensity identity with the dissipated-work interpretation, add verified concrete probabilities and generators to every example, record the odd-variable and heat/first-law scope limits, and add the standard references (Seifert 2012, Sekimoto 2010, Van den Broeck-Esposito 2015, Maes 2021, Spinney-Ford 2012).
…view Restrict the average-work inequality to positive inverse temperature in the abstract, contribution list, and Section 5; state that the reverse window path is reversed exactly once before storage so the marked reverse law is already chronology-aligned (reverseWindowKernel), and mark the transported reverse-work symbol explicitly; add the T > 0 hypothesis to the interior-time joint masses; describe condition (12) as the single-bath equilibrium specialization of local detailed balance instead of denying the connection; soften the cadlag-reversal remark to an informal correspondence.
…ks example - Open abstract and introduction with the trajectory-vs-master-equation identity question; move repository-wide scope to the artifact section - Add trajectory-level cancellation paragraph linking the measure identity to the standard stochastic-thermodynamics derivation - Present standard cadlag time reversal before the record-level implementation; state the reverse quench as the time mirror - Rename: Path-space Crooks relation, Crooks work-distribution relation, end-of-window quench convention; replace 'instantaneous detailed balance' with ordinary generator detailed balance language - Clarify F_M as final-landscape equilibrium free energy; state beta range interpretation at first use; add row-vector master-equation convention - Give physical-time renewal equation before the residual-fraction form - Add reverse work distribution and atomwise Crooks check to the two-state quench example; reframe Y-network and interior-time examples - Add KL dissipated-work remark (marked as unmechanized interpretation) - Cite Gardiner and Kawai-Parrondo-Van den Broeck
…identities - ContinuousTimeJumpTrajectoryReversal: record reversal realizes the cadlag time mirror of the right-continuous trajectory, pointwise off jump times on exact-horizon records, almost surely at each fixed time under sectorLawFrom/pathLawFrom, and for all finite-dimensional evaluations (map_trajectory_reverse_eq_map_mirror) - ContinuousTimeJumpDrivenKL: under the global Crooks hypotheses, the aligned reverse law is the forward law tilted by dissipated work, the log-likelihood ratio equals beta*(W - dF) forward-a.s., and for beta>0 klDiv(P_F, P_R^Theta) equals the mean dissipated work - Register both files in root imports and the driven axiom audit; all new theorems depend only on propext, Classical.choice, Quot.sound
…uscript - Replace the informal record-vs-cadlag hedge in Section 5.1 with the machine-checked mirror theorems (pointwise, almost-sure fixed-time, and windowwise finite-dimensional) - Upgrade the KL dissipated-work remark from unmechanized interpretation to the mechanized llr/klDiv theorems - Record the remaining global arbitrary-time mirror statement as a limitation - Extend the FORMALIZATION.md map with the six new declarations
kiyo-e
marked this pull request as ready for review
August 29, 2026 09:29
Codex Review SummaryThis comment shows the latest Codex review activity on this pull request.
ℹ️ About Codex in GitHubYour team has set up Codex to review pull requests in this repo. Reviews are triggered when you
Codex reacts with 👀 while any review is running, comments if it has suggestions, and reacts with 👍 once all reviews finish with no findings. |
![chatgpt-codex-connector[bot]](https://avatars.githubusercontent.com/in/1144995?s=60&v=4){kind=small}
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 85abc76f0a
ℹ️ 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".
- Answer the opening question immediately (compatibility is standard; the contribution is the machine-checked construction) and reword the abstract so no physical gap is implied - State the main physical result as a Radon-Nikodym identity at the end of the introduction; reorder contributions physics-first - Call the reverse law the chronology-aligned law from windowwise record reversal in the abstract; state the reverse quench as the time mirror of the forward schedule - Add heat Q_sys and the first law to the trajectory-level cancellation (marked as unformalized interpretation); rename the work convention evolve-then-quench - Name the balance condition equilibrium detailed balance and exhibit the adjoint rates k-dagger = k - Distinguish the energy schedule from the kinetic schedule and scope the thermodynamic bookkeeping - Replace the ratio-notation hedge with mutual absolute continuity and an explicit Radon-Nikodym derivative - Reduce software vocabulary in physics sections; add the row-notation reading of the kernel semigroup law - Two-state example: explain the energy gauge and the shifted-gauge values; three-state protocol: fully specify generators, initial state, and durations in the text; interior-time example: lead with the conditional midpoint probability - Cite Maes-Netocny and Spinney-Ford at the time-reversal definition and Crooks/Seifert at the KL identity
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 3b6322e9e7
ℹ️ 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".
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.
Direction
Positions the continuous-time result as the verified end-to-end connection from finite-state jump generators to global Crooks–Jarzynski laws, without broad priority claims.
Added
Review response
An external manuscript review was addressed in full:
P^glob_{R,align}trajectory_interior_not_ae_endpointFunction(ContinuousTimeJumpTwoStateInteriorTime.lean) proves that interior-time states are not functions of the endpoint pairFullPathcarrier statement is scoped precisely; the stage-1 table label handles theT = 0edge case; Lean 4 and Mathlib are citedValidation
makeinpaper/succeeds inside the CI TeX Live container withlatexmkandbiberlake build CrooksJarzynskisucceeds; the new theorem depends only onpropext,Classical.choice, andQuot.soundBefore submission