Physics

Download original file

This is the original source text. Reading it does not run or verify the program.

Read the typeset paper

1 {
2   "cache_resolution_sha256": "0d4ac1229d05e491a82d716c0a23e5e177918ce770234a518d3def92e7376f48",
3   "commands": 64,
4   "commands_sha256": "a6034bbd1461925300a7acbe466e0083e0ec74ddef58ae9c9a45dc072c18d801",
5   "compile_order": [
6     "KomorebiPhysics.RelativisticPauli",
7     "KomorebiPhysics.InvolutionExponential",
8     "KomorebiPhysics.DiracWalk1D",
9     "KomorebiPhysics.Dispersion1D",
10     "KomorebiPhysics.Relativistic1DGroupVelocity",
11     "KomorebiPhysics.Relativistic1DShellAsymptotics",
12     "KomorebiPhysics.Relativistic1DAsymptoticAlgebra",
13     "KomorebiPhysics.Relativistic1DAsymptoticExamples",
14     "KomorebiPhysics.Relativistic1DContinuumLimit",
15     "KomorebiPhysics.Relativistic3DCliffordTransportU1",
16     "KomorebiPhysics.Relativistic3DFourierGenerator",
17     "KomorebiPhysics.Relativistic3DFourierL2Generator",
18     "KomorebiPhysics.Relativistic3DFourierPropagator",
19     "KomorebiPhysics.LocalDiscreteGlobalContinuum",
20     "KomorebiPhysics.Relativistic3DCliffordHilbertRefinement",
21     "KomorebiPhysics.Relativistic3DFourierHilbertStability",
22     "KomorebiPhysics.Relativistic3DFourierCompactTime",
23     "KomorebiPhysics.Relativistic3DFullFourierEvolution",
24     "KomorebiPhysics.Relativistic3DTorusFourierEvolution",
25     "KomorebiPhysics.Relativistic3DUnboundedDirac",
26     "KomorebiPhysics.Relativistic3DWeightedDiracDomain",
27     "KomorebiPhysics.Relativistic3DGeneratorBridge",
28     "KomorebiPhysics.Relativistic3DCenteredConvergence",
29     "KomorebiPhysics.Relativistic3DModalPerturbation",
30     "KomorebiPhysics.Relativistic3DCenteredRates",
31     "KomorebiPhysics.Relativistic3DCenteredResolvent"
32   ],
33   "control_counts": {
34     "elaboration_reject": 12,
35     "policy_reject": 1,
36     "positive": 8
37   },
38   "control_objects_sha256": "b497e0fdf16ca102d0ead17710af5abddf8ae1f6d9211b5b85e4abdb64a42c6b",
39   "controls_manifest_sha256": "0d53bad691e3770b8dff0178599fda77d36e717e406f9e3c4567d4caebe73873",
40   "declarations": 209,
41   "declarations_sha256": "db6ae9c262568dedd54c2ccdac7102cca8848ceabeae18c59aebec82269de156",
42   "dependency_revisions": {
43     "Cli": "ab3a82db9fea14cf0fd7f5a2de650f4b534640af",
44     "LeanSearchClient": "ba67e212be1197b84c1f1f6299488a10a3002713",
45     "Qq": "507746ab8f4b643ccdacb2ec4cdb5853fa9f8ab3",
46     "aesop": "18889deb9e83ea7420ef51c160d6f88552e744e3",
47     "batteries": "4cac2177c37f5530c4da76aa8e4307f3fc9e4dcb",
48     "importGraph": "d8823026ac7ef130c253089d95685f9877b95323",
49     "mathlib": "aeb72f1e9981b6d35b426b16dca7759be3e7ba06",
50     "plausible": "d9598f07b1bc701f1e3aae163d2681c1fd978793",
51     "proofwidgets": "a8acbfd87375ff4abe14ce09db5b7664d383bc7f"
52   },
53   "direct_external_imports": [
54     "Mathlib.Algebra.BigOperators.Fin",
55     "Mathlib.Algebra.BigOperators.Group.Finset.Basic",
56     "Mathlib.Analysis.Asymptotics.AsymptoticEquivalent",
57     "Mathlib.Analysis.Asymptotics.Ring",
58     "Mathlib.Analysis.CStarAlgebra.Basic",
59     "Mathlib.Analysis.CStarAlgebra.ContinuousLinearMap",
60     "Mathlib.Analysis.CStarAlgebra.Spectrum",
61     "Mathlib.Analysis.Calculus.Deriv.Slope",
62     "Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas",
63     "Mathlib.Analysis.Calculus.MeanValue",
64     "Mathlib.Analysis.Calculus.Taylor",
65     "Mathlib.Analysis.Complex.Circle",
66     "Mathlib.Analysis.Complex.Trigonometric",
67     "Mathlib.Analysis.Fourier.AddCircleMulti",
68     "Mathlib.Analysis.InnerProductSpace.Adjoint",
69     "Mathlib.Analysis.InnerProductSpace.LinearPMap",
70     "Mathlib.Analysis.InnerProductSpace.PiL2",
71     "Mathlib.Analysis.InnerProductSpace.l2Space",
72     "Mathlib.Analysis.Normed.Algebra.Exponential",
73     "Mathlib.Analysis.Normed.Algebra.MatrixExponential",
74     "Mathlib.Analysis.Normed.Group.Bounded",
75     "Mathlib.Analysis.Normed.Group.Tannery",
76     "Mathlib.Analysis.Normed.Lp.lpSpace",
77     "Mathlib.Analysis.SpecialFunctions.Exponential",
78     "Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds",
79     "Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv",
80     "Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse",
81     "Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv",
82     "Mathlib.Analysis.SpecialFunctions.Trigonometric.Sinc",
83     "Mathlib.Data.Fin.VecNotation",
84     "Mathlib.Data.Fintype.Basic",
85     "Mathlib.Data.Fintype.BigOperators",
86     "Mathlib.Tactic.FinCases",
87     "Mathlib.Tactic.Group",
88     "Mathlib.Tactic.Module",
89     "Mathlib.Tactic.NoncommRing",
90     "Mathlib.Tactic.NormNum",
91     "Mathlib.Tactic.Ring",
92     "Mathlib.Topology.Algebra.InfiniteSum.Real"
93   ],
94   "effective_environment": {
95     "LD_PRELOAD": "/workspace/scratch/6a8ff46cf015/physics_next/runtime/Komorebi_Portable_Lean_4.34.0-rc2/compat/app_path.so",
96     "LEAN_NUM_THREADS": "1",
97     "LEAN_PATH": "/workspace/scratch/6a8ff46cf015/physics_next/verification/centered_run02/objects:/workspace/scratch/6a8ff46cf015/physics_next/runtime/Komorebi_Portable_Lean_4.34.0-rc2/workspace/.lake/packages/mathlib/.lake/build/lib/lean:/workspace/scratch/6a8ff46cf015/physics_next/runtime/Komorebi_Portable_Lean_4.34.0-rc2/workspace/.lake/packages/plausible/.lake/build/lib/lean:/workspace/scratch/6a8ff46cf015/physics_next/runtime/Komorebi_Portable_Lean_4.34.0-rc2/workspace/.lake/packages/LeanSearchClient/.lake/build/lib/lean:/workspace/scratch/6a8ff46cf015/physics_next/runtime/Komorebi_Portable_Lean_4.34.0-rc2/workspace/.lake/packages/importGraph/.lake/build/lib/lean:/workspace/scratch/6a8ff46cf015/physics_next/runtime/Komorebi_Portable_Lean_4.34.0-rc2/workspace/.lake/packages/proofwidgets/.lake/build/lib/lean:/workspace/scratch/6a8ff46cf015/physics_next/runtime/Komorebi_Portable_Lean_4.34.0-rc2/workspace/.lake/packages/aesop/.lake/build/lib/lean:/workspace/scratch/6a8ff46cf015/physics_next/runtime/Komorebi_Portable_Lean_4.34.0-rc2/workspace/.lake/packages/Qq/.lake/build/lib/lean:/workspace/scratch/6a8ff46cf015/physics_next/runtime/Komorebi_Portable_Lean_4.34.0-rc2/workspace/.lake/packages/batteries/.lake/build/lib/lean:/workspace/scratch/6a8ff46cf015/physics_next/runtime/Komorebi_Portable_Lean_4.34.0-rc2/toolchain/lib/lean",
98     "PATH": "/workspace/scratch/6a8ff46cf015/physics_next/runtime/Komorebi_Portable_Lean_4.34.0-rc2/toolchain/bin:/root/.codex/tmp/arg0/codex-arg02ZxhjU:/opt/codex/codex-path:/opt/codex/runtimes/codex-primary-runtime/dependencies/bin/override:/opt/codex/runtimes/codex-primary-runtime/dependencies/python/bin:/opt/codex/runtimes/codex-primary-runtime/dependencies/node/bin:/opt/codex/runtimes/codex-primary-runtime/dependencies/bin:/usr/local/sbin:/usr/local/bin:/usr/sbin:/usr/bin:/sbin:/bin:/opt/codex/runtimes/codex-primary-runtime/dependencies/bin/fallback"
99   },
100   "finished_utc": "2026-10-26T15:23:13.796108+00:00",
101   "generated_audit_sha256": {
102     "AuditCentered.lean": "a9068facebd3434a57c88a759976c27ad95f2888da1929bce0a1807d1e5ca72a",
103     "PolicyAudit_policy_custom_axiom.lean": "de7e0bad89f22bbcc046f5d13ee3e284bd7a06dfd3ebb227bf645ccfe243e3b2"
104   },
105   "lean_version": "Lean (version 4.34.0-rc2, x86_64-unknown-linux-gnu, commit 6a10ac8c22beadecabdbb0919c2b50214762f91d, Release)",
106   "local_targets": 26,
107   "missing_dependency_build_directories": [
108     {
109       "dependency": "Cli",
110       "path": "/workspace/scratch/6a8ff46cf015/physics_next/runtime/Komorebi_Portable_Lean_4.34.0-rc2/workspace/.lake/packages/Cli/.lake/build/lib/lean",
111       "present": false
112     }
113   ],
114   "new_declarations": 162,
115   "new_modules": [
116     "KomorebiPhysics.Relativistic3DCenteredConvergence",
117     "KomorebiPhysics.Relativistic3DModalPerturbation",
118     "KomorebiPhysics.Relativistic3DCenteredRates",
119     "KomorebiPhysics.Relativistic3DCenteredResolvent"
120   ],
121   "objects_unchanged": true,
122   "production_objects_sha256": "e1a60e1233a88e050bb1bc607a18b17714d2dc14ad0c92bf55dd5d6baf51d754",
123   "relevant_runtime_unchanged": true,
124   "root_modules": [
125     "KomorebiPhysics.Relativistic3DGeneratorBridge",
126     "KomorebiPhysics.Relativistic3DCenteredConvergence",
127     "KomorebiPhysics.Relativistic3DModalPerturbation",
128     "KomorebiPhysics.Relativistic3DCenteredRates",
129     "KomorebiPhysics.Relativistic3DCenteredResolvent"
130   ],
131   "runner_sha256": "2ae5b2e524b3a7527b4a762bc6914296dc06e90ee11056fba6eaaf6c7a1eaa26",
132   "runtime_after_sha256": "05abc1a7aa5e9276c664c77708f16eb94484041cbc53bcb73f2c18c785f1db76",
133   "runtime_before_sha256": "53f9c1e8c6e557d6c012369700fccf5211d0c056a18b77ad3cb66f9cf23da61b",
134   "runtime_manifest_sha256": "3d038009d119676dd1e61146556da63379bccbf2ae89fac6e33f1efa147e8f05",
135   "schema": "komorebi.physics.centered-gate.v1",
136   "source_input_count": 52,
137   "source_inputs_sha256": "515c933f79bc4f1be5e4607b57a1ebbda3a7035936b38b6b75b7c48181da8d24",
138   "source_sha256": {
139     "CONTROL_MANIFEST.json": "0d53bad691e3770b8dff0178599fda77d36e717e406f9e3c4567d4caebe73873",
140     "KomorebiPhysics/DiracWalk1D.lean": "5dd1d0f5604d83858efc522ca03a98255213152d67dc94e657d839db57000b99",
141     "KomorebiPhysics/Dispersion1D.lean": "c3be87ac176f7ef8e9b3783bbebe31f8f8e9cd3193f3ef142e24a76f4f5fdc66",
142     "KomorebiPhysics/InvolutionExponential.lean": "624bacc199153516730979bf416fdf68fd31c8e3dd7d3dbda90e21f8048bf5a5",
143     "KomorebiPhysics/LocalDiscreteGlobalContinuum.lean": "da988b22392bf7e4c630f1771f8486ad2d0cd7f49d07c62a8e7f535c3ef0312a",
144     "KomorebiPhysics/Relativistic1DAsymptoticAlgebra.lean": "2c545f1e84b66196cb698ea157c0b293a3e5f451a8dae13938c74dfd3ea1f225",
145     "KomorebiPhysics/Relativistic1DAsymptoticExamples.lean": "ed4801e541a943d174283d84f276e8ffb2b767b7e07f904fb7b1d000883ffeb4",
146     "KomorebiPhysics/Relativistic1DContinuumLimit.lean": "de26c3c61fa83eb95bb8f355ee3d8cd532e358d5c5bc207ec01c2e15c5efcf2b",
147     "KomorebiPhysics/Relativistic1DGroupVelocity.lean": "bddd40f29293fd70b44e0a10b5d5f9c6e5b184684b95fbcc0d5f0a0b8920c0d6",
148     "KomorebiPhysics/Relativistic1DShellAsymptotics.lean": "58187ec6ba7de6b91fc060011a93bda466ecd10f804b650e8c6ea3824ad12112",
149     "KomorebiPhysics/Relativistic3DCenteredConvergence.lean": "db4cd13a2700dbaf180bf39d874bb32bc226e339e69cab52bdbf455f363a00ff",
150     "KomorebiPhysics/Relativistic3DCenteredRates.lean": "30b1f44184da49cdd84851b84f0c08bd7bed362587de1268c2acb5adc4b65e27",
151     "KomorebiPhysics/Relativistic3DCenteredResolvent.lean": "937d369dc7ccc5c1bfb337d5fc4e13b3ffbb93536e04634f650714fe8b8bc909",
152     "KomorebiPhysics/Relativistic3DCliffordHilbertRefinement.lean": "78946f3d2539566a34e16a7070358cb434fb376af06e7e36a55305c3a3f7fe60",
153     "KomorebiPhysics/Relativistic3DCliffordTransportU1.lean": "52288e2f60a23a3315ceaa2e1c13ef52d15a25bb64ca07c29dbedb73a415d403",
154     "KomorebiPhysics/Relativistic3DFourierCompactTime.lean": "a01a296635f654bfb8513126a6d1070a2b3ded92821c59d0df8a71909daacc5c",
155     "KomorebiPhysics/Relativistic3DFourierGenerator.lean": "c95f12cddda5f9264789083259f3a785a52920a059d99924a7a82674f110a7e3",
156     "KomorebiPhysics/Relativistic3DFourierHilbertStability.lean": "62e4115ce90bb381a66237201754b75fc36d79684e8bdaea9e5a6cdb580f41b9",
157     "KomorebiPhysics/Relativistic3DFourierL2Generator.lean": "ae82e909419a33951f746ab93b3343af25304d4a6b5431083b91dbd1720258cf",
158     "KomorebiPhysics/Relativistic3DFourierPropagator.lean": "f8f16f9983fbc4087f4e57b90079971f39ce5fec1fea94561d878639517d19be",
159     "KomorebiPhysics/Relativistic3DFullFourierEvolution.lean": "186373e1aebd7a142199bfd5d769e973dfc47fa4258b5c7a01d8d3e271b2cc46",
160     "KomorebiPhysics/Relativistic3DGeneratorBridge.lean": "ee721cc3ab78f500bab87c1edb358be8b30a0892e7047c9e9cb5aa31a6d51499",
161     "KomorebiPhysics/Relativistic3DModalPerturbation.lean": "9e40e93c9f5a8acfa26c9b5b0047e86032641d91981ff7fbf2d81f14594bf793",
162     "KomorebiPhysics/Relativistic3DTorusFourierEvolution.lean": "cc429b40249be41d2d57c3a9b385ace82931d781cb011d8853fced7e3ddb3bcd",
163     "KomorebiPhysics/Relativistic3DUnboundedDirac.lean": "15f4fa4ddc655dce7950106ce1eb96ba4c34fb4758e4f81b15c219cc2d554858",
164     "KomorebiPhysics/Relativistic3DWeightedDiracDomain.lean": "cb31264d89d6a57a230ad4d6765937b140c84ee87f43e73dbfaff0d0cfaa09e5",
165     "KomorebiPhysics/RelativisticPauli.lean": "ec4f5cc14285082f380a0ee4174403f4718cef854f37b33aea4dac43e39114c3",
166     "lake-manifest.json": "2ba2018e7b8400a7d83c028a312111c629c07f4c882b03f1d303340c78d6f218",
167     "lakefile.toml": "5b0a4db8f9fadf9b504a1a6f8775b8b6a518d5847b385236d8dd62f530ef02bb",
168     "lean-toolchain": "8190e75a201741065fe508b28955dd64dd72d090babe5f70ce6848879d68ae88",
169     "negative_controls/block51/centered/MissingGraphDomain.lean": "763e4c941e2438406a2ad2974174c932ffc3bac89cbbeaf647d7db6ea12c57a4",
170     "negative_controls/block51/centered/MissingSpacingBound.lean": "e17c537d587c70c3f49206d21afcea75192579b17c508f1165e9e740c6254c69",
171     "negative_controls/block51/centered/MissingSpacingEvaluation.lean": "7fa0634c0751d2419c6280c4364868ccdb919123f07af4b3c433598a60293e4a",
172     "negative_controls/block51/centered/UnpuncturedGraph.lean": "0a21bb14e446e817ce2eaa59cce6fd95bfbd33bfb46a5828b877af2f4e1da7fc",
173     "negative_controls/block51/policy/CustomAxiom.lean": "62efa7147e40b908e623e3609f93e95cbbbe86a8864183dbd0d2eb89f04a7dc6",
174     "negative_controls/block51/policy/Placeholder.lean": "a9d36d3ffb238ca00b7eef00e51caba08c7bf5b4835f5c3b944bbf373bbfa1c9",
175     "negative_controls/block51/rates/MissingMoment.lean": "52f65e6dc0506f364fcf217b5f1ce9e8bbbe70545364aa08c2bd3b0c320106e0",
176     "negative_controls/block51/rates/MissingSpacing.lean": "2620791442e48c39f0c41c471213bd40c71b95ddf9f5407ae3a499f55b362605",
177     "negative_controls/block51/rates/SignedTime.lean": "bee9ce46bb48c813f79b6d68f6f6d4721279d67cb6e0beb60b09c1e5d0f8bae0",
178     "negative_controls/block51/resolvent/MissingNonrealHypothesis.lean": "cb38b2e473cd5ee5497368d0faf66698f908e47960280b6a35141c1226d8a233",
179     "negative_controls/block51/resolvent/RealParameter.lean": "0c3f5e8f32e473dab265f8821cdb81099e527e0191a3a862668b6b429aaed2b7",
180     "negative_controls/block51/resolvent/WrongShiftSign.lean": "e7773f6bc3314f2c1960179b639f1062c62dd362771d3ff1c577de4eedf92e2b",
181     "negative_controls/block51/resolvent/ZeroSpacingInverse.lean": "8ee26e8349686c0799802dc859329dbda2b920bb61185faf4dd3f40c689305bf",
182     "positive_controls/block51/centered/NegativeMassSpacing.lean": "dcc6768766e10f6a4e154f7b004a888e8688fabba0bfe86996209216d5288da3",
183     "positive_controls/block51/centered/PhysicalGraph.lean": "62cab1ccab4459bbcd6d49ad8b78730011b31fa0551cba3c3d0075c5b8cfaafe",
184     "positive_controls/block51/centered/ZeroMode.lean": "5179eea7e4d0b565e82277a8d404c0193d53f4ad009f7a1997636dae2b7fc4df",
185     "positive_controls/block51/rates/FiniteField.lean": "1aee67da3e98e7056c018ed23ad5f21c26901f68a2effbeef1e50bc07a1610ef",
186     "positive_controls/block51/rates/SignedAndModal.lean": "b2f9d54d9490294e7298f1f33644ed27c80fe56056a1dbcd8b97a9e8424c522e",
187     "positive_controls/block51/resolvent/LowerHalfPlanePhysical.lean": "01cc6e47bab494dd04c2669c16f3309cb17e6287bb15ffb0fe27131b7ed0dc6d",
188     "positive_controls/block51/resolvent/ShiftedNonrealParameter.lean": "1f53ee097faabb3af99eeaa83307f8557a479c700f66e28f2d8261b4dcb4b31e",
189     "positive_controls/block51/resolvent/UpperHalfPlane.lean": "b12dfc67608ce941c9e81a9e0bad28acc389114845f5bf2e42bbb7c8e44d796b",
190     "runner/verify_centered.py": "2ae5b2e524b3a7527b4a762bc6914296dc06e90ee11056fba6eaaf6c7a1eaa26"
191   },
192   "source_unchanged": true,
193   "started_utc": "2026-10-26T15:15:14.974693+00:00",
194   "status": "PASS_SCOPED_CENTERED_EXTENSION",
195   "trust_boundary": "Fresh local import closure compiled from exact sources; pinned compiled external dependencies reused. Module leanchecker replay uses the same Lean kernel and imported environment. Mutable dependency Git indexes are excluded from runtime source/cache identity. Not a compiler or Mathlib rebuild, independent kernel, full historical physics certification, finite-grid theorem, interacting physics or cosmological validation."
196 }

Back to source controls

Back to Physics