import Mathlib.Data.Real.Sqrt
import Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic

/-!
# Review Core: Flat Radiation Causal Geometry

Scope: one radial coordinate in a spatially flat FLRW approximation, c = 1.
Cosmic times and comoving coordinates are real numbers; physical theorems
require positive normalization and positive reception time. Zero time is a
limiting boundary, not an allowed emission event.

These eight definitions are the entire paper-local vocabulary for the causal
characterizations in RadiationHorizon.lean. They contain no assumed horizon
radius, causal-access flag, source ledger, or inflation-framework context.
The interpretation of the scale factor is Guth's preprint p. 8, equation
(2.18). The propagation relation spells out the radial light-speed bound.
This is a candidate specification for human review, not an approved
formalization of every meaning of observational accessibility.
-/

set_option autoImplicit false

namespace PhysicsLogic.Papers.Guth1981.RadiationHorizon
open MeasureTheory Set
noncomputable section

def scaleFactor (normalization time : Real) : Real :=
  normalization * Real.sqrt time

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

def physicalHorizon (normalization time : Real) : Real :=
  scaleFactor normalization time * conformalTime normalization time

/-- The speed bound holds between every pair of points, not only endpoints. -/
def CausalOn (position : Real → Real) (emission reception : Real) : Prop :=
  emission ≤ reception ∧ ∀ first ∈ Icc emission reception,
    ∀ second ∈ Icc emission reception, |position second - position first| ≤ |second - first|

/-- Regular cosmic emission time; the curve itself uses conformal time. -/
def SignalFrom (normalization emission reception coordinate : Real) : Prop :=
  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

def Reachable (normalization reception coordinate : Real) : Prop :=
  ∃ emission, SignalFrom normalization emission reception coordinate

/-- A causal curve from one comoving worldline to another, with regular emission. -/
def SignalBetween (normalization emission reception source target : Real) : Prop :=
  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

/-- One actual past event can send a signal to every point of a nonempty region.
The emission time and place are chosen before the reception point. This is
geometric access, not interaction, equilibration, or an observed common cause. -/
def CommonPastFor (normalization reception : Real) (region : Set Real) : Prop :=
  region.Nonempty ∧ ∃ emission source : Real,
    ∀ target ∈ region, SignalBetween normalization emission reception source target

end
end PhysicsLogic.Papers.Guth1981.RadiationHorizon