import PhysicsLogic.Papers.Guth1981.RadiationHorizon.Definitions

/-! Literal contracts for every definition in the radiation causal core.
These preserve the chosen meanings; they are not human semantic approval. -/

set_option autoImplicit false
open PhysicsLogic.Papers.Guth1981.RadiationHorizon
open MeasureTheory Set
noncomputable section

example (normalization time : Real) :
    scaleFactor normalization time = normalization * Real.sqrt time := rfl

example (normalization time : Real) :
    conformalTime normalization time =
      ∫ earlier in 0..time, (scaleFactor normalization earlier)⁻¹ := rfl

example (normalization time : Real) :
    physicalHorizon normalization time =
      scaleFactor normalization time * conformalTime normalization time := rfl

example (position : Real → Real) (emission reception : Real) :
    CausalOn position emission reception ↔
      emission ≤ reception ∧ ∀ first ∈ Icc emission reception,
        ∀ second ∈ Icc emission reception, |position second - position first| ≤ |second - first| := Iff.rfl

example (normalization emission reception coordinate : Real) :
    SignalFrom normalization emission reception coordinate ↔
      0 < emission ∧ emission < reception ∧ ∃ position : Real → Real,
        CausalOn position (conformalTime normalization emission) (conformalTime normalization reception) ∧
        position (conformalTime normalization emission) = coordinate ∧
        position (conformalTime normalization reception) = 0 := Iff.rfl

example (normalization reception coordinate : Real) :
    Reachable normalization reception coordinate ↔
      ∃ emission, SignalFrom normalization emission reception coordinate := Iff.rfl

example (normalization emission reception source target : Real) :
    SignalBetween normalization emission reception source target ↔
      0 < emission ∧ emission < reception ∧ ∃ position : Real → Real,
        CausalOn position (conformalTime normalization emission) (conformalTime normalization reception) ∧
        position (conformalTime normalization emission) = source ∧
        position (conformalTime normalization reception) = target := Iff.rfl

example (normalization reception : Real) (region : Set Real) :
    CommonPastFor normalization reception region ↔
      region.Nonempty ∧ ∃ emission source : Real,
        ∀ target ∈ region, SignalBetween normalization emission reception source target := Iff.rfl