From 329a291b5f23087a90d4ae80808384198d8cb094 Mon Sep 17 00:00:00 2001 From: "lean-agent-app[bot]" Date: Fri, 17 Jul 2026 11:45:43 +0000 Subject: [PATCH] =?UTF-8?q?Agent:=20Remove=20`isCausalTrip=5Fof=5FisTrip`?= =?UTF-8?q?=20from=20chronological-implies-causal=20lemma=E2=80=A6?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Drop the no-longer-present Lean name from the `\lean{...}` list to fix the blueprint-to-Lean cross-reference that was causing the merge to fail. Blueprint: aqft-in-lean Repository: physicslib/physicslib4 Agent job: 4891d230-3a08-4fcc-aca1-a0bb3cd3e452 Conversation: 8c3f8f53-54fb-4b75-a25c-1a20a5ce2abf --- blueprint/src/sections/sec10/10-2_spacetime.tex | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/blueprint/src/sections/sec10/10-2_spacetime.tex b/blueprint/src/sections/sec10/10-2_spacetime.tex index bcde896..41babb4 100644 --- a/blueprint/src/sections/sec10/10-2_spacetime.tex +++ b/blueprint/src/sections/sec10/10-2_spacetime.tex @@ -308,7 +308,7 @@ \section{Spacetime}\label{sctn:spacetime} \begin{lemma}[Chronological Precedence Implies Causal Precedence] \label{lmm:chronological-implies-causal} - \lean{Physicslib4.Spacetime.isCausal_of_isTimelike, Physicslib4.Spacetime.isCausalTrip_of_isTrip, Physicslib4.Spacetime.causallyPrecedes_of_chronologicallyPrecedes, Physicslib4.Spacetime.chronologicalFuture_subset_causalFuture, Physicslib4.Spacetime.chronologicalPast_subset_causalPast} + \lean{Physicslib4.Spacetime.isCausal_of_isTimelike, Physicslib4.Spacetime.causallyPrecedes_of_chronologicallyPrecedes, Physicslib4.Spacetime.chronologicalFuture_subset_causalFuture, Physicslib4.Spacetime.chronologicalPast_subset_causalPast} \leanfile{Physicslib4/Spacetime/Causality.lean} \leanok \uses{def:trip, def:causal-trip, def:chronological-future-and-chronological-past, def:causal-future-and-causal-past}