1. Physlib
  2. QFT
  3. PerturbationTheory
  4. FieldSpecification
  5. TimeOrder
Imports
/- Copyright (c) 2025 Joseph Tooby-Smith. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Joseph Tooby-Smith -/ module public import Physlib.QFT.PerturbationTheory.FieldSpecification.CrAnSection public import Physlib.QFT.PerturbationTheory.FieldSpecification.NormalOrder import all Mathlib.Data.List.Sort

Time ordering of states

@[expose] public section

Time ordering for states

The time ordering relation on states. We have that timeOrderRel φ0 φ1 is true if and only if φ1 has a time less-then or equal to φ0, or φ1 is a negative asymptotic state, or φ0 is a positive asymptotic state.

def timeOrderRel : 𝓕.FieldOp → 𝓕.FieldOp → Prop | FieldOp.outAsymp _, _ => True | FieldOp.position φ0, FieldOp.position φ1 => φ1.2 (Sum.inl 0) ≤ φ0.2 (Sum.inl 0) | FieldOp.position _, FieldOp.inAsymp _ => True | FieldOp.position _, FieldOp.outAsymp _ => False | FieldOp.inAsymp _, FieldOp.outAsymp _ => False | FieldOp.inAsymp _, FieldOp.position _ => False | FieldOp.inAsymp _, FieldOp.inAsymp _ => True

Time ordering is total.

instance : Std.Total 𝓕.timeOrderRel where total a b := 𝓕:FieldSpecificationa:𝓕.FieldOpb:𝓕.FieldOp⊢ timeOrderRel a b ∨ timeOrderRel b a 𝓕:FieldSpecificationb:𝓕.FieldOpa✝:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentum⊢ timeOrderRel (FieldOp.inAsymp a✝) b ∨ timeOrderRel b (FieldOp.inAsymp a✝)𝓕:FieldSpecificationb:𝓕.FieldOpa✝:((f : 𝓕.Field) × 𝓕.PositionLabel f) × SpaceTime⊢ timeOrderRel (FieldOp.position a✝) b ∨ timeOrderRel b (FieldOp.position a✝)𝓕:FieldSpecificationb:𝓕.FieldOpa✝:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentum⊢ timeOrderRel (FieldOp.outAsymp a✝) b ∨ timeOrderRel b (FieldOp.outAsymp a✝) 𝓕:FieldSpecificationb:𝓕.FieldOpa✝:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentum⊢ timeOrderRel (FieldOp.inAsymp a✝) b ∨ timeOrderRel b (FieldOp.inAsymp a✝)𝓕:FieldSpecificationb:𝓕.FieldOpa✝:((f : 𝓕.Field) × 𝓕.PositionLabel f) × SpaceTime⊢ timeOrderRel (FieldOp.position a✝) b ∨ timeOrderRel b (FieldOp.position a✝)𝓕:FieldSpecificationb:𝓕.FieldOpa✝:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentum⊢ timeOrderRel (FieldOp.outAsymp a✝) b ∨ timeOrderRel b (FieldOp.outAsymp a✝) 𝓕:FieldSpecificationa✝¹:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentuma✝:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentum⊢ timeOrderRel (FieldOp.outAsymp a✝¹) (FieldOp.inAsymp a✝) ∨ timeOrderRel (FieldOp.inAsymp a✝) (FieldOp.outAsymp a✝¹)𝓕:FieldSpecificationa✝¹:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentuma✝:((f : 𝓕.Field) × 𝓕.PositionLabel f) × SpaceTime⊢ timeOrderRel (FieldOp.outAsymp a✝¹) (FieldOp.position a✝) ∨ timeOrderRel (FieldOp.position a✝) (FieldOp.outAsymp a✝¹)𝓕:FieldSpecificationa✝¹:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentuma✝:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentum⊢ timeOrderRel (FieldOp.outAsymp a✝¹) (FieldOp.outAsymp a✝) ∨ timeOrderRel (FieldOp.outAsymp a✝) (FieldOp.outAsymp a✝¹) 𝓕:FieldSpecificationa✝¹:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentuma✝:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentum⊢ timeOrderRel (FieldOp.inAsymp a✝¹) (FieldOp.inAsymp a✝) ∨ timeOrderRel (FieldOp.inAsymp a✝) (FieldOp.inAsymp a✝¹)𝓕:FieldSpecificationa✝¹:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentuma✝:((f : 𝓕.Field) × 𝓕.PositionLabel f) × SpaceTime⊢ timeOrderRel (FieldOp.inAsymp a✝¹) (FieldOp.position a✝) ∨ timeOrderRel (FieldOp.position a✝) (FieldOp.inAsymp a✝¹)𝓕:FieldSpecificationa✝¹:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentuma✝:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentum⊢ timeOrderRel (FieldOp.inAsymp a✝¹) (FieldOp.outAsymp a✝) ∨ timeOrderRel (FieldOp.outAsymp a✝) (FieldOp.inAsymp a✝¹)𝓕:FieldSpecificationa✝¹:((f : 𝓕.Field) × 𝓕.PositionLabel f) × SpaceTimea✝:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentum⊢ timeOrderRel (FieldOp.position a✝¹) (FieldOp.inAsymp a✝) ∨ timeOrderRel (FieldOp.inAsymp a✝) (FieldOp.position a✝¹)𝓕:FieldSpecificationa✝¹:((f : 𝓕.Field) × 𝓕.PositionLabel f) × SpaceTimea✝:((f : 𝓕.Field) × 𝓕.PositionLabel f) × SpaceTime⊢ timeOrderRel (FieldOp.position a✝¹) (FieldOp.position a✝) ∨ timeOrderRel (FieldOp.position a✝) (FieldOp.position a✝¹)𝓕:FieldSpecificationa✝¹:((f : 𝓕.Field) × 𝓕.PositionLabel f) × SpaceTimea✝:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentum⊢ timeOrderRel (FieldOp.position a✝¹) (FieldOp.outAsymp a✝) ∨ timeOrderRel (FieldOp.outAsymp a✝) (FieldOp.position a✝¹)𝓕:FieldSpecificationa✝¹:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentuma✝:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentum⊢ timeOrderRel (FieldOp.outAsymp a✝¹) (FieldOp.inAsymp a✝) ∨ timeOrderRel (FieldOp.inAsymp a✝) (FieldOp.outAsymp a✝¹)𝓕:FieldSpecificationa✝¹:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentuma✝:((f : 𝓕.Field) × 𝓕.PositionLabel f) × SpaceTime⊢ timeOrderRel (FieldOp.outAsymp a✝¹) (FieldOp.position a✝) ∨ timeOrderRel (FieldOp.position a✝) (FieldOp.outAsymp a✝¹)𝓕:FieldSpecificationa✝¹:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentuma✝:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentum⊢ timeOrderRel (FieldOp.outAsymp a✝¹) (FieldOp.outAsymp a✝) ∨ timeOrderRel (FieldOp.outAsymp a✝) (FieldOp.outAsymp a✝¹) All goals completed! 🐙

Time ordering is transitive.

