Documentation

FUST.Physics.TimeStructure

Time Structure from φ-Scaling #

Time evolution f ↦ f(φ·) derived from Fζ translation symmetry.

φ/ψ Duality #

Algebraic properties of the golden ratio pair: φ·|ψ| = 1, φ > 1 > |ψ|.

source
theorem FUST.TimeStructure.phi_mul_abs_psi :
φ * |ψ| = 1
source
theorem FUST.TimeStructure.phi_pow_gt_one (n : ℕ) (hn : n ≥ 1) :
φ ^ n > 1

Kernel Membership #

source
def FUST.TimeStructure.IsInKerFζ (f : ℂ → ℂ) :
Prop

f ∈ ker(Fζ) iff Fζ f = 0 everywhere

Equations
Instances For
    source
    theorem FUST.TimeStructure.IsInKerFζ_const :
    IsInKerFζ fun (x : ℂ) => 1
    source
    theorem FUST.TimeStructure.IsInKerFζ_quad :
    IsInKerFζ fun (w : ℂ) => w ^ 2
    source
    theorem FUST.TimeStructure.IsInKerFζ_cube :
    IsInKerFζ fun (w : ℂ) => w ^ 3
    source
    theorem FUST.TimeStructure.IsInKerFζ_fourth :
    IsInKerFζ fun (w : ℂ) => w ^ 4
    source
    theorem FUST.TimeStructure.IsInKerFζ_vanish_mod6_0 (k : ℕ) :
    IsInKerFζ fun (w : ℂ) => w ^ (6 * k)
    source
    theorem FUST.TimeStructure.IsInKerFζ_vanish_mod6_2 (k : ℕ) :
    IsInKerFζ fun (w : ℂ) => w ^ (6 * k + 2)
    source
    theorem FUST.TimeStructure.IsInKerFζ_vanish_mod6_3 (k : ℕ) :
    IsInKerFζ fun (w : ℂ) => w ^ (6 * k + 3)
    source
    theorem FUST.TimeStructure.IsInKerFζ_vanish_mod6_4 (k : ℕ) :
    IsInKerFζ fun (w : ℂ) => w ^ (6 * k + 4)
    source
    theorem FUST.TimeStructure.IsInKerFζ_smul (c : ℂ) (f : ℂ → ℂ) (hf : IsInKerFζ f) :
    IsInKerFζ fun (w : ℂ) => c * f w

    Action Functional #

    |Fζ f|² is non-negative with minimum at ker(Fζ).

    source
    noncomputable def FUST.TimeStructure.FζLagrangian (f : ℂ → ℂ) (z : ℂ) :
    ℝ
    Equations
    Instances For
      source
      theorem FUST.TimeStructure.Fζ_lagrangian_nonneg (f : ℂ → ℂ) (z : ℂ) :
      FζLagrangian f z ≥ 0
      source
      theorem FUST.TimeStructure.Fζ_lagrangian_zero_iff (f : ℂ → ℂ) (z : ℂ) :
      FζLagrangian f z = 0 ↔ FζOperator.Fζ f z = 0
      source
      theorem FUST.TimeStructure.Fζ_lagrangian_ker_zero (f : ℂ → ℂ) (hf : IsInKerFζ f) (z : ℂ) :
      FζLagrangian f z = 0

      Time Evolution #

      f ↦ f(φ·) from Fζ translation symmetry: Fζf(c·) = Fζf.

      source
      noncomputable def FUST.TimeStructure.timeEvolution (f : ℂ → ℂ) :
      ℂ → ℂ
      Equations
      Instances For
        source
        theorem FUST.TimeStructure.ker_Fζ_invariant (f : ℂ → ℂ) (hf : IsInKerFζ f) :
        IsInKerFζ (timeEvolution f)
        source
        theorem FUST.TimeStructure.timeEvolution_preserves_Fζ (f : ℂ → ℂ) :
        ¬IsInKerFζ f ↔ ¬IsInKerFζ (timeEvolution f)
        source
        theorem FUST.TimeStructure.monomial_amplification (n : ℕ) (t : ℂ) :
        timeEvolution (fun (s : ℂ) => s ^ n) t = ↑φ ^ n * t ^ n
        source
        theorem FUST.TimeStructure.Fζ_gauge_scaling (f : ℂ → ℂ) (c z : ℂ) :
        FζOperator.Fζ (fun (t : ℂ) => f (c * t)) z = FζOperator.Fζ f (c * z)
        source
        theorem FUST.TimeStructure.lagrangian_phi_equivariant (f : ℂ → ℂ) (z : ℂ) :
        FζLagrangian (timeEvolution f) z = FζLagrangian f (↑φ * z)

        |Fζ f|² is a Lagrangian: equivariant under time evolution Lf(φ·) = Lf

        Fζ Nonzero Implies Non-Kernel #

        source
        theorem FUST.TimeStructure.Fζ_nonzero_implies_time (f : ℂ → ℂ) (z : ℂ) (hFζ : FζOperator.Fζ f z ≠ 0) :
        ¬IsInKerFζ f

        Entropy and Third Law #

        |Fζ f|² measures departure from ker(Fζ). f ∉ ker(Fζ) ⟹ ∃z: entropy > 0.

        source
        noncomputable def FUST.TimeStructure.entropyAtFζ (f : ℂ → ℂ) (z : ℂ) :
        ℝ
        Equations
        Instances For
          source
          theorem FUST.TimeStructure.entropyAtFζ_nonneg (f : ℂ → ℂ) (z : ℂ) :
          entropyAtFζ f z ≥ 0
          source
          theorem FUST.TimeStructure.entropyAtFζ_zero_iff (f : ℂ → ℂ) (z : ℂ) :
          entropyAtFζ f z = 0 ↔ FζOperator.Fζ f z = 0
          source
          theorem FUST.TimeStructure.entropy_zero_iff_kerFζ (f : ℂ → ℂ) :
          (∀ (z : ℂ), entropyAtFζ f z = 0) ↔ IsInKerFζ f
          source
          theorem FUST.TimeStructure.third_law_Fζ (f : ℂ → ℂ) (hf : ¬IsInKerFζ f) :
          ∃ (z : ℂ), entropyAtFζ f z > 0

          Planck Second #

          |temporal Fζ eigenvalue|² = 6000, Planck second = 1/(20√15).

          source
          noncomputable def FUST.TimeStructure.temporalEigenNormSq :
          ℝ
          Equations
          Instances For
            source
            theorem FUST.TimeStructure.temporalEigenNormSq_eq :
            temporalEigenNormSq = 6000
            source
            theorem FUST.TimeStructure.temporalEigenNormSq_from_channels :
            temporalEigenNormSq = (20 * √15) ^ 2
            source
            theorem FUST.TimeStructure.temporalEigenNormSq_pos :
            temporalEigenNormSq > 0
            source
            noncomputable def FUST.TimeStructure.planckSecondSq :
            ℝ
            Equations
            Instances For
              source
              theorem FUST.TimeStructure.planckSecondSq_eq :
              planckSecondSq = 1 / 6000
              source
              theorem FUST.TimeStructure.planckSecondSq_pos :
              planckSecondSq > 0
              source
              noncomputable def FUST.TimeStructure.planckSecond :
              ℝ
              Equations
              Instances For
                source
                theorem FUST.TimeStructure.planckSecond_pos :
                planckSecond > 0
                source
                theorem FUST.TimeStructure.planckSecond_sq :
                planckSecond ^ 2 = planckSecondSq

                Planck second algebraic decomposition #

                source
                theorem FUST.TimeStructure.planckSecondSq_from_sqrt5 :
                planckSecondSq = 1 / (5 * (2 * √5)) ^ 2 / 12
                source
                theorem FUST.TimeStructure.temporalEigenNormSq_AF_decomposition :
                temporalEigenNormSq = Complex.normSq DζOperator.AF_coeff * (5 * (2 * √5)) ^ 2