Comment on "General relativistic statistical mechanics"

This record contains the English and Japanese versions of Comment on “General relativistic statistical mechanics”, together with accompanying Isabelle/HOL proof sources. The Comment examines the classical thermal-time construction in Carlo Rovelli’s General relativistic statistical mechanics, Physical Review D 87, 084055 (2013), https://doi.org/10.1103/PhysRevD.87.084055. 本レコードには、『General relativistic statistical mechanics』へのCommentの英語版・日本語版と、Isabelle/HOLによる証明ソースを収録します。このCommentは、Carlo Rovelliの論文 General relativistic statistical mechanics(Physical Review D 87, 084055、2013年)における古典的な熱時間構成を検討します。対象論文:https://doi.org/10.1103/PhysRevD.87.084055 Abstract Rovelli's 2013 proposal assigns a preferred time flow to each statistical state. This Comment shows that the classical construction does not generally supply the stationary ensemble evolution required to infer equilibrium time from the state. The counterexample is a smooth, everywhere positive, normalized state whose thermal-flow domain has probability less than one at every nonzero flow parameter. The state satisfies infinitesimal stationarity and admits a constrained realization of the local Gibbs relation. The associated canonical family has finite partition functions, mean energies, and energy variances at every positive inverse temperature. Nevertheless, specified bounded smooth observables have undefined temporal correlations. Restricting the integration domain gives a unit-observable correlation below one. For finite-dimensional thermal flows, almost-everywhere two-sided completeness is equivalent to a full-probability domain at one, and hence every, nonzero parameter; imposing it restricts the admissible states. For the counterexample, neither nontrivial autonomous Hamiltonians preserving the density on its original symplectic space nor positive-power temperature changes restore completeness. Periodic and reflecting completions preserve the initial distribution but produce different correlations through additional boundary rules. Density modifications arbitrarily small in L1 restore completeness for different states. Thus the state-based inference of equilibrium time lacks a general construction of the required stationary ensemble evolution. A completeness restriction assigns stationary thermal flows on a smaller state class, whereas completing the counterexample's flow introduces predictive data not selected by the state and local generator. 要旨 Rovelli (2013)は、各統計状態に優先的な時間流を対応させる構想を提示する。このCommentは、その古典的構成が、状態から平衡時間を読み取るために必要な全集団の定常発展を一般には与えないことを示す。反例は滑らかで全点で正の正規化状態であり、その熱流の定義域は、どの非零パラメータでも確率1に達しない。この状態は無限小の定常性を満たし、局所Gibbs関係の拘束系による実現を持つ。対応する正準集団の族の分配関数、平均エネルギー、エネルギー分散は、すべての正の逆温度で有限である。それにもかかわらず、具体的に指定した有界で滑らかな観測量の時間相関は未定義となる。積分域を制限すると、単位観測量の相関は1未満になる。有限次元の熱流では、一つの非零パラメータで定義域が確率1を持つことは、ほとんど至るところでの両側完備性と同値であり、その場合はすべての非零パラメータで定義域の確率が1となる。この条件を課すと許容状態が制限される。反例については、元のシンプレクティック空間上で密度を保存する非自明な自律Hamiltonianでも、正冪による温度変更でも、完備性は回復しない。周期補完と反射補完は初期分布を保存するが、追加する境界規則によって異なる相関を与える。L1ノルムで任意に小さい密度の変更は、別の状態について完備性を回復する。したがって、状態から平衡時間を読み取る構想には、その前提となる全集団の定常発展の一般的構成が欠けている。完備性による制限は、より狭い状態クラス上で定常的な熱流を対応させる。一方、反例の流の補完は、状態と局所生成子からは選択されない、予測を左右するデータを導入する。 Comment / コメント論文 The English and Japanese manuscripts contain the same mathematical argument, with corresponding section, proposition and equation numbers. Each contains four propositions, explicit counterexample calculations, analytical proofs and the consequences for Rovelli’s classical state-to-time-flow assignment. 英語版と日本語版は、対応する節・命題・式番号を備え、同じ数学的論証を記述します。四つの命題、反例の具体的計算、解析的証明、およびRovelliの古典的構成における状態から時間流への対応に対する帰結を収録します。 Proof assets / 証明資産 The proof archive contains 24 Isabelle2025-2 theory files in two sessions, session configuration, a README, a verification record and source checksums. Mechanically verified components support Proposition 1 (the smooth positive normalized state and its incomplete thermal flow) and Proposition 4 (probability-preserving endpoint completions with different correlations). In the strip representation, the reflection group law and identity statements hold almost everywhere. The formal correlation witness uses a bounded position observable and a rectangle indicator; the smooth-observable comparison is proved analytically in the article. Propositions 2 and 3 and the additional analytical arguments are proved in the article. 証明ZIPには、Isabelle2025-2の理論ファイル24本、2セッションの設定、README、検証記録、およびソースのチェックサムを収録します。機械検証の対象には、命題1を支える滑らかな正値正規化状態とその不完備な熱流、および命題4を支える異なる相関を与える確率保存的な端点補完が含まれます。帯領域で表した反射の群法則と恒等写像に関する命題は、ほとんど至るところで成立します。形式化された相関の具体例は有界な位置観測量と矩形の指示関数を用い、滑らかな観測量による比較は本文の解析的証明で与えます。命題2・3と追加の解析的論証も本文で証明します。 Document and proof navigation / 文書と証明資産の対応 The archive’s README.md identifies the mechanically verified components, additional formal results and analytical arguments in the Comment, and provides the Isabelle build command. verification.txt records execution and theorem-dependency checks for the supplied sources; sha256.json identifies the theory files and ROOT. ZIP内のREADME.mdは、機械検証された構成要素、追加の形式化結果、およびComment本文の解析的論証を区別して案内し、Isabelleの再実行コマンドを示します。verification.txtには同梱ソースの実行記録と定理依存関係の検査を、sha256.jsonには理論ファイルとROOTの同定情報を収録します。 License scope / ライセンスの適用範囲 The author’s two English and Japanese PDFs, documentation, and audit data are licensed under CC BY-NC-ND 4.0. The author’s verification programs, execution scripts, and formalization code are licensed under BSD-3-Clause. Third-party materials retain their respective copyright notices and license terms. These scopes also apply to the proof archive and its expanded files. 著者による英語・日本語の2PDF、説明文および監査データにはCC BY-NC-ND 4.0を適用します。著者が作成した検証プログラム、実行用スクリプトおよび形式化コードにはBSD-3-Clauseを適用します。第三者資料には、それぞれの著作権表示とライセンスが適用されます。これらの適用範囲は、証明資産のZIPと展開済みファイルにも共通します。