instance : IsTrans 𝓕.FieldOp 𝓕.timeOrderRel where trans a b c := 𝓕:FieldSpecificationa:𝓕.FieldOpb:𝓕.FieldOpc:𝓕.FieldOp⊢ timeOrderRel a b → timeOrderRel b c → timeOrderRel a c 𝓕:FieldSpecificationb:𝓕.FieldOpc:𝓕.FieldOpa✝:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentum⊢ timeOrderRel (FieldOp.inAsymp a✝) b → timeOrderRel b c → timeOrderRel (FieldOp.inAsymp a✝) c𝓕:FieldSpecificationb:𝓕.FieldOpc:𝓕.FieldOpa✝:((f : 𝓕.Field) × 𝓕.PositionLabel f) × SpaceTime⊢ timeOrderRel (FieldOp.position a✝) b → timeOrderRel b c → timeOrderRel (FieldOp.position a✝) c𝓕:FieldSpecificationb:𝓕.FieldOpc:𝓕.FieldOpa✝:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentum⊢ timeOrderRel (FieldOp.outAsymp a✝) b → timeOrderRel b c → timeOrderRel (FieldOp.outAsymp a✝) c 𝓕:FieldSpecificationb:𝓕.FieldOpc:𝓕.FieldOpa✝:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentum⊢ timeOrderRel (FieldOp.inAsymp a✝) b → timeOrderRel b c → timeOrderRel (FieldOp.inAsymp a✝) c𝓕:FieldSpecificationb:𝓕.FieldOpc:𝓕.FieldOpa✝:((f : 𝓕.Field) × 𝓕.PositionLabel f) × SpaceTime⊢ timeOrderRel (FieldOp.position a✝) b → timeOrderRel b c → timeOrderRel (FieldOp.position a✝) c𝓕:FieldSpecificationb:𝓕.FieldOpc:𝓕.FieldOpa✝:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentum⊢ timeOrderRel (FieldOp.outAsymp a✝) b → timeOrderRel b c → timeOrderRel (FieldOp.outAsymp a✝) c 𝓕:FieldSpecificationc:𝓕.FieldOpa✝¹:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentuma✝:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentum⊢ timeOrderRel (FieldOp.outAsymp a✝¹) (FieldOp.inAsymp a✝) → timeOrderRel (FieldOp.inAsymp a✝) c → timeOrderRel (FieldOp.outAsymp a✝¹) c𝓕:FieldSpecificationc:𝓕.FieldOpa✝¹:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentuma✝:((f : 𝓕.Field) × 𝓕.PositionLabel f) × SpaceTime⊢ timeOrderRel (FieldOp.outAsymp a✝¹) (FieldOp.position a✝) → timeOrderRel (FieldOp.position a✝) c → timeOrderRel (FieldOp.outAsymp a✝¹) c𝓕:FieldSpecificationc:𝓕.FieldOpa✝¹:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentuma✝:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentum⊢ timeOrderRel (FieldOp.outAsymp a✝¹) (FieldOp.outAsymp a✝) → timeOrderRel (FieldOp.outAsymp a✝) c → timeOrderRel (FieldOp.outAsymp a✝¹) c 𝓕:FieldSpecificationc:𝓕.FieldOpa✝¹:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentuma✝:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentum⊢ timeOrderRel (FieldOp.inAsymp a✝¹) (FieldOp.inAsymp a✝) → timeOrderRel (FieldOp.inAsymp a✝) c → timeOrderRel (FieldOp.inAsymp a✝¹) c𝓕:FieldSpecificationc:𝓕.FieldOpa✝¹:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentuma✝:((f : 𝓕.Field) × 𝓕.PositionLabel f) × SpaceTime⊢ timeOrderRel (FieldOp.inAsymp a✝¹) (FieldOp.position a✝) → timeOrderRel (FieldOp.position a✝) c → timeOrderRel (FieldOp.inAsymp a✝¹) c𝓕:FieldSpecificationc:𝓕.FieldOpa✝¹:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentuma✝:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentum⊢ timeOrderRel (FieldOp.inAsymp a✝¹) (FieldOp.outAsymp a✝) → timeOrderRel (FieldOp.outAsymp a✝) c → timeOrderRel (FieldOp.inAsymp a✝¹) c𝓕:FieldSpecificationc:𝓕.FieldOpa✝¹:((f : 𝓕.Field) × 𝓕.PositionLabel f) × SpaceTimea✝:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentum⊢ timeOrderRel (FieldOp.position a✝¹) (FieldOp.inAsymp a✝) → timeOrderRel (FieldOp.inAsymp a✝) c → timeOrderRel (FieldOp.position a✝¹) c𝓕:FieldSpecificationc:𝓕.FieldOpa✝¹:((f : 𝓕.Field) × 𝓕.PositionLabel f) × SpaceTimea✝:((f : 𝓕.Field) × 𝓕.PositionLabel f) × SpaceTime⊢ timeOrderRel (FieldOp.position a✝¹) (FieldOp.position a✝) → timeOrderRel (FieldOp.position a✝) c → timeOrderRel (FieldOp.position a✝¹) c𝓕:FieldSpecificationc:𝓕.FieldOpa✝¹:((f : 𝓕.Field) × 𝓕.PositionLabel f) × SpaceTimea✝:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentum⊢ timeOrderRel (FieldOp.position a✝¹) (FieldOp.outAsymp a✝) → timeOrderRel (FieldOp.outAsymp a✝) c → timeOrderRel (FieldOp.position a✝¹) c𝓕:FieldSpecificationc:𝓕.FieldOpa✝¹:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentuma✝:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentum⊢ timeOrderRel (FieldOp.outAsymp a✝¹) (FieldOp.inAsymp a✝) → timeOrderRel (FieldOp.inAsymp a✝) c → timeOrderRel (FieldOp.outAsymp a✝¹) c𝓕:FieldSpecificationc:𝓕.FieldOpa✝¹:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentuma✝:((f : 𝓕.Field) × 𝓕.PositionLabel f) × SpaceTime⊢ timeOrderRel (FieldOp.outAsymp a✝¹) (FieldOp.position a✝) → timeOrderRel (FieldOp.position a✝) c → timeOrderRel (FieldOp.outAsymp a✝¹) c𝓕:FieldSpecificationc:𝓕.FieldOpa✝¹:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentuma✝:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentum⊢ timeOrderRel (FieldOp.outAsymp a✝¹) (FieldOp.outAsymp a✝) → timeOrderRel (FieldOp.outAsymp a✝) c → timeOrderRel (FieldOp.outAsymp a✝¹) c 𝓕:FieldSpecificationa✝²:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentuma✝¹:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentuma✝:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentum⊢ timeOrderRel (FieldOp.outAsymp a✝²) (FieldOp.outAsymp a✝¹) → timeOrderRel (FieldOp.outAsymp a✝¹) (FieldOp.inAsymp a✝) → timeOrderRel (FieldOp.outAsymp a✝²) (FieldOp.inAsymp a✝)𝓕:FieldSpecificationa✝²:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentuma✝¹:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentuma✝:((f : 𝓕.Field) × 𝓕.PositionLabel f) × SpaceTime⊢ timeOrderRel (FieldOp.outAsymp a✝²) (FieldOp.outAsymp a✝¹) → timeOrderRel (FieldOp.outAsymp a✝¹) (FieldOp.position a✝) → timeOrderRel (FieldOp.outAsymp a✝²) (FieldOp.position a✝)𝓕:FieldSpecificationa✝²:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentuma✝¹:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentuma✝:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentum⊢ timeOrderRel (FieldOp.outAsymp a✝²) (FieldOp.outAsymp a✝¹) → timeOrderRel (FieldOp.outAsymp a✝¹) (FieldOp.outAsymp a✝) → timeOrderRel (FieldOp.outAsymp a✝²) (FieldOp.outAsymp a✝) 𝓕:FieldSpecificationa✝²:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentuma✝¹:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentuma✝:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentum⊢ timeOrderRel (FieldOp.inAsymp a✝²) (FieldOp.inAsymp a✝¹) → timeOrderRel (FieldOp.inAsymp a✝¹) (FieldOp.inAsymp a✝) → timeOrderRel (FieldOp.inAsymp a✝²) (FieldOp.inAsymp a✝)𝓕:FieldSpecificationa✝²:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentuma✝¹:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentuma✝:((f : 𝓕.Field) × 𝓕.PositionLabel f) × SpaceTime⊢ timeOrderRel (FieldOp.inAsymp a✝²) (FieldOp.inAsymp a✝¹) → timeOrderRel (FieldOp.inAsymp a✝¹) (FieldOp.position a✝) → timeOrderRel (FieldOp.inAsymp a✝²) (FieldOp.position a✝)𝓕:FieldSpecificationa✝²:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentuma✝¹:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentuma✝:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentum⊢ timeOrderRel (FieldOp.inAsymp a✝²) (FieldOp.inAsymp a✝¹) → timeOrderRel (FieldOp.inAsymp a✝¹) (FieldOp.outAsymp a✝) → timeOrderRel (FieldOp.inAsymp a✝²) (FieldOp.outAsymp a✝)𝓕:FieldSpecificationa✝²:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentuma✝¹:((f : 𝓕.Field) × 𝓕.PositionLabel f) × SpaceTimea✝:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentum⊢ timeOrderRel (FieldOp.inAsymp a✝²) (FieldOp.position a✝¹) → timeOrderRel (FieldOp.position a✝¹) (FieldOp.inAsymp a✝) → timeOrderRel (FieldOp.inAsymp a✝²) (FieldOp.inAsymp a✝)𝓕:FieldSpecificationa✝²:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentuma✝¹:((f : 𝓕.Field) × 𝓕.PositionLabel f) × SpaceTimea✝:((f : 𝓕.Field) × 𝓕.PositionLabel f) × SpaceTime⊢ timeOrderRel (FieldOp.inAsymp a✝²) (FieldOp.position a✝¹) → timeOrderRel (FieldOp.position a✝¹) (FieldOp.position a✝) → timeOrderRel (FieldOp.inAsymp a✝²) (FieldOp.position a✝)𝓕:FieldSpecificationa✝²:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentuma✝¹:((f : 𝓕.Field) × 𝓕.PositionLabel f) × SpaceTimea✝:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentum⊢ timeOrderRel (FieldOp.inAsymp a✝²) (FieldOp.position a✝¹) → timeOrderRel (FieldOp.position a✝¹) (FieldOp.outAsymp a✝) → timeOrderRel (FieldOp.inAsymp a✝²) (FieldOp.outAsymp a✝)𝓕:FieldSpecificationa✝²:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentuma✝¹:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentuma✝:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentum⊢ timeOrderRel (FieldOp.inAsymp a✝²) (FieldOp.outAsymp a✝¹) → timeOrderRel (FieldOp.outAsymp a✝¹) (FieldOp.inAsymp a✝) → timeOrderRel (FieldOp.inAsymp a✝²) (FieldOp.inAsymp a✝)𝓕:FieldSpecificationa✝²:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentuma✝¹:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentuma✝:((f : 𝓕.Field) × 𝓕.PositionLabel f) × SpaceTime⊢ timeOrderRel (FieldOp.inAsymp a✝²) (FieldOp.outAsymp a✝¹) → timeOrderRel (FieldOp.outAsymp a✝¹) (FieldOp.position a✝) → timeOrderRel (FieldOp.inAsymp a✝²) (FieldOp.position a✝)𝓕:FieldSpecificationa✝²:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentuma✝¹:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentuma✝:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentum⊢ timeOrderRel (FieldOp.inAsymp a✝²) (FieldOp.outAsymp a✝¹) → timeOrderRel (FieldOp.outAsymp a✝¹) (FieldOp.outAsymp a✝) → timeOrderRel (FieldOp.inAsymp a✝²) (FieldOp.outAsymp a✝)𝓕:FieldSpecificationa✝²:((f : 𝓕.Field) × 𝓕.PositionLabel f) × SpaceTimea✝¹:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentuma✝:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentum⊢ timeOrderRel (FieldOp.position a✝²) (FieldOp.inAsymp a✝¹) → timeOrderRel (FieldOp.inAsymp a✝¹) (FieldOp.inAsymp a✝) → timeOrderRel (FieldOp.position a✝²) (FieldOp.inAsymp a✝)𝓕:FieldSpecificationa✝²:((f : 𝓕.Field) × 𝓕.PositionLabel f) × SpaceTimea✝¹:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentuma✝:((f : 𝓕.Field) × 𝓕.PositionLabel f) × SpaceTime⊢ timeOrderRel (FieldOp.position a✝²) (FieldOp.inAsymp a✝¹) → timeOrderRel (FieldOp.inAsymp a✝¹) (FieldOp.position a✝) → timeOrderRel (FieldOp.position a✝²) (FieldOp.position a✝)𝓕:FieldSpecificationa✝²:((f : 𝓕.Field) × 𝓕.PositionLabel f) × SpaceTimea✝¹:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentuma✝:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentum⊢ timeOrderRel (FieldOp.position a✝²) (FieldOp.inAsymp a✝¹) → timeOrderRel (FieldOp.inAsymp a✝¹) (FieldOp.outAsymp a✝) → timeOrderRel (FieldOp.position a✝²) (FieldOp.outAsymp a✝)𝓕:FieldSpecificationa✝²:((f : 𝓕.Field) × 𝓕.PositionLabel f) × SpaceTimea✝¹:((f : 𝓕.Field) × 𝓕.PositionLabel f) × SpaceTimea✝:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentum⊢ timeOrderRel (FieldOp.position a✝²) (FieldOp.position a✝¹) → timeOrderRel (FieldOp.position a✝¹) (FieldOp.inAsymp a✝) → timeOrderRel (FieldOp.position a✝²) (FieldOp.inAsymp a✝)𝓕:FieldSpecificationa✝²:((f : 𝓕.Field) × 𝓕.PositionLabel f) × SpaceTimea✝¹:((f : 𝓕.Field) × 𝓕.PositionLabel f) × SpaceTimea✝:((f : 𝓕.Field) × 𝓕.PositionLabel f) × SpaceTime⊢ timeOrderRel (FieldOp.position a✝²) (FieldOp.position a✝¹) → timeOrderRel (FieldOp.position a✝¹) (FieldOp.position a✝) → timeOrderRel (FieldOp.position a✝²) (FieldOp.position a✝)𝓕:FieldSpecificationa✝²:((f : 𝓕.Field) × 𝓕.PositionLabel f) × SpaceTimea✝¹:((f : 𝓕.Field) × 𝓕.PositionLabel f) × SpaceTimea✝:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentum⊢ timeOrderRel (FieldOp.position a✝²) (FieldOp.position a✝¹) → timeOrderRel (FieldOp.position a✝¹) (FieldOp.outAsymp a✝) → timeOrderRel (FieldOp.position a✝²) (FieldOp.outAsymp a✝)𝓕:FieldSpecificationa✝²:((f : 𝓕.Field) × 𝓕.PositionLabel f) × SpaceTimea✝¹:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentuma✝:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentum⊢ timeOrderRel (FieldOp.position a✝²) (FieldOp.outAsymp a✝¹) → timeOrderRel (FieldOp.outAsymp a✝¹) (FieldOp.inAsymp a✝) → timeOrderRel (FieldOp.position a✝²) (FieldOp.inAsymp a✝)𝓕:FieldSpecificationa✝²:((f : 𝓕.Field) × 𝓕.PositionLabel f) × SpaceTimea✝¹:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentuma✝:((f : 𝓕.Field) × 𝓕.PositionLabel f) × SpaceTime⊢ timeOrderRel (FieldOp.position a✝²) (FieldOp.outAsymp a✝¹) → timeOrderRel (FieldOp.outAsymp a✝¹) (FieldOp.position a✝) → timeOrderRel (FieldOp.position a✝²) (FieldOp.position a✝)𝓕:FieldSpecificationa✝²:((f : 𝓕.Field) × 𝓕.PositionLabel f) × SpaceTimea✝¹:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentuma✝:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentum⊢ timeOrderRel (FieldOp.position a✝²) (FieldOp.outAsymp a✝¹) → timeOrderRel (FieldOp.outAsymp a✝¹) (FieldOp.outAsymp a✝) → timeOrderRel (FieldOp.position a✝²) (FieldOp.outAsymp a✝)𝓕:FieldSpecificationa✝²:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentuma✝¹:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentuma✝:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentum⊢ timeOrderRel (FieldOp.outAsymp a✝²) (FieldOp.inAsymp a✝¹) → timeOrderRel (FieldOp.inAsymp a✝¹) (FieldOp.inAsymp a✝) → timeOrderRel (FieldOp.outAsymp a✝²) (FieldOp.inAsymp a✝)𝓕:FieldSpecificationa✝²:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentuma✝¹:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentuma✝:((f : 𝓕.Field) × 𝓕.PositionLabel f) × SpaceTime⊢ timeOrderRel (FieldOp.outAsymp a✝²) (FieldOp.inAsymp a✝¹) → timeOrderRel (FieldOp.inAsymp a✝¹) (FieldOp.position a✝) → timeOrderRel (FieldOp.outAsymp a✝²) (FieldOp.position a✝)𝓕:FieldSpecificationa✝²:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentuma✝¹:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentuma✝:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentum⊢ timeOrderRel (FieldOp.outAsymp a✝²) (FieldOp.inAsymp a✝¹) → timeOrderRel (FieldOp.inAsymp a✝¹) (FieldOp.outAsymp a✝) → timeOrderRel (FieldOp.outAsymp a✝²) (FieldOp.outAsymp a✝)𝓕:FieldSpecificationa✝²:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentuma✝¹:((f : 𝓕.Field) × 𝓕.PositionLabel f) × SpaceTimea✝:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentum⊢ timeOrderRel (FieldOp.outAsymp a✝²) (FieldOp.position a✝¹) → timeOrderRel (FieldOp.position a✝¹) (FieldOp.inAsymp a✝) → timeOrderRel (FieldOp.outAsymp a✝²) (FieldOp.inAsymp a✝)𝓕:FieldSpecificationa✝²:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentuma✝¹:((f : 𝓕.Field) × 𝓕.PositionLabel f) × SpaceTimea✝:((f : 𝓕.Field) × 𝓕.PositionLabel f) × SpaceTime⊢ timeOrderRel (FieldOp.outAsymp a✝²) (FieldOp.position a✝¹) → timeOrderRel (FieldOp.position a✝¹) (FieldOp.position a✝) → timeOrderRel (FieldOp.outAsymp a✝²) (FieldOp.position a✝)𝓕:FieldSpecificationa✝²:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentuma✝¹:((f : 𝓕.Field) × 𝓕.PositionLabel f) × SpaceTimea✝:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentum⊢ timeOrderRel (FieldOp.outAsymp a✝²) (FieldOp.position a✝¹) → timeOrderRel (FieldOp.position a✝¹) (FieldOp.outAsymp a✝) → timeOrderRel (FieldOp.outAsymp a✝²) (FieldOp.outAsymp a✝)𝓕:FieldSpecificationa✝²:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentuma✝¹:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentuma✝:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentum⊢ timeOrderRel (FieldOp.outAsymp a✝²) (FieldOp.outAsymp a✝¹) → timeOrderRel (FieldOp.outAsymp a✝¹) (FieldOp.inAsymp a✝) → timeOrderRel (FieldOp.outAsymp a✝²) (FieldOp.inAsymp a✝)𝓕:FieldSpecificationa✝²:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentuma✝¹:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentuma✝:((f : 𝓕.Field) × 𝓕.PositionLabel f) × SpaceTime⊢ timeOrderRel (FieldOp.outAsymp a✝²) (FieldOp.outAsymp a✝¹) → timeOrderRel (FieldOp.outAsymp a✝¹) (FieldOp.position a✝) → timeOrderRel (FieldOp.outAsymp a✝²) (FieldOp.position a✝)𝓕:FieldSpecificationa✝²:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentuma✝¹:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentuma✝:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentum⊢ timeOrderRel (FieldOp.outAsymp a✝²) (FieldOp.outAsymp a✝¹) → timeOrderRel (FieldOp.outAsymp a✝¹) (FieldOp.outAsymp a✝) → timeOrderRel (FieldOp.outAsymp a✝²) (FieldOp.outAsymp a✝) All goals completed! 🐙 All goals completed! 🐙

Given a list φ :: φs of states, the (zero-based) position of the state which is of maximum time. For example

    for the list [φ1(t = 4), φ2(t = 5), φ3(t = 3), φ4(t = 5)] this would return 1. This is defined for a list φ :: φs instead of φs to ensure that such a position exists.

def maxTimeFieldPos (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp) : ℕ := insertionSortMinPos timeOrderRel φ φs
lemma maxTimeFieldPos_lt_length (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp) : maxTimeFieldPos φ φs < (φ :: φs).length := (insertionSortMinPos timeOrderRel φ φs).isLt

Given a list φ :: φs of states, the left-most state of maximum time, if there are more. As an example:

    for the list [φ1(t = 4), φ2(t = 5), φ3(t = 3), φ4(t = 5)] this would return φ2(t = 5). It is the state at the position maxTimeFieldPos φ φs.

def maxTimeField (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp) : 𝓕.FieldOp := insertionSortMin timeOrderRel φ φs

Given a list φ :: φs of states, the list with the left-most state of maximum time removed. As an example:

    for the list [φ1(t = 4), φ2(t = 5), φ3(t = 3), φ4(t = 5)] this would return [φ1(t = 4), φ3(t = 3), φ4(t = 5)].

def eraseMaxTimeField (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp) : List 𝓕.FieldOp := insertionSortDropMinPos timeOrderRel φ φs
@[simp] lemma eraseMaxTimeField_length (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp) : (eraseMaxTimeField φ φs).length = φs.length := 𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOp⊢ (eraseMaxTimeField φ φs).length = φs.length All goals completed! 🐙lemma maxTimeFieldPos_lt_eraseMaxTimeField_length_succ (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp) : maxTimeFieldPos φ φs < (eraseMaxTimeField φ φs).length.succ := 𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOp⊢ maxTimeFieldPos φ φs < (eraseMaxTimeField φ φs).length.succ All goals completed! 🐙

Given a list φ :: φs of states, the position of the left-most state of maximum time as an element of Fin (eraseMaxTimeField φ φs).length.succ. As an example:

    for the list [φ1(t = 4), φ2(t = 5), φ3(t = 3), φ4(t = 5)] this would return ⟨1,...⟩.

def maxTimeFieldPosFin (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp) : Fin (eraseMaxTimeField φ φs).length.succ := insertionSortMinPosFin timeOrderRel φ φs
lemma lt_maxTimeFieldPosFin_not_timeOrder (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp) (i : Fin (eraseMaxTimeField φ φs).length) (hi : (maxTimeFieldPosFin φ φs).succAbove i < maxTimeFieldPosFin φ φs) : ¬ timeOrderRel ((eraseMaxTimeField φ φs)[i.val]) (maxTimeField φ φs) := insertionSortMin_lt_mem_insertionSortDropMinPos_of_lt timeOrderRel φ φs i hilemma timeOrder_maxTimeField (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp) (i : Fin (eraseMaxTimeField φ φs).length) : timeOrderRel (maxTimeField φ φs) ((eraseMaxTimeField φ φs)[i.val]) := insertionSortMin_lt_mem_insertionSortDropMinPos timeOrderRel φ φs _

The sign associated with putting a list of states into time order (with the state of greatest time to the left). We pick up a minus sign for every fermion paired crossed.

def timeOrderSign (φs : List 𝓕.FieldOp) : ℂ := Wick.koszulSign 𝓕.fieldOpStatistic 𝓕.timeOrderRel φs
@[simp] lemma timeOrderSign_nil : timeOrderSign (𝓕 := 𝓕) [] = 1 := 𝓕:FieldSpecification⊢ timeOrderSign [] = 1 All goals completed! 🐙lemma timeOrderSign_pair_ordered {φ ψ : 𝓕.FieldOp} (h : timeOrderRel φ ψ) : timeOrderSign [φ, ψ] = 1 := 𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph:timeOrderRel φ ψ⊢ timeOrderSign [φ, ψ] = 1 All goals completed! 🐙lemma timeOrderSign_pair_not_ordered {φ ψ : 𝓕.FieldOp} (h : ¬ timeOrderRel φ ψ) : timeOrderSign [φ, ψ] = 𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ ψ) := 𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph:¬timeOrderRel φ ψ⊢ timeOrderSign [φ, ψ] = (exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛψ) All goals completed! 🐙𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOp⊢ timeOrderSign (φ :: φs) * (exchangeSign (𝓕|>ₛmaxTimeField φ φs)) (ofList 𝓕.fieldOpStatistic (List.take (↑(insertionSortMinPos timeOrderRel φ φs)) (φ :: φs))) = timeOrderSign (φ :: φs) * (exchangeSign (𝓕|>ₛmaxTimeField φ φs)) (ofList 𝓕.fieldOpStatistic (List.take (maxTimeFieldPos φ φs) (φ :: φs))) All goals completed! 🐙

The time ordering of a list of states. A schematic example is:

    normalOrderList [φ1(t = 4), φ2(t = 5), φ3(t = 3), φ4(t = 5)] is equal to [φ2(t = 5), φ4(t = 5), φ1(t = 4), φ3(t = 3)]

def timeOrderList (φs : List 𝓕.FieldOp) : List 𝓕.FieldOp := List.insertionSort 𝓕.timeOrderRel φs
lemma timeOrderList_pair_ordered {φ ψ : 𝓕.FieldOp} (h : timeOrderRel φ ψ) : timeOrderList [φ, ψ] = [φ, ψ] := 𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph:timeOrderRel φ ψ⊢ timeOrderList [φ, ψ] = [φ, ψ] All goals completed! 🐙lemma timeOrderList_pair_not_ordered {φ ψ : 𝓕.FieldOp} (h : ¬ timeOrderRel φ ψ) : timeOrderList [φ, ψ] = [ψ, φ] := 𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.FieldOph:¬timeOrderRel φ ψ⊢ timeOrderList [φ, ψ] = [ψ, φ] All goals completed! 🐙@[simp] lemma timeOrderList_nil : timeOrderList (𝓕 := 𝓕) [] = [] := 𝓕:FieldSpecification⊢ timeOrderList [] = [] All goals completed! 🐙lemma timeOrderList_eq_maxTimeField_timeOrderList (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp) : timeOrderList (φ :: φs) = maxTimeField φ φs :: timeOrderList (eraseMaxTimeField φ φs) := insertionSort_eq_insertionSortMin_cons timeOrderRel φ φs

Time ordering for CrAnFieldOp

timeOrderRel

For a field specification 𝓕, 𝓕.crAnTimeOrderRel is a relation on 𝓕.CrAnFieldOp representing time ordering. It is defined such that 𝓕.crAnTimeOrderRel φ₀ φ₁ is true if and only if one of the following holds

    φ₀ is an outgoing asymptotic operator

    φ₁ is an incoming asymptotic field operator

    φ₀ and φ₁ are both position field operators where the SpaceTime point of φ₀ has a time greater than or equal to that of φ₁.

Thus, colloquially 𝓕.crAnTimeOrderRel φ₀ φ₁ if φ₀ has time greater than or equal to φ₁. The use of greater than rather then less than is because on ordering lists of operators it is needed that the operator with the greatest time is to the left.

def crAnTimeOrderRel (a b : 𝓕.CrAnFieldOp) : Prop := 𝓕.timeOrderRel a.1 b.1

Time ordering of CrAnFieldOp is total.

instance : Std.Total 𝓕.crAnTimeOrderRel where total a b := Std.Total.total (r := 𝓕.timeOrderRel) a.1 b.1

Time ordering of CrAnFieldOp is transitive.

instance : IsTrans 𝓕.CrAnFieldOp 𝓕.crAnTimeOrderRel where trans a b c := IsTrans.trans (r := 𝓕.timeOrderRel) a.1 b.1 c.1
@[simp] lemma crAnTimeOrderRel_refl (φ : 𝓕.CrAnFieldOp) : crAnTimeOrderRel φ φ := (Std.Total.to_refl (r := 𝓕.crAnTimeOrderRel)).refl φ

For a field specification 𝓕, and a list φs of 𝓕.CrAnFieldOp, 𝓕.crAnTimeOrderSign φs is the sign corresponding to the number of ferimionic-fermionic exchanges undertaken to time-order (i.e. order with respect to 𝓕.crAnTimeOrderRel) φs using the insertion sort algorithm.

def crAnTimeOrderSign (φs : List 𝓕.CrAnFieldOp) : ℂ := Wick.koszulSign 𝓕.crAnStatistics 𝓕.crAnTimeOrderRel φs
@[simp] lemma crAnTimeOrderSign_nil : crAnTimeOrderSign (𝓕 := 𝓕) [] = 1 := 𝓕:FieldSpecification⊢ crAnTimeOrderSign [] = 1 All goals completed! 🐙lemma crAnTimeOrderSign_pair_ordered {φ ψ : 𝓕.CrAnFieldOp} (h : crAnTimeOrderRel φ ψ) : crAnTimeOrderSign [φ, ψ] = 1 := 𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpψ:𝓕.CrAnFieldOph:crAnTimeOrderRel φ ψ⊢ crAnTimeOrderSign [φ, ψ] = 1 All goals completed! 🐙lemma crAnTimeOrderSign_pair_not_ordered {φ ψ : 𝓕.CrAnFieldOp} (h : ¬ crAnTimeOrderRel φ ψ) : crAnTimeOrderSign [φ, ψ] = 𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ ψ) := 𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpψ:𝓕.CrAnFieldOph:¬crAnTimeOrderRel φ ψ⊢ crAnTimeOrderSign [φ, ψ] = (exchangeSign (𝓕.crAnStatistics φ)) (𝓕.crAnStatistics ψ) All goals completed! 🐙lemma crAnTimeOrderSign_swap_eq_time {φ ψ : 𝓕.CrAnFieldOp} (h1 : crAnTimeOrderRel φ ψ) (h2 : crAnTimeOrderRel ψ φ) (φs φs' : List 𝓕.CrAnFieldOp) : crAnTimeOrderSign (φs ++ φ :: ψ :: φs') = crAnTimeOrderSign (φs ++ ψ :: φ :: φs') := Wick.koszulSign_swap_eq_rel _ _ h1 h2 _ _

For a field specification 𝓕, and a list φs of 𝓕.CrAnFieldOp, 𝓕.crAnTimeOrderList φs is the list φs time-ordered using the insertion sort algorithm.

def crAnTimeOrderList (φs : List 𝓕.CrAnFieldOp) : List 𝓕.CrAnFieldOp := List.insertionSort 𝓕.crAnTimeOrderRel φs
@[simp] lemma crAnTimeOrderList_nil : crAnTimeOrderList (𝓕 := 𝓕) [] = [] := 𝓕:FieldSpecification⊢ crAnTimeOrderList [] = [] All goals completed! 🐙lemma crAnTimeOrderList_pair_ordered {φ ψ : 𝓕.CrAnFieldOp} (h : crAnTimeOrderRel φ ψ) : crAnTimeOrderList [φ, ψ] = [φ, ψ] := 𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpψ:𝓕.CrAnFieldOph:crAnTimeOrderRel φ ψ⊢ crAnTimeOrderList [φ, ψ] = [φ, ψ] All goals completed! 🐙lemma crAnTimeOrderList_pair_not_ordered {φ ψ : 𝓕.CrAnFieldOp} (h : ¬ crAnTimeOrderRel φ ψ) : crAnTimeOrderList [φ, ψ] = [ψ, φ] := 𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpψ:𝓕.CrAnFieldOph:¬crAnTimeOrderRel φ ψ⊢ crAnTimeOrderList [φ, ψ] = [ψ, φ] All goals completed! 🐙𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpψ:𝓕.CrAnFieldOph1:crAnTimeOrderRel φ ψh2:crAnTimeOrderRel ψ φφs:List 𝓕.CrAnFieldOp⊢ List.takeWhile (fun b => decide ¬crAnTimeOrderRel φ b) (List.takeWhile (fun b => decide ¬crAnTimeOrderRel ψ b) φs ++ ψ :: List.dropWhile (fun b => decide ¬crAnTimeOrderRel ψ b) φs) ++ φ :: List.dropWhile (fun b => decide ¬crAnTimeOrderRel φ b) (List.takeWhile (fun b => decide ¬crAnTimeOrderRel ψ b) φs ++ ψ :: List.dropWhile (fun b => decide ¬crAnTimeOrderRel ψ b) φs) = List.takeWhile (fun b => decide ¬crAnTimeOrderRel ψ b) φs ++ φ :: ψ :: List.dropWhile (fun b => decide ¬crAnTimeOrderRel ψ b) φs 𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpψ:𝓕.CrAnFieldOph1✝:crAnTimeOrderRel φ ψh2:crAnTimeOrderRel ψ φφs:List 𝓕.CrAnFieldOph1:∀ (b : 𝓕.CrAnFieldOp), crAnTimeOrderRel φ b ↔ crAnTimeOrderRel ψ b⊢ List.takeWhile (fun b => decide ¬crAnTimeOrderRel φ b) (List.takeWhile (fun b => decide ¬crAnTimeOrderRel ψ b) φs ++ ψ :: List.dropWhile (fun b => decide ¬crAnTimeOrderRel ψ b) φs) ++ φ :: List.dropWhile (fun b => decide ¬crAnTimeOrderRel φ b) (List.takeWhile (fun b => decide ¬crAnTimeOrderRel ψ b) φs ++ ψ :: List.dropWhile (fun b => decide ¬crAnTimeOrderRel ψ b) φs) = List.takeWhile (fun b => decide ¬crAnTimeOrderRel ψ b) φs ++ φ :: ψ :: List.dropWhile (fun b => decide ¬crAnTimeOrderRel ψ b) φs 𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpψ:𝓕.CrAnFieldOph1✝:crAnTimeOrderRel φ ψh2:crAnTimeOrderRel ψ φφs:List 𝓕.CrAnFieldOph1:∀ (b : 𝓕.CrAnFieldOp), crAnTimeOrderRel φ b ↔ crAnTimeOrderRel ψ b⊢ ∀ x ∈ List.takeWhile (fun b => !decide (crAnTimeOrderRel ψ b)) φs, crAnTimeOrderRel ψ x → ∀ x ∈ List.takeWhile (fun b => !decide (crAnTimeOrderRel ψ b)) φs, ¬crAnTimeOrderRel ψ x 𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpψ:𝓕.CrAnFieldOph1✝:crAnTimeOrderRel φ ψh2:crAnTimeOrderRel ψ φφs:List 𝓕.CrAnFieldOph1:∀ (b : 𝓕.CrAnFieldOp), crAnTimeOrderRel φ b ↔ crAnTimeOrderRel ψ bx:𝓕.CrAnFieldOphx:x ∈ List.takeWhile (fun b => !decide (crAnTimeOrderRel ψ b)) φshxψ:crAnTimeOrderRel ψ xy:𝓕.CrAnFieldOphy:y ∈ List.takeWhile (fun b => !decide (crAnTimeOrderRel ψ b)) φs⊢ ¬crAnTimeOrderRel ψ y All goals completed! 🐙𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpψ:𝓕.CrAnFieldOpφ':𝓕.CrAnFieldOph1:crAnTimeOrderRel φ ψh2:crAnTimeOrderRel ψ φφ'':𝓕.CrAnFieldOpφs:List 𝓕.CrAnFieldOpφs':List 𝓕.CrAnFieldOpl1:List 𝓕.CrAnFieldOpl2:List 𝓕.CrAnFieldOphl:List.orderedInsert crAnTimeOrderRel φ' (φs ++ φ :: ψ :: φs') = l1 ++ φ :: ψ :: l2 ∧ List.orderedInsert crAnTimeOrderRel φ' (φs ++ ψ :: φ :: φs') = l1 ++ ψ :: φ :: l2⊢ ∃ l1_1 l2_1, (if crAnTimeOrderRel φ' φ'' then φ' :: φ'' :: (φs ++ φ :: ψ :: φs') else φ'' :: (l1 ++ φ :: ψ :: l2)) = l1_1 ++ φ :: ψ :: l2_1 ∧ (if crAnTimeOrderRel φ' φ'' then φ' :: φ'' :: (φs ++ ψ :: φ :: φs') else φ'' :: (l1 ++ ψ :: φ :: l2)) = l1_1 ++ ψ :: φ :: l2_1 𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpψ:𝓕.CrAnFieldOpφ':𝓕.CrAnFieldOph1:crAnTimeOrderRel φ ψh2:crAnTimeOrderRel ψ φφ'':𝓕.CrAnFieldOpφs:List 𝓕.CrAnFieldOpφs':List 𝓕.CrAnFieldOpl1:List 𝓕.CrAnFieldOpl2:List 𝓕.CrAnFieldOphl:List.orderedInsert crAnTimeOrderRel φ' (φs ++ φ :: ψ :: φs') = l1 ++ φ :: ψ :: l2 ∧ List.orderedInsert crAnTimeOrderRel φ' (φs ++ ψ :: φ :: φs') = l1 ++ ψ :: φ :: l2h:crAnTimeOrderRel φ' φ''⊢ ∃ l1_1 l2_1, (if crAnTimeOrderRel φ' φ'' then φ' :: φ'' :: (φs ++ φ :: ψ :: φs') else φ'' :: (l1 ++ φ :: ψ :: l2)) = l1_1 ++ φ :: ψ :: l2_1 ∧ (if crAnTimeOrderRel φ' φ'' then φ' :: φ'' :: (φs ++ ψ :: φ :: φs') else φ'' :: (l1 ++ ψ :: φ :: l2)) = l1_1 ++ ψ :: φ :: l2_1𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpψ:𝓕.CrAnFieldOpφ':𝓕.CrAnFieldOph1:crAnTimeOrderRel φ ψh2:crAnTimeOrderRel ψ φφ'':𝓕.CrAnFieldOpφs:List 𝓕.CrAnFieldOpφs':List 𝓕.CrAnFieldOpl1:List 𝓕.CrAnFieldOpl2:List 𝓕.CrAnFieldOphl:List.orderedInsert crAnTimeOrderRel φ' (φs ++ φ :: ψ :: φs') = l1 ++ φ :: ψ :: l2 ∧ List.orderedInsert crAnTimeOrderRel φ' (φs ++ ψ :: φ :: φs') = l1 ++ ψ :: φ :: l2h:¬crAnTimeOrderRel φ' φ''⊢ ∃ l1_1 l2_1, (if crAnTimeOrderRel φ' φ'' then φ' :: φ'' :: (φs ++ φ :: ψ :: φs') else φ'' :: (l1 ++ φ :: ψ :: l2)) = l1_1 ++ φ :: ψ :: l2_1 ∧ (if crAnTimeOrderRel φ' φ'' then φ' :: φ'' :: (φs ++ ψ :: φ :: φs') else φ'' :: (l1 ++ ψ :: φ :: l2)) = l1_1 ++ ψ :: φ :: l2_1 𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpψ:𝓕.CrAnFieldOpφ':𝓕.CrAnFieldOph1:crAnTimeOrderRel φ ψh2:crAnTimeOrderRel ψ φφ'':𝓕.CrAnFieldOpφs:List 𝓕.CrAnFieldOpφs':List 𝓕.CrAnFieldOpl1:List 𝓕.CrAnFieldOpl2:List 𝓕.CrAnFieldOphl:List.orderedInsert crAnTimeOrderRel φ' (φs ++ φ :: ψ :: φs') = l1 ++ φ :: ψ :: l2 ∧ List.orderedInsert crAnTimeOrderRel φ' (φs ++ ψ :: φ :: φs') = l1 ++ ψ :: φ :: l2h:crAnTimeOrderRel φ' φ''⊢ ∃ l1_1 l2_1, (if crAnTimeOrderRel φ' φ'' then φ' :: φ'' :: (φs ++ φ :: ψ :: φs') else φ'' :: (l1 ++ φ :: ψ :: l2)) = l1_1 ++ φ :: ψ :: l2_1 ∧ (if crAnTimeOrderRel φ' φ'' then φ' :: φ'' :: (φs ++ ψ :: φ :: φs') else φ'' :: (l1 ++ ψ :: φ :: l2)) = l1_1 ++ ψ :: φ :: l2_1 𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpψ:𝓕.CrAnFieldOpφ':𝓕.CrAnFieldOph1:crAnTimeOrderRel φ ψh2:crAnTimeOrderRel ψ φφ'':𝓕.CrAnFieldOpφs:List 𝓕.CrAnFieldOpφs':List 𝓕.CrAnFieldOpl1:List 𝓕.CrAnFieldOpl2:List 𝓕.CrAnFieldOphl:List.orderedInsert crAnTimeOrderRel φ' (φs ++ φ :: ψ :: φs') = l1 ++ φ :: ψ :: l2 ∧ List.orderedInsert crAnTimeOrderRel φ' (φs ++ ψ :: φ :: φs') = l1 ++ ψ :: φ :: l2h:crAnTimeOrderRel φ' φ''⊢ (if crAnTimeOrderRel φ' φ'' then φ' :: φ'' :: (φs ++ φ :: ψ :: φs') else φ'' :: (l1 ++ φ :: ψ :: l2)) = φ' :: φ'' :: φs ++ φ :: ψ :: φs' ∧ (if crAnTimeOrderRel φ' φ'' then φ' :: φ'' :: (φs ++ ψ :: φ :: φs') else φ'' :: (l1 ++ ψ :: φ :: l2)) = φ' :: φ'' :: φs ++ ψ :: φ :: φs' All goals completed! 🐙 𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpψ:𝓕.CrAnFieldOpφ':𝓕.CrAnFieldOph1:crAnTimeOrderRel φ ψh2:crAnTimeOrderRel ψ φφ'':𝓕.CrAnFieldOpφs:List 𝓕.CrAnFieldOpφs':List 𝓕.CrAnFieldOpl1:List 𝓕.CrAnFieldOpl2:List 𝓕.CrAnFieldOphl:List.orderedInsert crAnTimeOrderRel φ' (φs ++ φ :: ψ :: φs') = l1 ++ φ :: ψ :: l2 ∧ List.orderedInsert crAnTimeOrderRel φ' (φs ++ ψ :: φ :: φs') = l1 ++ ψ :: φ :: l2h:¬crAnTimeOrderRel φ' φ''⊢ ∃ l1_1 l2_1, (if crAnTimeOrderRel φ' φ'' then φ' :: φ'' :: (φs ++ φ :: ψ :: φs') else φ'' :: (l1 ++ φ :: ψ :: l2)) = l1_1 ++ φ :: ψ :: l2_1 ∧ (if crAnTimeOrderRel φ' φ'' then φ' :: φ'' :: (φs ++ ψ :: φ :: φs') else φ'' :: (l1 ++ ψ :: φ :: l2)) = l1_1 ++ ψ :: φ :: l2_1 𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpψ:𝓕.CrAnFieldOpφ':𝓕.CrAnFieldOph1:crAnTimeOrderRel φ ψh2:crAnTimeOrderRel ψ φφ'':𝓕.CrAnFieldOpφs:List 𝓕.CrAnFieldOpφs':List 𝓕.CrAnFieldOpl1:List 𝓕.CrAnFieldOpl2:List 𝓕.CrAnFieldOphl:List.orderedInsert crAnTimeOrderRel φ' (φs ++ φ :: ψ :: φs') = l1 ++ φ :: ψ :: l2 ∧ List.orderedInsert crAnTimeOrderRel φ' (φs ++ ψ :: φ :: φs') = l1 ++ ψ :: φ :: l2h:¬crAnTimeOrderRel φ' φ''⊢ (if crAnTimeOrderRel φ' φ'' then φ' :: φ'' :: (φs ++ φ :: ψ :: φs') else φ'' :: (l1 ++ φ :: ψ :: l2)) = φ'' :: l1 ++ φ :: ψ :: l2 ∧ (if crAnTimeOrderRel φ' φ'' then φ' :: φ'' :: (φs ++ ψ :: φ :: φs') else φ'' :: (l1 ++ ψ :: φ :: l2)) = φ'' :: l1 ++ ψ :: φ :: l2 All goals completed! 🐙𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpψ:𝓕.CrAnFieldOph1:crAnTimeOrderRel φ ψh2:crAnTimeOrderRel ψ φφ'':𝓕.CrAnFieldOpφs:List 𝓕.CrAnFieldOpφs':List 𝓕.CrAnFieldOpl1:List 𝓕.CrAnFieldOpl2:List 𝓕.CrAnFieldOphl:List.insertionSort crAnTimeOrderRel (φs ++ φ :: ψ :: φs') = l1 ++ φ :: ψ :: l2 ∧ List.insertionSort crAnTimeOrderRel (φs ++ ψ :: φ :: φs') = l1 ++ ψ :: φ :: l2⊢ ∃ l1_1 l2_1, List.orderedInsert crAnTimeOrderRel φ'' (l1 ++ φ :: ψ :: l2) = l1_1 ++ φ :: ψ :: l2_1 ∧ List.orderedInsert crAnTimeOrderRel φ'' (l1 ++ ψ :: φ :: l2) = l1_1 ++ ψ :: φ :: l2_1 All goals completed! 🐙

Relationship to sections

lemma koszulSignInsert_crAnTimeOrderRel_crAnSection {φ : 𝓕.FieldOp} {ψ : 𝓕.CrAnFieldOp} (h : ψ.1 = φ) : {φs : List 𝓕.FieldOp} → (ψs : CrAnSection φs) → Wick.koszulSignInsert 𝓕.crAnStatistics 𝓕.crAnTimeOrderRel ψ ψs.1 = Wick.koszulSignInsert 𝓕.fieldOpStatistic 𝓕.timeOrderRel φ φs 𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.CrAnFieldOph✝:ψ.fst = φh:List.map 𝓕.crAnFieldOpToFieldOp [] = []⊢ Wick.koszulSignInsert 𝓕.crAnStatistics crAnTimeOrderRel ψ ↑⟨[], h⟩ = Wick.koszulSignInsert 𝓕.fieldOpStatistic timeOrderRel φ [] 𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.CrAnFieldOph✝:ψ.fst = φh:List.map 𝓕.crAnFieldOpToFieldOp [] = []⊢ Wick.koszulSignInsert 𝓕.crAnStatistics crAnTimeOrderRel ψ ↑⟨[], h⟩ = Wick.koszulSignInsert 𝓕.fieldOpStatistic timeOrderRel φ [] All goals completed! 🐙 𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.CrAnFieldOph:ψ.fst = φφ':𝓕.FieldOpφs:List 𝓕.FieldOpψ':𝓕.CrAnFieldOpψs:List 𝓕.CrAnFieldOph1:List.map 𝓕.crAnFieldOpToFieldOp (ψ' :: ψs) = φ' :: φs⊢ Wick.koszulSignInsert 𝓕.crAnStatistics crAnTimeOrderRel ψ ↑⟨ψ' :: ψs, h1⟩ = Wick.koszulSignInsert 𝓕.fieldOpStatistic timeOrderRel φ (φ' :: φs) 𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.CrAnFieldOph:ψ.fst = φφ':𝓕.FieldOpφs:List 𝓕.FieldOpψ':𝓕.CrAnFieldOpψs:List 𝓕.CrAnFieldOph1:List.map 𝓕.crAnFieldOpToFieldOp (ψ' :: ψs) = φ' :: φs⊢ Wick.koszulSignInsert 𝓕.crAnStatistics crAnTimeOrderRel ψ ↑⟨ψ' :: ψs, h1⟩ = Wick.koszulSignInsert 𝓕.fieldOpStatistic timeOrderRel φ (φ' :: φs) 𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.CrAnFieldOph:ψ.fst = φφ':𝓕.FieldOpφs:List 𝓕.FieldOpψ':𝓕.CrAnFieldOpψs:List 𝓕.CrAnFieldOph1✝:List.map 𝓕.crAnFieldOpToFieldOp (ψ' :: ψs) = φ' :: φsh1:𝓕.crAnFieldOpToFieldOp ψ' = φ' ∧ List.map 𝓕.crAnFieldOpToFieldOp ψs = φs⊢ Wick.koszulSignInsert 𝓕.crAnStatistics crAnTimeOrderRel ψ ↑⟨ψ' :: ψs, h1⟩ = Wick.koszulSignInsert 𝓕.fieldOpStatistic timeOrderRel φ (φ' :: φs) 𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.CrAnFieldOph:ψ.fst = φφs:List 𝓕.FieldOpψ':𝓕.CrAnFieldOpψs:List 𝓕.CrAnFieldOph2:List.map 𝓕.crAnFieldOpToFieldOp ψs = φsh1:List.map 𝓕.crAnFieldOpToFieldOp (ψ' :: ψs) = 𝓕.crAnFieldOpToFieldOp ψ' :: φs⊢ Wick.koszulSignInsert 𝓕.crAnStatistics crAnTimeOrderRel ψ ↑⟨ψ' :: ψs, h1⟩ = Wick.koszulSignInsert 𝓕.fieldOpStatistic timeOrderRel φ (𝓕.crAnFieldOpToFieldOp ψ' :: φs) 𝓕:FieldSpecificationψ:𝓕.CrAnFieldOpφs:List 𝓕.FieldOpψ':𝓕.CrAnFieldOpψs:List 𝓕.CrAnFieldOph2:List.map 𝓕.crAnFieldOpToFieldOp ψs = φsh1:List.map 𝓕.crAnFieldOpToFieldOp (ψ' :: ψs) = 𝓕.crAnFieldOpToFieldOp ψ' :: φs⊢ Wick.koszulSignInsert 𝓕.crAnStatistics crAnTimeOrderRel ψ ↑⟨ψ' :: ψs, h1⟩ = Wick.koszulSignInsert 𝓕.fieldOpStatistic timeOrderRel ψ.fst (𝓕.crAnFieldOpToFieldOp ψ' :: φs) 𝓕:FieldSpecificationψ:𝓕.CrAnFieldOpφs:List 𝓕.FieldOpψ':𝓕.CrAnFieldOpψs:List 𝓕.CrAnFieldOph2:List.map 𝓕.crAnFieldOpToFieldOp ψs = φsh1:List.map 𝓕.crAnFieldOpToFieldOp (ψ' :: ψs) = 𝓕.crAnFieldOpToFieldOp ψ' :: φs⊢ (if crAnTimeOrderRel ψ ψ' then Wick.koszulSignInsert 𝓕.fieldOpStatistic timeOrderRel ψ.fst φs else if 𝓕.crAnStatistics ψ = fermionic ∧ 𝓕.crAnStatistics ψ' = fermionic then -Wick.koszulSignInsert 𝓕.fieldOpStatistic timeOrderRel ψ.fst φs else Wick.koszulSignInsert 𝓕.fieldOpStatistic timeOrderRel ψ.fst φs) = if timeOrderRel ψ.fst (𝓕.crAnFieldOpToFieldOp ψ') then Wick.koszulSignInsert 𝓕.fieldOpStatistic timeOrderRel ψ.fst φs else if (𝓕|>ₛψ.fst) = fermionic ∧ (𝓕|>ₛ𝓕.crAnFieldOpToFieldOp ψ') = fermionic then -Wick.koszulSignInsert 𝓕.fieldOpStatistic timeOrderRel ψ.fst φs else Wick.koszulSignInsert 𝓕.fieldOpStatistic timeOrderRel ψ.fst φs All goals completed! 🐙@[simp] lemma crAnTimeOrderSign_crAnSection : {φs : List 𝓕.FieldOp} → (ψs : CrAnSection φs) → crAnTimeOrderSign ψs.1 = timeOrderSign φs 𝓕:FieldSpecificationh:List.map 𝓕.crAnFieldOpToFieldOp [] = []⊢ crAnTimeOrderSign ↑⟨[], h⟩ = timeOrderSign [] 𝓕:FieldSpecificationh:List.map 𝓕.crAnFieldOpToFieldOp [] = []⊢ crAnTimeOrderSign ↑⟨[], h⟩ = timeOrderSign [] All goals completed! 🐙 𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpψ:𝓕.CrAnFieldOpψs:List 𝓕.CrAnFieldOph:List.map 𝓕.crAnFieldOpToFieldOp (ψ :: ψs) = φ :: φs⊢ crAnTimeOrderSign ↑⟨ψ :: ψs, h⟩ = timeOrderSign (φ :: φs) 𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpψ:𝓕.CrAnFieldOpψs:List 𝓕.CrAnFieldOph:List.map 𝓕.crAnFieldOpToFieldOp (ψ :: ψs) = φ :: φs⊢ crAnTimeOrderSign ↑⟨ψ :: ψs, h⟩ = timeOrderSign (φ :: φs) 𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpψ:𝓕.CrAnFieldOpψs:List 𝓕.CrAnFieldOph✝:List.map 𝓕.crAnFieldOpToFieldOp (ψ :: ψs) = φ :: φsh:𝓕.crAnFieldOpToFieldOp ψ = φ ∧ List.map 𝓕.crAnFieldOpToFieldOp ψs = φs⊢ crAnTimeOrderSign ↑⟨ψ :: ψs, h⟩ = timeOrderSign (φ :: φs) All goals completed! 🐙𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.CrAnFieldOph:ψ.fst = φφs:List 𝓕.FieldOpψ':𝓕.CrAnFieldOpψs:List 𝓕.CrAnFieldOph2:List.map Sigma.fst ψs = φsh1:List.map 𝓕.crAnFieldOpToFieldOp (ψ' :: ψs) = 𝓕.crAnFieldOpToFieldOp ψ' :: φs⊢ List.map 𝓕.crAnFieldOpToFieldOp (List.orderedInsert crAnTimeOrderRel ψ ↑⟨ψ' :: ψs, h1⟩) = List.orderedInsert timeOrderRel φ (𝓕.crAnFieldOpToFieldOp ψ' :: φs) 𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.CrAnFieldOph:ψ.fst = φφs:List 𝓕.FieldOpψ':𝓕.CrAnFieldOpψs:List 𝓕.CrAnFieldOph2:List.map Sigma.fst ψs = φsh1:List.map 𝓕.crAnFieldOpToFieldOp (ψ' :: ψs) = 𝓕.crAnFieldOpToFieldOp ψ' :: φsih:List.map 𝓕.crAnFieldOpToFieldOp (List.orderedInsert crAnTimeOrderRel ψ ↑⟨ψs, h2⟩) = List.orderedInsert timeOrderRel φ φs⊢ List.map 𝓕.crAnFieldOpToFieldOp (List.orderedInsert crAnTimeOrderRel ψ ↑⟨ψ' :: ψs, h1⟩) = List.orderedInsert timeOrderRel φ (𝓕.crAnFieldOpToFieldOp ψ' :: φs) 𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.CrAnFieldOph:ψ.fst = φφs:List 𝓕.FieldOpψ':𝓕.CrAnFieldOpψs:List 𝓕.CrAnFieldOph2:List.map Sigma.fst ψs = φsh1:List.map 𝓕.crAnFieldOpToFieldOp (ψ' :: ψs) = 𝓕.crAnFieldOpToFieldOp ψ' :: φsih:List.map 𝓕.crAnFieldOpToFieldOp (List.orderedInsert crAnTimeOrderRel ψ ↑⟨ψs, h2⟩) = List.orderedInsert timeOrderRel φ φshr:crAnTimeOrderRel ψ ψ'⊢ List.map 𝓕.crAnFieldOpToFieldOp (List.orderedInsert crAnTimeOrderRel ψ ↑⟨ψ' :: ψs, h1⟩) = List.orderedInsert timeOrderRel φ (𝓕.crAnFieldOpToFieldOp ψ' :: φs)𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.CrAnFieldOph:ψ.fst = φφs:List 𝓕.FieldOpψ':𝓕.CrAnFieldOpψs:List 𝓕.CrAnFieldOph2:List.map Sigma.fst ψs = φsh1:List.map 𝓕.crAnFieldOpToFieldOp (ψ' :: ψs) = 𝓕.crAnFieldOpToFieldOp ψ' :: φsih:List.map 𝓕.crAnFieldOpToFieldOp (List.orderedInsert crAnTimeOrderRel ψ ↑⟨ψs, h2⟩) = List.orderedInsert timeOrderRel φ φshr:¬crAnTimeOrderRel ψ ψ'⊢ List.map 𝓕.crAnFieldOpToFieldOp (List.orderedInsert crAnTimeOrderRel ψ ↑⟨ψ' :: ψs, h1⟩) = List.orderedInsert timeOrderRel φ (𝓕.crAnFieldOpToFieldOp ψ' :: φs) 𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.CrAnFieldOph:ψ.fst = φφs:List 𝓕.FieldOpψ':𝓕.CrAnFieldOpψs:List 𝓕.CrAnFieldOph2:List.map Sigma.fst ψs = φsh1:List.map 𝓕.crAnFieldOpToFieldOp (ψ' :: ψs) = 𝓕.crAnFieldOpToFieldOp ψ' :: φsih:List.map 𝓕.crAnFieldOpToFieldOp (List.orderedInsert crAnTimeOrderRel ψ ↑⟨ψs, h2⟩) = List.orderedInsert timeOrderRel φ φshr:crAnTimeOrderRel ψ ψ'⊢ List.map 𝓕.crAnFieldOpToFieldOp (List.orderedInsert crAnTimeOrderRel ψ ↑⟨ψ' :: ψs, h1⟩) = List.orderedInsert timeOrderRel φ (𝓕.crAnFieldOpToFieldOp ψ' :: φs)𝓕:FieldSpecificationφ:𝓕.FieldOpψ:𝓕.CrAnFieldOph:ψ.fst = φφs:List 𝓕.FieldOpψ':𝓕.CrAnFieldOpψs:List 𝓕.CrAnFieldOph2:List.map Sigma.fst ψs = φsh1:List.map 𝓕.crAnFieldOpToFieldOp (ψ' :: ψs) = 𝓕.crAnFieldOpToFieldOp ψ' :: φsih:List.map 𝓕.crAnFieldOpToFieldOp (List.orderedInsert crAnTimeOrderRel ψ ↑⟨ψs, h2⟩) = List.orderedInsert timeOrderRel φ φshr:¬crAnTimeOrderRel ψ ψ'⊢ List.map 𝓕.crAnFieldOpToFieldOp (List.orderedInsert crAnTimeOrderRel ψ ↑⟨ψ' :: ψs, h1⟩) = List.orderedInsert timeOrderRel φ (𝓕.crAnFieldOpToFieldOp ψ' :: φs) All goals completed! 🐙lemma crAnTimeOrderList_crAnSection_is_crAnSection : {φs : List 𝓕.FieldOp} → (ψs : CrAnSection φs) → (crAnTimeOrderList ψs.1).map 𝓕.crAnFieldOpToFieldOp = timeOrderList φs 𝓕:FieldSpecificationh:List.map 𝓕.crAnFieldOpToFieldOp [] = []⊢ List.map 𝓕.crAnFieldOpToFieldOp (crAnTimeOrderList ↑⟨[], h⟩) = timeOrderList [] 𝓕:FieldSpecificationh:List.map 𝓕.crAnFieldOpToFieldOp [] = []⊢ List.map 𝓕.crAnFieldOpToFieldOp (crAnTimeOrderList ↑⟨[], h⟩) = timeOrderList [] All goals completed! 🐙 𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpψ:𝓕.CrAnFieldOpψs:List 𝓕.CrAnFieldOph:List.map 𝓕.crAnFieldOpToFieldOp (ψ :: ψs) = φ :: φs⊢ List.map 𝓕.crAnFieldOpToFieldOp (crAnTimeOrderList ↑⟨ψ :: ψs, h⟩) = timeOrderList (φ :: φs) 𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpψ:𝓕.CrAnFieldOpψs:List 𝓕.CrAnFieldOph:List.map 𝓕.crAnFieldOpToFieldOp (ψ :: ψs) = φ :: φs⊢ List.map 𝓕.crAnFieldOpToFieldOp (crAnTimeOrderList ↑⟨ψ :: ψs, h⟩) = timeOrderList (φ :: φs) 𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpψ:𝓕.CrAnFieldOpψs:List 𝓕.CrAnFieldOph✝:List.map 𝓕.crAnFieldOpToFieldOp (ψ :: ψs) = φ :: φsh:𝓕.crAnFieldOpToFieldOp ψ = φ ∧ List.map 𝓕.crAnFieldOpToFieldOp ψs = φs⊢ List.map 𝓕.crAnFieldOpToFieldOp (crAnTimeOrderList ↑⟨ψ :: ψs, h⟩) = timeOrderList (φ :: φs) All goals completed! 🐙

Time ordering of sections of a list of states.

def crAnSectionTimeOrder (φs : List 𝓕.FieldOp) (ψs : CrAnSection φs) : CrAnSection (timeOrderList φs) := ⟨crAnTimeOrderList ψs.1, crAnTimeOrderList_crAnSection_is_crAnSection ψs⟩
𝓕:FieldSpecificationψ:𝓕.CrAnFieldOpψ':𝓕.CrAnFieldOph:ψ.fst = ψ'.fstφ:𝓕.FieldOpφs:List 𝓕.FieldOpψ1:𝓕.CrAnFieldOpψs:List 𝓕.CrAnFieldOph1✝:List.map 𝓕.crAnFieldOpToFieldOp (ψ1 :: ψs) = φ :: φsψ1':𝓕.CrAnFieldOpψs':List 𝓕.CrAnFieldOph1'✝:List.map 𝓕.crAnFieldOpToFieldOp (ψ1' :: ψs') = φ :: φsho:List.orderedInsert crAnTimeOrderRel ψ ↑⟨ψ1 :: ψs, h1⟩ = List.orderedInsert crAnTimeOrderRel ψ' ↑⟨ψ1' :: ψs', h1'⟩h1:𝓕.crAnFieldOpToFieldOp ψ1 = φ ∧ List.map 𝓕.crAnFieldOpToFieldOp ψs = φsh1':𝓕.crAnFieldOpToFieldOp ψ1' = φ ∧ List.map 𝓕.crAnFieldOpToFieldOp ψs' = φskey:crAnTimeOrderRel ψ ψ1 ↔ crAnTimeOrderRel ψ' ψ1'⊢ ψ = ψ' ∧ ⟨ψ1 :: ψs, h1✝⟩ = ⟨ψ1' :: ψs', h1'✝⟩ 𝓕:FieldSpecificationψ:𝓕.CrAnFieldOpψ':𝓕.CrAnFieldOph:ψ.fst = ψ'.fstφ:𝓕.FieldOpφs:List 𝓕.FieldOpψ1:𝓕.CrAnFieldOpψs:List 𝓕.CrAnFieldOph1✝:List.map 𝓕.crAnFieldOpToFieldOp (ψ1 :: ψs) = φ :: φsψ1':𝓕.CrAnFieldOpψs':List 𝓕.CrAnFieldOph1'✝:List.map 𝓕.crAnFieldOpToFieldOp (ψ1' :: ψs') = φ :: φsho:(if crAnTimeOrderRel ψ ψ1 then ψ :: ψ1 :: ψs else ψ1 :: List.orderedInsert crAnTimeOrderRel ψ ψs) = if crAnTimeOrderRel ψ' ψ1' then ψ' :: ψ1' :: ψs' else ψ1' :: List.orderedInsert crAnTimeOrderRel ψ' ψs'h1:𝓕.crAnFieldOpToFieldOp ψ1 = φ ∧ List.map 𝓕.crAnFieldOpToFieldOp ψs = φsh1':𝓕.crAnFieldOpToFieldOp ψ1' = φ ∧ List.map 𝓕.crAnFieldOpToFieldOp ψs' = φskey:crAnTimeOrderRel ψ ψ1 ↔ crAnTimeOrderRel ψ' ψ1'⊢ ψ = ψ' ∧ ⟨ψ1 :: ψs, h1✝⟩ = ⟨ψ1' :: ψs', h1'✝⟩ 𝓕:FieldSpecificationψ:𝓕.CrAnFieldOpψ':𝓕.CrAnFieldOph:ψ.fst = ψ'.fstφ:𝓕.FieldOpφs:List 𝓕.FieldOpψ1:𝓕.CrAnFieldOpψs:List 𝓕.CrAnFieldOph1✝:List.map 𝓕.crAnFieldOpToFieldOp (ψ1 :: ψs) = φ :: φsψ1':𝓕.CrAnFieldOpψs':List 𝓕.CrAnFieldOph1'✝:List.map 𝓕.crAnFieldOpToFieldOp (ψ1' :: ψs') = φ :: φsho:(if crAnTimeOrderRel ψ ψ1 then ψ :: ψ1 :: ψs else ψ1 :: List.orderedInsert crAnTimeOrderRel ψ ψs) = if crAnTimeOrderRel ψ' ψ1' then ψ' :: ψ1' :: ψs' else ψ1' :: List.orderedInsert crAnTimeOrderRel ψ' ψs'h1:𝓕.crAnFieldOpToFieldOp ψ1 = φ ∧ List.map 𝓕.crAnFieldOpToFieldOp ψs = φsh1':𝓕.crAnFieldOpToFieldOp ψ1' = φ ∧ List.map 𝓕.crAnFieldOpToFieldOp ψs' = φskey:crAnTimeOrderRel ψ ψ1 ↔ crAnTimeOrderRel ψ' ψ1'hr:crAnTimeOrderRel ψ ψ1⊢ ψ = ψ' ∧ ⟨ψ1 :: ψs, h1✝⟩ = ⟨ψ1' :: ψs', h1'✝⟩𝓕:FieldSpecificationψ:𝓕.CrAnFieldOpψ':𝓕.CrAnFieldOph:ψ.fst = ψ'.fstφ:𝓕.FieldOpφs:List 𝓕.FieldOpψ1:𝓕.CrAnFieldOpψs:List 𝓕.CrAnFieldOph1✝:List.map 𝓕.crAnFieldOpToFieldOp (ψ1 :: ψs) = φ :: φsψ1':𝓕.CrAnFieldOpψs':List 𝓕.CrAnFieldOph1'✝:List.map 𝓕.crAnFieldOpToFieldOp (ψ1' :: ψs') = φ :: φsho:(if crAnTimeOrderRel ψ ψ1 then ψ :: ψ1 :: ψs else ψ1 :: List.orderedInsert crAnTimeOrderRel ψ ψs) = if crAnTimeOrderRel ψ' ψ1' then ψ' :: ψ1' :: ψs' else ψ1' :: List.orderedInsert crAnTimeOrderRel ψ' ψs'h1:𝓕.crAnFieldOpToFieldOp ψ1 = φ ∧ List.map 𝓕.crAnFieldOpToFieldOp ψs = φsh1':𝓕.crAnFieldOpToFieldOp ψ1' = φ ∧ List.map 𝓕.crAnFieldOpToFieldOp ψs' = φskey:crAnTimeOrderRel ψ ψ1 ↔ crAnTimeOrderRel ψ' ψ1'hr:¬crAnTimeOrderRel ψ ψ1⊢ ψ = ψ' ∧ ⟨ψ1 :: ψs, h1✝⟩ = ⟨ψ1' :: ψs', h1'✝⟩ 𝓕:FieldSpecificationψ:𝓕.CrAnFieldOpψ':𝓕.CrAnFieldOph:ψ.fst = ψ'.fstφ:𝓕.FieldOpφs:List 𝓕.FieldOpψ1:𝓕.CrAnFieldOpψs:List 𝓕.CrAnFieldOph1✝:List.map 𝓕.crAnFieldOpToFieldOp (ψ1 :: ψs) = φ :: φsψ1':𝓕.CrAnFieldOpψs':List 𝓕.CrAnFieldOph1'✝:List.map 𝓕.crAnFieldOpToFieldOp (ψ1' :: ψs') = φ :: φsho:(if crAnTimeOrderRel ψ ψ1 then ψ :: ψ1 :: ψs else ψ1 :: List.orderedInsert crAnTimeOrderRel ψ ψs) = if crAnTimeOrderRel ψ' ψ1' then ψ' :: ψ1' :: ψs' else ψ1' :: List.orderedInsert crAnTimeOrderRel ψ' ψs'h1:𝓕.crAnFieldOpToFieldOp ψ1 = φ ∧ List.map 𝓕.crAnFieldOpToFieldOp ψs = φsh1':𝓕.crAnFieldOpToFieldOp ψ1' = φ ∧ List.map 𝓕.crAnFieldOpToFieldOp ψs' = φskey:crAnTimeOrderRel ψ ψ1 ↔ crAnTimeOrderRel ψ' ψ1'hr:crAnTimeOrderRel ψ ψ1⊢ ψ = ψ' ∧ ⟨ψ1 :: ψs, h1✝⟩ = ⟨ψ1' :: ψs', h1'✝⟩ All goals completed! 🐙 𝓕:FieldSpecificationψ:𝓕.CrAnFieldOpψ':𝓕.CrAnFieldOph:ψ.fst = ψ'.fstφ:𝓕.FieldOpφs:List 𝓕.FieldOpψ1:𝓕.CrAnFieldOpψs:List 𝓕.CrAnFieldOph1✝:List.map 𝓕.crAnFieldOpToFieldOp (ψ1 :: ψs) = φ :: φsψ1':𝓕.CrAnFieldOpψs':List 𝓕.CrAnFieldOph1'✝:List.map 𝓕.crAnFieldOpToFieldOp (ψ1' :: ψs') = φ :: φsho:(if crAnTimeOrderRel ψ ψ1 then ψ :: ψ1 :: ψs else ψ1 :: List.orderedInsert crAnTimeOrderRel ψ ψs) = if crAnTimeOrderRel ψ' ψ1' then ψ' :: ψ1' :: ψs' else ψ1' :: List.orderedInsert crAnTimeOrderRel ψ' ψs'h1:𝓕.crAnFieldOpToFieldOp ψ1 = φ ∧ List.map 𝓕.crAnFieldOpToFieldOp ψs = φsh1':𝓕.crAnFieldOpToFieldOp ψ1' = φ ∧ List.map 𝓕.crAnFieldOpToFieldOp ψs' = φskey:crAnTimeOrderRel ψ ψ1 ↔ crAnTimeOrderRel ψ' ψ1'hr:¬crAnTimeOrderRel ψ ψ1⊢ ψ = ψ' ∧ ⟨ψ1 :: ψs, h1✝⟩ = ⟨ψ1' :: ψs', h1'✝⟩ 𝓕:FieldSpecificationψ:𝓕.CrAnFieldOpψ':𝓕.CrAnFieldOph:ψ.fst = ψ'.fstφ:𝓕.FieldOpφs:List 𝓕.FieldOpψ1:𝓕.CrAnFieldOpψs:List 𝓕.CrAnFieldOph1✝:List.map 𝓕.crAnFieldOpToFieldOp (ψ1 :: ψs) = φ :: φsψ1':𝓕.CrAnFieldOpψs':List 𝓕.CrAnFieldOph1'✝:List.map 𝓕.crAnFieldOpToFieldOp (ψ1' :: ψs') = φ :: φsh1:𝓕.crAnFieldOpToFieldOp ψ1 = φ ∧ List.map 𝓕.crAnFieldOpToFieldOp ψs = φsh1':𝓕.crAnFieldOpToFieldOp ψ1' = φ ∧ List.map 𝓕.crAnFieldOpToFieldOp ψs' = φskey:crAnTimeOrderRel ψ ψ1 ↔ crAnTimeOrderRel ψ' ψ1'hr:¬crAnTimeOrderRel ψ ψ1ho:ψ1 = ψ1' ∧ List.orderedInsert crAnTimeOrderRel ψ ψs = List.orderedInsert crAnTimeOrderRel ψ' ψs'⊢ ψ = ψ' ∧ ⟨ψ1 :: ψs, h1✝⟩ = ⟨ψ1' :: ψs', h1'✝⟩ 𝓕:FieldSpecificationψ:𝓕.CrAnFieldOpψ':𝓕.CrAnFieldOph:ψ.fst = ψ'.fstφ:𝓕.FieldOpφs:List 𝓕.FieldOpψ1:𝓕.CrAnFieldOpψs:List 𝓕.CrAnFieldOph1✝:List.map 𝓕.crAnFieldOpToFieldOp (ψ1 :: ψs) = φ :: φsψs':List 𝓕.CrAnFieldOph1:𝓕.crAnFieldOpToFieldOp ψ1 = φ ∧ List.map 𝓕.crAnFieldOpToFieldOp ψs = φshr:¬crAnTimeOrderRel ψ ψ1ho2:List.orderedInsert crAnTimeOrderRel ψ ψs = List.orderedInsert crAnTimeOrderRel ψ' ψs'h1'✝:List.map 𝓕.crAnFieldOpToFieldOp (ψ1 :: ψs') = φ :: φsh1':𝓕.crAnFieldOpToFieldOp ψ1 = φ ∧ List.map 𝓕.crAnFieldOpToFieldOp ψs' = φskey:crAnTimeOrderRel ψ ψ1 ↔ crAnTimeOrderRel ψ' ψ1⊢ ψ = ψ' ∧ ⟨ψ1 :: ψs, h1✝⟩ = ⟨ψ1 :: ψs', h1'✝⟩ 𝓕:FieldSpecificationψ:𝓕.CrAnFieldOpφ:𝓕.FieldOpφs:List 𝓕.FieldOpψ1:𝓕.CrAnFieldOpψs:List 𝓕.CrAnFieldOph1✝:List.map 𝓕.crAnFieldOpToFieldOp (ψ1 :: ψs) = φ :: φsψs':List 𝓕.CrAnFieldOph1:𝓕.crAnFieldOpToFieldOp ψ1 = φ ∧ List.map 𝓕.crAnFieldOpToFieldOp ψs = φshr:¬crAnTimeOrderRel ψ ψ1h1'✝:List.map 𝓕.crAnFieldOpToFieldOp (ψ1 :: ψs') = φ :: φsh1':𝓕.crAnFieldOpToFieldOp ψ1 = φ ∧ List.map 𝓕.crAnFieldOpToFieldOp ψs' = φshs:⟨ψs, ⋯⟩ = ⟨ψs', ⋯⟩h:ψ.fst = ψ.fstho2:List.orderedInsert crAnTimeOrderRel ψ ψs = List.orderedInsert crAnTimeOrderRel ψ ψs'key:crAnTimeOrderRel ψ ψ1 ↔ crAnTimeOrderRel ψ ψ1⊢ ψ = ψ ∧ ⟨ψ1 :: ψs, h1✝⟩ = ⟨ψ1 :: ψs', h1'✝⟩ All goals completed! 🐙𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpψ:𝓕.CrAnFieldOpψs:List 𝓕.CrAnFieldOpψ':𝓕.CrAnFieldOpψs':List 𝓕.CrAnFieldOph1:List.foldr (List.orderedInsert crAnTimeOrderRel) [] (ψ :: ψs) = List.foldr (List.orderedInsert crAnTimeOrderRel) [] (ψ' :: ψs')h:ψ.fst = φ ∧ List.map Sigma.fst ψs = φsh':ψ'.fst = φ ∧ List.map Sigma.fst ψs' = φs⊢ ψ = ψ' ∧ ψs = ψs' 𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpψ:𝓕.CrAnFieldOpψs:List 𝓕.CrAnFieldOpψ':𝓕.CrAnFieldOpψs':List 𝓕.CrAnFieldOph1:List.foldr (List.orderedInsert crAnTimeOrderRel) [] (ψ :: ψs) = List.foldr (List.orderedInsert crAnTimeOrderRel) [] (ψ' :: ψs')h:ψ.fst = φ ∧ List.map Sigma.fst ψs = φsh':ψ'.fst = φ ∧ List.map Sigma.fst ψs' = φshin:ψ = ψ' ∧ crAnSectionTimeOrder φs ⟨ψs, ⋯⟩ = crAnSectionTimeOrder φs ⟨ψs', ⋯⟩⊢ ψ = ψ' ∧ ψs = ψs' All goals completed! 🐙lemma crAnSectionTimeOrder_bijective (φs : List 𝓕.FieldOp) : Function.Bijective (𝓕.crAnSectionTimeOrder φs) := (Fintype.bijective_iff_injective_and_card _).mpr ⟨crAnSectionTimeOrder_injective, CrAnSection.card_perm_eq (List.perm_insertionSort timeOrderRel φs).symm⟩lemma sum_crAnSections_timeOrder {φs : List 𝓕.FieldOp} [AddCommMonoid M] (f : CrAnSection (timeOrderList φs) → M) : ∑ s, f s = ∑ s, f (𝓕.crAnSectionTimeOrder φs s) := ((Equiv.ofBijective _ (𝓕.crAnSectionTimeOrder_bijective φs)).sum_comp f).symm

normTimeOrderRel

The time ordering relation on CrAnFieldOp such that if two CrAnFieldOp have the same time, we normal order them.

def normTimeOrderRel (a b : 𝓕.CrAnFieldOp) : Prop := crAnTimeOrderRel a b ∧ (crAnTimeOrderRel b a → normalOrderRel a b)

Norm-Time ordering of CrAnFieldOp is total.

instance : Std.Total 𝓕.normTimeOrderRel where total a b := 𝓕:FieldSpecificationa:𝓕.CrAnFieldOpb:𝓕.CrAnFieldOp⊢ normTimeOrderRel a b ∨ normTimeOrderRel b a 𝓕:FieldSpecificationa:𝓕.CrAnFieldOpb:𝓕.CrAnFieldOph1:crAnTimeOrderRel a b ∨ crAnTimeOrderRel b a⊢ normTimeOrderRel a b ∨ normTimeOrderRel b a 𝓕:FieldSpecificationa:𝓕.CrAnFieldOpb:𝓕.CrAnFieldOph1:crAnTimeOrderRel a b ∨ crAnTimeOrderRel b ah2:normalOrderRel a b ∨ normalOrderRel b a⊢ normTimeOrderRel a b ∨ normTimeOrderRel b a 𝓕:FieldSpecificationa:𝓕.CrAnFieldOpb:𝓕.CrAnFieldOph1:crAnTimeOrderRel a b ∨ crAnTimeOrderRel b ah2:normalOrderRel a b ∨ normalOrderRel b a⊢ crAnTimeOrderRel a b ∧ (crAnTimeOrderRel b a → normalOrderRel a b) ∨ crAnTimeOrderRel b a ∧ (crAnTimeOrderRel a b → normalOrderRel b a) All goals completed! 🐙

Norm-Time ordering of CrAnFieldOp is transitive.

instance : IsTrans 𝓕.CrAnFieldOp 𝓕.normTimeOrderRel where trans a b c := 𝓕:FieldSpecificationa:𝓕.CrAnFieldOpb:𝓕.CrAnFieldOpc:𝓕.CrAnFieldOp⊢ normTimeOrderRel a b → normTimeOrderRel b c → normTimeOrderRel a c 𝓕:FieldSpecificationa:𝓕.CrAnFieldOpb:𝓕.CrAnFieldOpc:𝓕.CrAnFieldOph1:normTimeOrderRel a bh2:normTimeOrderRel b c⊢ normTimeOrderRel a c 𝓕:FieldSpecificationa:𝓕.CrAnFieldOpb:𝓕.CrAnFieldOpc:𝓕.CrAnFieldOph1:crAnTimeOrderRel a b ∧ (crAnTimeOrderRel b a → normalOrderRel a b)h2:crAnTimeOrderRel b c ∧ (crAnTimeOrderRel c b → normalOrderRel b c)⊢ crAnTimeOrderRel a c ∧ (crAnTimeOrderRel c a → normalOrderRel a c) All goals completed! 🐙

The sign associated with putting a list of CrAnFieldOp into normal-time order (with the state of greatest time to the left). We pick up a minus sign for every fermion paired crossed.

def normTimeOrderSign (φs : List 𝓕.CrAnFieldOp) : ℂ := Wick.koszulSign 𝓕.crAnStatistics 𝓕.normTimeOrderRel φs

Sort a list of CrAnFieldOp based on normTimeOrderRel.

def normTimeOrderList (φs : List 𝓕.CrAnFieldOp) : List 𝓕.CrAnFieldOp := List.insertionSort 𝓕.normTimeOrderRel φs