From d1f0b38ec19465f22f4a133bc5aa59e3309f51e2 Mon Sep 17 00:00:00 2001 From: "Jorge A. Garcia" Date: Wed, 8 Jul 2026 01:32:06 -0600 Subject: [PATCH] feat(entropic-time): entropic proper time with information dimension --- Physlib.lean | 5 + Physlib/SpaceAndTime/EntropicProperTime.lean | 296 ++++++++++++++++++ Physlib/SpaceAndTime/SpaceTime/Lapse.lean | 86 +++++ Physlib/SpaceAndTime/TolmanScaling.lean | 91 ++++++ Physlib/Units/ComplexActionDimension.lean | 231 ++++++++++++++ Physlib/Units/Dimension.lean | 139 +++++++- .../Units/InformationDimensionCollision.lean | 148 +++++++++ QuantumInfo.lean | 2 + QuantumInfo/Entropy/EntropicProperTime.lean | 18 ++ .../Entropy/EntropicProperTime/Basic.lean | 108 +++++++ 10 files changed, 1110 insertions(+), 14 deletions(-) create mode 100644 Physlib/SpaceAndTime/EntropicProperTime.lean create mode 100644 Physlib/SpaceAndTime/SpaceTime/Lapse.lean create mode 100644 Physlib/SpaceAndTime/TolmanScaling.lean create mode 100644 Physlib/Units/ComplexActionDimension.lean create mode 100644 Physlib/Units/InformationDimensionCollision.lean create mode 100644 QuantumInfo/Entropy/EntropicProperTime.lean create mode 100644 QuantumInfo/Entropy/EntropicProperTime/Basic.lean diff --git a/Physlib.lean b/Physlib.lean index b967eed14..9617d53c6 100644 --- a/Physlib.lean +++ b/Physlib.lean @@ -403,6 +403,7 @@ public import Physlib.Relativity.Tensors.Reindexing public import Physlib.Relativity.Tensors.TensorSpecies.Basic public import Physlib.Relativity.Tensors.Tensorial public import Physlib.Relativity.Tensors.UnitTensor +public import Physlib.SpaceAndTime.EntropicProperTime public import Physlib.SpaceAndTime.GalileanGroup.Basic public import Physlib.SpaceAndTime.Space.Basic public import Physlib.SpaceAndTime.Space.ConstantSliceDist @@ -436,6 +437,7 @@ public import Physlib.SpaceAndTime.Space.Translations public import Physlib.SpaceAndTime.SpaceTime.Basic public import Physlib.SpaceAndTime.SpaceTime.Boosts public import Physlib.SpaceAndTime.SpaceTime.Derivatives +public import Physlib.SpaceAndTime.SpaceTime.Lapse public import Physlib.SpaceAndTime.SpaceTime.LorentzAction public import Physlib.SpaceAndTime.SpaceTime.TimeSlice public import Physlib.SpaceAndTime.Time.Basic @@ -448,6 +450,7 @@ public import Physlib.SpaceAndTime.TimeAndSpace.Basic public import Physlib.SpaceAndTime.TimeAndSpace.ConstantTimeDist public import Physlib.SpaceAndTime.TimeAndSpace.EuclideanGroup.Action public import Physlib.SpaceAndTime.TimeAndSpace.EuclideanGroup.SchwartzAction +public import Physlib.SpaceAndTime.TolmanScaling public import Physlib.StatisticalMechanics.BoltzmannConstant public import Physlib.StatisticalMechanics.CanonicalEnsemble.Basic public import Physlib.StatisticalMechanics.CanonicalEnsemble.Finite @@ -475,6 +478,8 @@ public import Physlib.Thermodynamics.Temperature.Basic public import Physlib.Thermodynamics.Temperature.TemperatureUnits public import Physlib.Units.Basic public import Physlib.Units.Dimension +public import Physlib.Units.InformationDimensionCollision +public import Physlib.Units.ComplexActionDimension public import Physlib.Units.Examples public import Physlib.Units.FDeriv public import Physlib.Units.Integral diff --git a/Physlib/SpaceAndTime/EntropicProperTime.lean b/Physlib/SpaceAndTime/EntropicProperTime.lean new file mode 100644 index 000000000..828006fc5 --- /dev/null +++ b/Physlib/SpaceAndTime/EntropicProperTime.lean @@ -0,0 +1,296 @@ +/- +Copyright (c) 2026 Jorge A. Garcia. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Jorge A. Garcia +-/ +module + +public import QuantumInfo.Entropy.EntropicProperTime +public import Physlib.SpaceAndTime.SpaceTime.Lapse +public import Physlib.Relativity.Tensors.RealTensor.Vector.MinkowskiProduct +public import Physlib.Units.Dimension +public import Physlib.Units.ComplexActionDimension +public import Physlib.SpaceAndTime.TolmanScaling + +/-! + +# Entropic proper time — dimensional lift and spacetime coupling + +`QuantumInfo.Finite.entropicProperTime ρ σ = qRelativeEnt ρ σ` is a +dimensionless `ENNReal`. This module lifts it to a metric time via a +positive scale of dimension `T`, + +The previous additive form `τ_total = τ_geom + D(ρ‖σ)` was dimensionally +inconsistent (a length/time added to a dimensionless number). The corrected +form is `τ_total = τ_geom + (ℏ/(k_B T_∞)) · D(ρ‖σ)`. + +defines the metric **relative-entropy time** `(ℏ/(k_B T_∞)) · D(ρ‖σ)`, +and equips it with a `TolmanScaling`-style lapse redshift on a +`Lapse sd`. The combined observable + + `τ_total := τ_geom + (ℏ/(k_B T_∞)) · D(ρ‖σ)` + +(`totalProperTimeMetric` below) is dimensionally consistent — both +summands include the dimension of time. + +## Source and equation map + +* H. Umegaki, *Conditional expectation in an operator algebra. IV. Entropy and information*, + Kodai Mathematical Seminar Reports 14 (1962), 59-85, doi:10.2996/kmj/1138844604: + finite quantum relative entropy `D(ρ‖σ) = Tr(ρ(log ρ - log σ))`. +* H. Araki, *Relative Entropy of States of von Neumann Algebras*, Publications of the + Research Institute for Mathematical Sciences 11 (1976), 809-833, + doi:10.2977/prims/1195191148: modular relative entropy and its finite-dimensional + logarithmic specialization. +* A. Connes and C. Rovelli, *Von Neumann algebra automorphisms and time-thermodynamics + relation in generally covariant quantum theories*, Classical and Quantum Gravity 11 + (1994), 2899-2918, doi:10.1088/0264-9381/11/12/007: thermal-time motivation via + state-dependent modular flow. This module keeps the more modest finite-state scalar + `D(ρ‖σ)` and does not assert a Tomita-Takesaki identification. +* R. C. Tolman, *On the Weight of Heat and Thermal Equilibrium in General Relativity*, + Physical Review 35 (1930), 904-924, doi:10.1103/PhysRev.35.904; and R. C. Tolman + with P. Ehrenfest, *Temperature Equilibrium in a Static Gravitational Field*, Physical + Review 36 (1930), 1791-1798, doi:10.1103/PhysRev.36.1791: lapse-redshift law + `O_loc(x) * N(x) = O_∞`. +* C. Rovelli and M. Smerlak, *Thermal time and Tolman-Ehrenfest effect: temperature as + the speed of time*, Classical and Quantum Gravity 28 (2011), 075007, + doi:10.1088/0264-9381/28/7/075007: thermal-time/Tolman relation used as motivation + for redshifting clock rates. + +The Lean statements correspond to these equations: + +* `entropicGap ρ σ = (D(ρ‖σ)).toReal`; +* `entropicProperTimeMetric U ρ σ = (ℏ/(k_B T_∞)) * D(ρ‖σ)`; +* `totalProperTimeMetric = τ_geom + (ℏ/(k_B T_∞)) * D(ρ‖σ)`; +* `totalProperTimeMetric_at_frozen`: when `ρ = σ`, `D(ρ‖ρ)=0`, so the total time + reduces to the geometric interval; +* `entropicProperTimeLocalMetric_tolman`: `τ_ent,loc(x) * N(x) = τ_ent,∞`. +* `entropicProperTime_no_scalar_complex_action_with_information`: a scalar complex action + with dimensionless `i` cannot identify an informational imaginary part + `E·T·I` with the mechanical action dimension `E·T`; the independent `[I]` axis is + therefore part of the dimensional data, not optional decoration. +-/ + +@[expose] public section + +noncomputable section + +namespace QuantumInfo.Finite + +open Physlib.SpaceTime Dimension Lorentz Vector Real + +variable {d : Type*} [Fintype d] [DecidableEq d] +variable {sd : ℕ} + +/-! ## A. Unit data -/ + +/-- Physical unit data converting dimensionless relative entropy into a metric +time via the scale `ℏ / (k_B · T_∞)`. -/ +structure EntropicTimeUnits where + /-- Reduced Planck constant. -/ + hbar : ℝ + /-- Boltzmann constant. -/ + kB : ℝ + /-- Reference temperature. -/ + T_inf : ℝ + /-- `ℏ > 0`. -/ + hbar_pos : 0 < hbar + /-- `k_B > 0`. -/ + kB_pos : 0 < kB + /-- `T_∞ > 0`. -/ + T_inf_pos : 0 < T_inf + +namespace EntropicTimeUnits + +/-- The time scale `ℏ / (k_B · T_∞)`. -/ +def scale (U : EntropicTimeUnits) : ℝ := + U.hbar / (U.kB * U.T_inf) + +/-- The time scale is strictly positive. -/ +theorem scale_pos (U : EntropicTimeUnits) : 0 < U.scale := by + unfold scale + exact div_pos U.hbar_pos (mul_pos U.kB_pos U.T_inf_pos) + +end EntropicTimeUnits + +/-! ## B. Dimensionless gap and metric lift -/ + +/-- The dimensionless entropic gap `D(ρ‖σ)` as a real number. -/ +def entropicGap (ρ σ : MState d) : ℝ := + (entropicProperTime ρ σ).toReal + +@[simp] theorem entropicGap_self (ρ : MState d) : + entropicGap ρ ρ = 0 := by + unfold entropicGap + rw [entropicProperTime_self] + simp + +theorem entropicGap_nonneg (ρ σ : MState d) : + 0 ≤ entropicGap ρ σ := + ENNReal.toReal_nonneg + +/-- The **metric entropic proper time** `τ_ent := (ℏ/(k_B T_∞)) · D(ρ‖σ)`. -/ +def entropicProperTimeMetric + (U : EntropicTimeUnits) (ρ σ : MState d) : ℝ := + U.scale * entropicGap ρ σ + +@[simp] theorem entropicProperTimeMetric_self + (U : EntropicTimeUnits) (ρ : MState d) : + entropicProperTimeMetric U ρ ρ = 0 := by + unfold entropicProperTimeMetric + rw [entropicGap_self] + ring + +/-- **Non-negativity of the metric entropic proper time**: a positive +scale times a non-negative `entropicGap` is non-negative. + +Does not prove: discreteness of values; minimum nonzero step; +uniqueness of `τ_ent`; equality to physical proper time. +The same conclusion holds for `σ := ρ` (gap is `0`). +-/ +theorem entropicProperTimeMetric_nonneg + (U : EntropicTimeUnits) (ρ σ : MState d) : + 0 ≤ entropicProperTimeMetric U ρ σ := by + unfold entropicProperTimeMetric + exact mul_nonneg U.scale_pos.le (entropicGap_nonneg ρ σ) + +/-! ## C. Geometric interval and total proper time -/ + +/-- The **geometric Minkowski interval** between events `q` and `p`: +`√⟪p−q, p−q⟫ₘ`. This is the bare geometric part of the total proper time; +in the entropic-time framework it is *not* the primitive but the frozen-LRF residue of +`totalProperTimeMetric`. Declared here so that `totalProperTimeMetric` +is self-contained; `Physlib.Relativity.Special.ProperTime` defines +`SpaceTime.properTime` as the frozen-extraction of `totalProperTimeMetric` +via this value. -/ +def geometricInterval {sd : ℕ} (q p : SpaceTime sd) : ℝ := + √⟪p - q, p - q⟫ₘ + +/-- **Total proper time** with the dimensionally-correct entropic lift: +`τ_total = τ_geom + (ℏ/(k_B T_∞)) · D(ρ‖σ)`. + +In the entropic-time inversion this is the **primitive observable**; the +geometric Minkowski interval emerges as its frozen-LRF residue +(see `totalProperTimeMetric_at_frozen`). -/ +def totalProperTimeMetric + (U : EntropicTimeUnits) + (q p : SpaceTime sd) (ρ σ : MState d) : ℝ := + geometricInterval q p + entropicProperTimeMetric U ρ σ + +/-- At the Frozen-LRF (`ρ = σ`), the total proper time reduces to the +bare geometric Minkowski interval. **The entropic-time load-bearing claim**: +the geometric "proper time" is a side-effect of total proper time at +zero relative entropy. -/ +theorem totalProperTimeMetric_at_frozen + (U : EntropicTimeUnits) (q p : SpaceTime sd) (ρ : MState d) : + totalProperTimeMetric U q p ρ ρ = geometricInterval q p := by + unfold totalProperTimeMetric + rw [entropicProperTimeMetric_self] + ring + +/-! ## D. Local lapse form (metric) -/ + +/-- **Local-frame metric entropic time** at event `x`, redshifted by the lapse: +`τ_ent_loc = τ_ent / N(x)`, built on the dimensionally-correct metric time. -/ +def entropicProperTimeLocalMetric + (U : EntropicTimeUnits) (L : Lapse sd) (ρ σ : MState d) (x : SpaceTime sd) : ℝ := + entropicProperTimeMetric U ρ σ / L.N x + +/-- Local Tolman invariant: `τ_ent_loc(x) · N(x) = τ_ent`. -/ +theorem entropicProperTimeLocalMetric_tolman + (U : EntropicTimeUnits) (L : Lapse sd) (ρ σ : MState d) (x : SpaceTime sd) : + entropicProperTimeLocalMetric U L ρ σ x * L.N x = + entropicProperTimeMetric U ρ σ := + div_mul_cancel₀ _ (L.N_pos x).ne' + +/-- Frozen-LRF: the local metric entropic time vanishes at every event. -/ +@[simp] theorem entropicProperTimeLocalMetric_self + (U : EntropicTimeUnits) (L : Lapse sd) (ρ : MState d) (x : SpaceTime sd) : + entropicProperTimeLocalMetric U L ρ ρ x = 0 := by + unfold entropicProperTimeLocalMetric + rw [entropicProperTimeMetric_self] + simp + +/-- Unit-lapse limit: the local metric entropic time equals the asymptotic +metric entropic time. -/ +theorem entropicProperTimeLocalMetric_unit_lapse + (U : EntropicTimeUnits) (ρ σ : MState d) (x : SpaceTime sd) : + entropicProperTimeLocalMetric U (Lapse.unit (d := sd)) ρ σ x = + entropicProperTimeMetric U ρ σ := by + unfold entropicProperTimeLocalMetric + rw [Lapse.unit_N, div_one] + +/-- **Metric entropic proper time as a Tolman-scaled observable** over a lapse: +the asymptotic value is `τ_ent = (ℏ/(k_B T_∞))·D(ρ‖σ)`, with the redshift law +held as a structure field rather than a hidden definition. -/ +def entropicProperTimeTolmanScaling + (U : EntropicTimeUnits) (L : Lapse sd) (ρ σ : MState d) : TolmanScaling sd where + L := L + asymptotic := entropicProperTimeMetric U ρ σ + localValue := fun x => entropicProperTimeMetric U ρ σ / L.N x + law := fun x => div_mul_cancel₀ _ (L.N_pos x).ne' + +/-- The Tolman-instance local value is exactly `entropicProperTimeLocalMetric`. -/ +@[simp] theorem entropicProperTimeTolmanScaling_localValue + (U : EntropicTimeUnits) (L : Lapse sd) (ρ σ : MState d) (x : SpaceTime sd) : + (entropicProperTimeTolmanScaling U L ρ σ).localValue x = + entropicProperTimeLocalMetric U L ρ σ x := + rfl + +/-- The local metric entropic time satisfies the Tolman invariant (named to +state the law explicitly). -/ +theorem entropicProperTimeLocalMetric_satisfies_tolman + (U : EntropicTimeUnits) (L : Lapse sd) (ρ σ : MState d) (x : SpaceTime sd) : + entropicProperTimeLocalMetric U L ρ σ x * L.N x = + entropicProperTimeMetric U ρ σ := + (entropicProperTimeTolmanScaling U L ρ σ).law x + +/-! ## E. Complex proper time (metric) -/ + +/-- **Complex proper time**: real part the geometric Minkowski interval, +imaginary part the dimensionally-scaled metric entropic proper time. -/ +def complexProperTimeMetric + (U : EntropicTimeUnits) (q p : SpaceTime sd) (ρ σ : MState d) : ℂ := + ⟨geometricInterval q p, entropicProperTimeMetric U ρ σ⟩ + +theorem complexProperTimeMetric_at_frozen + (U : EntropicTimeUnits) (q p : SpaceTime sd) (ρ : MState d) : + complexProperTimeMetric U q p ρ ρ = (geometricInterval q p : ℂ) := by + apply Complex.ext + · show geometricInterval q p = geometricInterval q p; rfl + · show entropicProperTimeMetric U ρ ρ = 0 + rw [entropicProperTimeMetric_self] + +@[simp] theorem complexProperTimeMetric_re + (U : EntropicTimeUnits) (q p : SpaceTime sd) (ρ σ : MState d) : + (complexProperTimeMetric U q p ρ σ).re = geometricInterval q p := rfl + +@[simp] theorem complexProperTimeMetric_im + (U : EntropicTimeUnits) (q p : SpaceTime sd) (ρ σ : MState d) : + (complexProperTimeMetric U q p ρ σ).im = entropicProperTimeMetric U ρ σ := rfl + +/-! ## F. Dimensional tag -/ + +/-- **No-go link to the unit layer.** A scalar complex action with dimensionless `i` +cannot absorb an informational imaginary part into the mechanical action dimension: +`[i] = 1` and `[i*S_I] = E*T` force `[S_I] = E*T`, not `E*T*I`. +Thus the entropic-time scale relies on the independent information axis `[I]` already +installed in `Dimension`. -/ +theorem entropicProperTime_no_scalar_complex_action_with_information : + ¬ ∃ imag : Dimension, imag * imag = 1 ∧ + imag * (Physlib.Units.InformationDimensionCollision.energy_dim * T𝓭 * I𝓭) = + Physlib.Units.InformationDimensionCollision.energy_dim * T𝓭 := + Physlib.Units.ComplexActionDimension.scalar_no_informational_imaginary + +/-- The entropic time scale `ℏ/(k_B T_∞)` includes the dimension of **time**: +`[ℏ/(k_B T_∞)] = (M·L²·T⁻¹)/((M·L²·T⁻²·Θ⁻¹)·Θ) = T`. -/ +theorem entropicTimeScale_dimension : + (M𝓭 * L𝓭 ^ (2 : ℚ) * T𝓭 ^ (-1 : ℚ)) + / ((M𝓭 * L𝓭 ^ (2 : ℚ) * T𝓭 ^ (-2 : ℚ) * Θ𝓭 ^ (-1 : ℚ)) * Θ𝓭) + = T𝓭 := by + ext + all_goals simp <;> ring_nf + +end QuantumInfo.Finite + +end diff --git a/Physlib/SpaceAndTime/SpaceTime/Lapse.lean b/Physlib/SpaceAndTime/SpaceTime/Lapse.lean new file mode 100644 index 000000000..a318af514 --- /dev/null +++ b/Physlib/SpaceAndTime/SpaceTime/Lapse.lean @@ -0,0 +1,86 @@ +/- +Copyright (c) 2026 Jorge A. Garcia. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +-/ +module + +public import Physlib.SpaceAndTime.SpaceTime.Basic + +/-! +# Lapse function on spacetime + +A `Lapse d` is a strictly-positive scalar function on +`SpaceTime d`, in the ADM sense: + + `N : SpaceTime d → ℝ`, `∀ x, 0 < N x`. + +The lapse converts asymptotic-frame quantities to local-frame +quantities at a given event via the Tolman law + + `O_loc(x) := O_∞ / N(x)`, so that `O_loc(x) · N(x) = O_∞`. + +A thin abstraction over Physlib's existing `SpaceTime d` structure +(built on `Lorentz.Vector d`), so that consumers can take a lapse as +an input parameter without importing additional spacetime machinery. + +## Conventions + +* Coordinate `0` is time; `1..d` are spatial. +* `Lapse.unit` is the Minkowski-limit lapse `N(x) ≡ 1`. +* `tolman_invariant` is the position-independent identity + `(O_∞ / N(x)) · N(x) = O_∞`. + +## Source and equation map + +* R. Arnowitt, S. Deser, and C. W. Misner, *The dynamics of general relativity*, + in *Gravitation: An Introduction to Current Research* (1962), republished in + General Relativity and Gravitation 40 (2008), 1997-2027, doi:10.1007/s10714-008-0661-1. + This is the standard ADM source for using a positive lapse in spacetime splitting. +* R. C. Tolman, *On the Weight of Heat and Thermal Equilibrium in General Relativity*, + Physical Review 35 (1930), 904-924, doi:10.1103/PhysRev.35.904. +* R. C. Tolman and P. Ehrenfest, *Temperature Equilibrium in a Static Gravitational + Field*, Physical Review 36 (1930), 1791-1798, doi:10.1103/PhysRev.36.1791. + +The Lean structure records only the reusable positive-lapse interface: +`N : SpaceTime d → ℝ`, `0 < N x`. The Tolman expression is represented abstractly as +`O_loc(x) = O_∞ / N(x)`, hence `O_loc(x) * N(x) = O_∞`. +-/ + +set_option autoImplicit false + +@[expose] public section + +noncomputable section + +namespace Physlib.SpaceTime + +variable {d : ℕ} + +/-- **Lapse function** `N : SpaceTime d → ℝ⁺`. -/ +structure Lapse (d : ℕ := 3) where + /-- The lapse value at each spacetime event. -/ + N : SpaceTime d → ℝ + /-- Lapse is strictly positive everywhere. -/ + N_pos : ∀ x, 0 < N x + +namespace Lapse + +/-- The **unit lapse** `N(x) ≡ 1` (Minkowski limit, no redshift). -/ +def unit : Lapse d where + N := fun _ => 1 + N_pos := fun _ => one_pos + +@[simp] theorem unit_N (x : SpaceTime d) : (unit (d := d)).N x = 1 := rfl + +/-- **Tolman invariant**: for any asymptotic value `O_∞` and any +event `x`, the local value `O_loc(x) := O_∞ / N(x)` satisfies +`O_loc(x) · N(x) = O_∞`. -/ +theorem tolman_invariant (L : Lapse d) (O_inf : ℝ) (x : SpaceTime d) : + (O_inf / L.N x) * L.N x = O_inf := + div_mul_cancel₀ _ (L.N_pos x).ne' + +end Lapse + +end Physlib.SpaceTime + +end diff --git a/Physlib/SpaceAndTime/TolmanScaling.lean b/Physlib/SpaceAndTime/TolmanScaling.lean new file mode 100644 index 000000000..b56ae65c1 --- /dev/null +++ b/Physlib/SpaceAndTime/TolmanScaling.lean @@ -0,0 +1,91 @@ +/- +Copyright (c) 2026 Jorge A. Garcia. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +-/ +module + +public import Physlib.SpaceAndTime.SpaceTime.Lapse + +/-! +# Tolman scaling + +A `TolmanScaling` packages an asymptotic value `O_∞`, a position-dependent local +value `O_loc : SpaceTime → ℝ`, and a lapse `N`, subject to the Tolman invariant +`O_loc(x) · N(x) = O_∞`. This is the generic structure behind gravitational +redshift laws (temperature, decoherence rate, clock rate, …): any quantity that +redshifts by the lapse satisfies the same law. + +(The field is named `localValue` because `local` is a reserved keyword.) + +## Source and equation map + +* R. C. Tolman, *On the Weight of Heat and Thermal Equilibrium in General Relativity*, + Physical Review 35 (1930), 904-924, doi:10.1103/PhysRev.35.904. +* R. C. Tolman and P. Ehrenfest, *Temperature Equilibrium in a Static Gravitational + Field*, Physical Review 36 (1930), 1791-1798, doi:10.1103/PhysRev.36.1791. +* C. Rovelli and M. Smerlak, *Thermal time and Tolman-Ehrenfest effect: temperature as + the speed of time*, Classical and Quantum Gravity 28 (2011), 075007, + doi:10.1088/0264-9381/28/7/075007. + +The physical Tolman-Ehrenfest temperature law is `T(x) N(x) = T_∞` in lapse notation +(for a static metric, `N = sqrt(-g_00)` in common sign conventions). This file abstracts +that equation to any scalar observable `O` satisfying `O_loc(x) * N(x) = O_∞`. +-/ + +@[expose] public section + +noncomputable section + +namespace Physlib.SpaceTime + +variable {sd : ℕ} + +/-- A quantity that redshifts by the lapse: `O_loc(x) · N(x) = O_∞`. -/ +structure TolmanScaling (sd : ℕ) where + /-- The lapse field. -/ + L : Lapse sd + /-- Asymptotic (infinity-frame) value. -/ + asymptotic : ℝ + /-- Locally measured value at each event. -/ + localValue : SpaceTime sd → ℝ + /-- Tolman invariant. -/ + law : ∀ x, localValue x * L.N x = asymptotic + +namespace TolmanScaling + +/-- The local value is the asymptotic value divided by the lapse. -/ +theorem localValue_eq_asymptotic_div_lapse + (T : TolmanScaling sd) (x : SpaceTime sd) : + T.localValue x = T.asymptotic / T.L.N x := by + have hN : T.L.N x ≠ 0 := (T.L.N_pos x).ne' + exact (eq_div_iff hN).mpr (T.law x) + +/-- The Tolman invariant as a `@[simp]` rewrite. -/ +@[simp] theorem localValue_mul_lapse + (T : TolmanScaling sd) (x : SpaceTime sd) : + T.localValue x * T.L.N x = T.asymptotic := + T.law x + +/-- The local/asymptotic ratio is the inverse lapse `1/N(x)`. -/ +theorem localValue_div_asymptotic_eq_inv_lapse + (T : TolmanScaling sd) (x : SpaceTime sd) (hA : T.asymptotic ≠ 0) : + T.localValue x / T.asymptotic = 1 / T.L.N x := by + rw [T.localValue_eq_asymptotic_div_lapse x] + field_simp + +/-- **Monotonicity under lapse ordering**: for a positive asymptotic value, +a smaller lapse gives a larger local value (deeper gravity well ⇒ larger local +quantity). The single reusable monotonicity fact for all Tolman-scaled +observables. -/ +theorem localValue_monotone_of_positive_asymptotic + (T : TolmanScaling sd) (hA : 0 < T.asymptotic) + {x₁ x₂ : SpaceTime sd} (hN : T.L.N x₂ ≤ T.L.N x₁) : + T.localValue x₁ ≤ T.localValue x₂ := by + rw [T.localValue_eq_asymptotic_div_lapse x₁, T.localValue_eq_asymptotic_div_lapse x₂] + exact div_le_div_of_nonneg_left hA.le (T.L.N_pos x₂) hN + +end TolmanScaling + +end Physlib.SpaceTime + +end diff --git a/Physlib/Units/ComplexActionDimension.lean b/Physlib/Units/ComplexActionDimension.lean new file mode 100644 index 000000000..c2902a76a --- /dev/null +++ b/Physlib/Units/ComplexActionDimension.lean @@ -0,0 +1,231 @@ +/- +Copyright (c) 2026 Jorge A. Garcia. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Jorge A. Garcia +-/ +module + +public import Physlib.Units.InformationDimensionCollision +public import Mathlib.Analysis.SpecialFunctions.Log.Basic + +/-! +# The intrinsically complex (graded) action resolves `action = angular momentum` + +In the Nagao–Nielsen **Complex Action Theory** (complex-action) the action is intrinsically +**complex**, `S = S_R + i·S_I`. This is introduced in §1 (Introduction), Prog. Theor. +Phys. **126**(6), p. 1021–1022: the path-integral integrand `exp(i S/ℏ)` is complex, +so `S` may be complex (complex-action vs the real-action theory RAT). The formal real/imaginary +split `S = Re_{} S + i·Im_{} S` is the *modified real/imaginary parts* of §2.3, +Eqs (2.8)–(2.14), p. 1025–1026 (`{}`-real (2.13), purely `{}`-imaginary (2.14)); the +non-hermitian operators with complex eigenvalues are §2.1, Eqs (2.1)–(2.3), p. 1024. + +**complex-action is the scalar reading.** In complex-action the phase `i S/ℏ` must be dimensionless, so the +complex action is an **action-dimensioned scalar**: both `S_R` and `S_I` have dimension `E·T`. +That is exactly the *scalar reading* below — to which the no-go (`scalar_action_noGo`) +applies, so the complex-action action is dimensionally indistinguishable from angular momentum. + +Here we instead read the action **graded**: `S_R` on the mechanical action axis `E·T`, +`S_I` on the **information** axis `I𝓭` — a genuine direct sum of two dimensional axes, +not a single homogeneous scalar. **This dimensional/information-graded reading is an +addition beyond Nagao–Nielsen complex-action**, not part of their formulation; it is what resolves +the `action = angular momentum` collision the scalar complex-action reading cannot. + +## Why the imaginary unit is dimensionless — two agreeing reasons + +The imaginary unit `i` is dimensionless, `[i] = 1`, for two independent reasons that +agree: + +* **Algebraic** (the mathematical backstop, `dimensionless_of_sq_one`): `i² = −1` is + dimensionless, so `[i]² = 1`, and in the rational-exponent dimension group that forces + `[i] = 1` (`q + q = 0 ⟹ q = 0`). +* **Informational** (the physical content): the imaginary axis is information, and the + information dimension is a *count* — its quantum is the **pure real `ln 2`**, the + Landauer minimum (proven minimal in `DiscreteEntropicClock`, `landauerFloor = ln 2`). + +Because the information quantum is `informationQuantum = ln 2`, a dimensionless *number* +(a count of nats), the imaginary unit — which advances the imaginary action by one such +quantum — has no dimensional exponent: `[i] = 1`. The dimension `I𝓭` belongs to +the imaginary *action* `S_I` (`imaginaryAction_dim`), not the *unit* `i` +(`imaginaryUnit_dim`); these are distinct (`imaginaryUnit_dim_ne_imaginaryAction_dim`). +That is precisely the special character of `[I]`: alone among the base dimensions it has +a proven minimal quantum that is a pure number. + +## How the collision is resolved — one coordinate of the dimension vector + +Dimensions are 6-tuples `⟨length, time, mass, charge, temperature, information⟩`. + +**The collision (scalar reading).** Both quantities have the *same* vector: +``` + angular momentum = r × p = M·L²·T⁻¹ = ⟨2, −1, 1, 0, 0, 0⟩ + action (scalar) = E·T = M·L²·T⁻¹ = ⟨2, −1, 1, 0, 0, 0⟩ ← information = 0 +``` +Identical ⇒ they collide (`scalarAction_collides_angularMomentum`). + +**The resolution (graded reading).** The graded complex action puts its two parts on +*different* axes — `S_R` on `E·T` and `S_I` on the information axis `I𝓭` — so the full +action occupies both, giving it a *nonzero information coordinate*: +``` + complex action = ⟨2, −1, 1, 0, 0, 1⟩ ← information = 1 + angular momentum = ⟨2, −1, 1, 0, 0, 0⟩ ← information = 0 + ↑ + differ in exactly ONE coordinate +``` +The information coordinate is `1` for the action but `0` for purely-mechanical angular +momentum. One coordinate differs ⇒ the vectors are distinct +(`complexAction_ne_angularMomentum`); the Lean proof projects the assumed equality onto +the information axis (`congrArg Dimension.information`) and derives `1 = 0`. + +**Why the scalar reading could not do this.** Homogeneity of `S_R + i·S_I` forces `S_I` +to share `S_R`'s dimension `E·T`, so the action never leaves the mechanical axes +(information stays `0`) and collides. The graded reading lets `S_I` live on its own +information axis; what permits that — without `i` having to bridge `E·T` and `I` — is +that **`i` is dimensionless** (it merely marks the imaginary direction), for the two +agreeing reasons above. + +**In one sentence.** The collision is resolved because the imaginary action `S_I` +has the information dimension `[I]`, giving the complex action a nonzero information +coordinate (`1`) that angular momentum lacks (`0`) — the two vectors, identical on the +mechanical axes, now differ on the information axis. + +## References + +* K. Nagao, H. B. Nielsen, *Formulation of Complex Action Theory*, Prog. Theor. Phys. + **126**(6) (2011) 1021–1049, doi:10.1143/PTP.126.1021. The complex action + `S = S_R + i·S_I`: §1 (Introduction), p. 1021–1022 (`exp(i S/ℏ)` complex ⟹ `S` + complex). Formal real/imaginary split `Re_{} S`, `Im_{} S`: §2.3, Eqs (2.8)–(2.14), + p. 1025–1026. Non-hermitian `q̂_new, p̂_new` with `[q̂_new, p̂_new] = iℏ`: §2.1, + Eqs (2.1)–(2.3), p. 1024. +* K. Nagao, H. B. Nielsen, *Momentum relation and classical limit in the + future-not-included complex action theory*, PTEP **2018**(1) 013B02, + doi:10.1093/ptep/ptx176. +* L. Brillouin, *Science and Information Theory* (1956); R. Landauer, *Irreversibility + and heat generation in the computing process* (1961) — the information dimension `[I]` + and the floor `ln 2`. +-/ + +set_option autoImplicit false + +open Dimension Physlib.Units.InformationDimensionCollision + +@[expose] public section + +namespace Physlib.Units.ComplexActionDimension + +/-- **The information (Landauer) quantum**: the minimal information value, a *pure +positive real* `ln 2`. Proven minimal in `DiscreteEntropicClock` +(`landauerFloor = ln 2`). Being a count of nats, it is dimensionless as a *value*; its +*dimension* is the information axis `I𝓭`. This is the reason the imaginary unit is +dimensionless. -/ +noncomputable def informationQuantum : ℝ := Real.log 2 + +theorem informationQuantum_pos : 0 < informationQuantum := + Real.log_pos (by norm_num) + +/-- **Algebraic corroboration that `[i] = 1`.** Any dimension squaring to the unit *is* +the unit: `d·d = 1 ⟹ d = 1`. So the bare constraint `[i]² = 1` (from `i² = −1` +dimensionless) independently forces `[i] = 1` — the rational exponents are torsion-free +(`q + q = 0 ⟹ q = 0`). This agrees with the informational reason; the informational one +is the physical input, this is the mathematical backstop. -/ +theorem dimensionless_of_sq_one (d : Dimension) (h : d * d = 1) : d = 1 := by + have e : ∀ q : ℚ, q + q = 0 → q = 0 := fun q hq => by linarith + ext + · exact e _ (by have := congrArg Dimension.length h; simpa using this) + · exact e _ (by have := congrArg Dimension.time h; simpa using this) + · exact e _ (by have := congrArg Dimension.mass h; simpa using this) + · exact e _ (by have := congrArg Dimension.charge h; simpa using this) + · exact e _ (by have := congrArg Dimension.temperature h; simpa using this) + · exact e _ (by have := congrArg Dimension.information h; simpa using this) + +/-- The imaginary action `S_I` is intrinsically **informational**: `[S_I] = I𝓭`. -/ +def imaginaryAction_dim : Dimension := I𝓭 + +/-- **The imaginary unit is dimensionless**, `[i] = 1` — because its quantum is the pure +real `informationQuantum = ln 2`. The dimension `I𝓭` sits on the imaginary action, not +on the unit. -/ +def imaginaryUnit_dim : Dimension := 1 + +/-- The dimensionless imaginary unit is distinct from the informational imaginary axis: +`[i] = 1 ≠ I𝓭 = [S_I]`. The unit has the dimensionless value `ln 2`; the action +has dimension `[I]`. -/ +theorem imaginaryUnit_dim_ne_imaginaryAction_dim : + imaginaryUnit_dim ≠ imaginaryAction_dim := by + rw [imaginaryUnit_dim, imaginaryAction_dim] + exact fun h => I𝓭_ne_one h.symm + +/-- The homogeneous-scalar reading of the action: both parts on the mechanical axis, +`[S] = E·T`. -/ +def scalarAction_dim : Dimension := energy_dim * T𝓭 + +/-- **Scalar reading: the collision stands.** `[E·T] = M·L²·T⁻¹ =` angular momentum. -/ +theorem scalarAction_collides_angularMomentum : + scalarAction_dim = angularMomentum_dim := by + unfold scalarAction_dim + ext <;> norm_num [energy_dim, angularMomentum_dim] + +/-! ## No-go theorem for the scalar reading + +Under the scalar reading the imaginary part is **dimensionally inert**: homogeneity plus +a dimensionless imaginary unit force `[S_I] = [S_R]`, so no information can enter and the +action is locked onto the mechanical axis. Hence it can never be distinguished from +angular momentum — the collision is unavoidable. -/ + +/-- **The scalar imaginary action is forced to be mechanical.** Homogeneity +`[S_R] = [i·S_I]` with mechanical real part `[S_R] = E·T` and a dimensionless imaginary +unit (`imag·imag = 1`, i.e. `i² = −1`) forces `[S_I] = E·T`. The imaginary action cannot +occupy any other axis. -/ +theorem scalar_imaginary_inert {imag S_I : Dimension} + (hi : imag * imag = 1) (hhom : energy_dim * T𝓭 = imag * S_I) : + S_I = energy_dim * T𝓭 := by + rw [dimensionless_of_sq_one imag hi, one_mul] at hhom + exact hhom.symm + +/-- **The scalar imaginary action has zero information**: `[S_I].information = 0`. +Information is dimensionally barred from a scalar action. -/ +theorem scalar_imaginary_information_zero {imag S_I : Dimension} + (hi : imag * imag = 1) (hhom : energy_dim * T𝓭 = imag * S_I) : + S_I.information = 0 := by + rw [scalar_imaginary_inert hi hhom]; simp [energy_dim] + +/-- **No-go (collision is unavoidable).** There is no scalar complex action with a +mechanical real part `E·T` and a dimensionless imaginary unit that differs from angular +momentum: homogeneity collapses the whole action onto `E·T = M·L²·T⁻¹`, identical to +angular momentum. -/ +theorem scalar_action_noGo : + ¬ ∃ actionDim imag S_I : Dimension, + imag * imag = 1 + ∧ actionDim = energy_dim * T𝓭 + ∧ actionDim = imag * S_I + ∧ actionDim ≠ angularMomentum_dim := by + rintro ⟨actionDim, imag, S_I, _, hreal, _, hne⟩ + exact hne (hreal.trans scalarAction_collides_angularMomentum) + +/-- **No-go (information cannot enter a scalar action).** There is no dimensionless +imaginary unit making the scalar action homogeneous with an *informational* imaginary +part `[S_I] = E·T·I`: it would require `[i] = I⁻¹`, contradicting `[i] = 1`. The +information dimension is available only to the graded (non-scalar) action — which is +exactly why the graded reading resolves the collision. -/ +theorem scalar_no_informational_imaginary : + ¬ ∃ imag : Dimension, imag * imag = 1 ∧ + imag * (energy_dim * T𝓭 * I𝓭) = energy_dim * T𝓭 := by + rintro ⟨imag, hsq, hhom⟩ + rw [dimensionless_of_sq_one imag hsq, one_mul] at hhom + exact I𝓭_ne_one (mul_left_cancel (a := energy_dim * T𝓭) (by rw [mul_one]; exact hhom)) + +/-- **The graded complex action**: real part `E·T`, imaginary part `I𝓭`. Its dimensional +content has a nonzero information exponent. -/ +def complexAction_dim : Dimension := energy_dim * T𝓭 * imaginaryAction_dim + +/-- **`action = angular momentum` is resolved.** The two dimension vectors are identical +on the mechanical axes but differ on the **information** coordinate: the graded complex +action has information exponent `1` (assigned to `S_I`), angular momentum has `0`. One +coordinate differs, so the dimensions are distinct. The proof projects the assumed +equality onto the information axis and derives `1 = 0`. -/ +theorem complexAction_ne_angularMomentum : + complexAction_dim ≠ angularMomentum_dim := by + intro h + have := congrArg Dimension.information h + simp [complexAction_dim, imaginaryAction_dim, energy_dim, angularMomentum_dim] at this + +end Physlib.Units.ComplexActionDimension + +end diff --git a/Physlib/Units/Dimension.lean b/Physlib/Units/Dimension.lean index 3b59e8a3b..922d212ff 100644 --- a/Physlib/Units/Dimension.lean +++ b/Physlib/Units/Dimension.lean @@ -10,7 +10,7 @@ public import Mathlib.Analysis.Normed.Field.Lemmas # Dimension -In this module we define the type `Dimension` which carries the dimension +In this module we define the type `Dimension` which records the dimension of a physical quantity. -/ @@ -26,7 +26,15 @@ open NNReal -/ /-- The foundational dimensions. - Defined in the order ⟨length, time, mass, charge, temperature⟩ -/ + Defined in the order ⟨length, time, mass, charge, temperature, information⟩. + + The `information` slot tracks the dimension of *information content* + (Shannon entropy, bits, qubits) as a primitive base, independent of + thermodynamic temperature. Without it the SI/ISQ basis cannot + distinguish dimensionless ratios from genuinely dimensionless + information measures — the Brillouin (1956) / Landauer (1961) + argument. Boltzmann's constant `k_B` then has dimension + `[E·Θ⁻¹·I⁻¹]` (energy per temperature per nat). -/ structure Dimension where /-- The length dimension. -/ length : ℚ @@ -38,6 +46,8 @@ structure Dimension where charge : ℚ /-- The temperature dimension. -/ temperature : ℚ + /-- The information dimension (bits / nats / qubits). -/ + information : ℚ := 0 namespace Dimension @@ -47,7 +57,8 @@ lemma ext {d1 d2 : Dimension} (h2 : d1.time = d2.time) (h3 : d1.mass = d2.mass) (h4 : d1.charge = d2.charge) - (h5 : d1.temperature = d2.temperature) : + (h5 : d1.temperature = d2.temperature) + (h6 : d1.information = d2.information) : d1 = d2 := by cases d1 cases d2 @@ -58,7 +69,8 @@ instance : Mul Dimension where d1.time + d2.time, d1.mass + d2.mass, d1.charge + d2.charge, - d1.temperature + d2.temperature⟩ + d1.temperature + d2.temperature, + d1.information + d2.information⟩ @[simp] lemma time_mul (d1 d2 : Dimension) : @@ -80,8 +92,12 @@ lemma charge_mul (d1 d2 : Dimension) : lemma temperature_mul (d1 d2 : Dimension) : (d1 * d2).temperature = d1.temperature + d2.temperature := rfl +@[simp] +lemma information_mul (d1 d2 : Dimension) : + (d1 * d2).information = d1.information + d2.information := rfl + instance : One Dimension where - one := ⟨0, 0, 0, 0, 0⟩ + one := ⟨0, 0, 0, 0, 0, 0⟩ @[simp] lemma one_length : (1 : Dimension).length = 0 := rfl @@ -97,11 +113,15 @@ lemma one_charge : (1 : Dimension).charge = 0 := rfl @[simp] lemma one_temperature : (1 : Dimension).temperature = 0 := rfl +@[simp] +lemma one_information : (1 : Dimension).information = 0 := rfl + instance : CommGroup Dimension where mul_assoc a b c := by ext all_goals - simp only [length_mul, time_mul, mass_mul, charge_mul, temperature_mul] + simp only [length_mul, time_mul, mass_mul, charge_mul, temperature_mul, + information_mul] ring one_mul a := by ext @@ -111,14 +131,15 @@ instance : CommGroup Dimension where ext all_goals simp - inv d := ⟨-d.length, -d.time, -d.mass, -d.charge, -d.temperature⟩ + inv d := ⟨-d.length, -d.time, -d.mass, -d.charge, -d.temperature, -d.information⟩ inv_mul_cancel a := by ext all_goals simp mul_comm a b := by ext all_goals - simp only [length_mul, time_mul, mass_mul, charge_mul, temperature_mul] + simp only [length_mul, time_mul, mass_mul, charge_mul, temperature_mul, + information_mul] ring @[simp] @@ -136,6 +157,9 @@ lemma inv_charge (d : Dimension) : d⁻¹.charge = -d.charge := rfl @[simp] lemma inv_temperature (d : Dimension) : d⁻¹.temperature = -d.temperature := rfl +@[simp] +lemma inv_information (d : Dimension) : d⁻¹.information = -d.information := rfl + @[simp] lemma div_length (d1 d2 : Dimension) : (d1 / d2).length = d1.length - d2.length := by simp [div_eq_mul_inv, sub_eq_add_neg] @@ -157,6 +181,12 @@ lemma div_temperature (d1 d2 : Dimension) : (d1 / d2).temperature = d1.temperature - d2.temperature := by simp [div_eq_mul_inv, sub_eq_add_neg] +@[simp] +lemma div_information (d1 d2 : Dimension) : + (d1 / d2).information = d1.information - d2.information := by + rw [div_eq_mul_inv, information_mul, inv_information] + ring + @[simp] lemma npow_length (d : Dimension) (n : ℕ) : (d ^ n).length = n • d.length := by induction n with @@ -187,11 +217,42 @@ lemma npow_temperature (d : Dimension) (n : ℕ) : (d ^ n).temperature = n • d | zero => simp | succ n ih => rw [pow_succ, temperature_mul, ih, succ_nsmul] +@[simp] +lemma npow_information (d : Dimension) (n : ℕ) : + (d ^ n).information = n • d.information := by + induction n with + | zero => simp + | succ n ih => + rw [@pow_add] + simp [ih] + ring + instance : Pow Dimension ℚ where - pow d n := ⟨d.length * n, d.time * n, d.mass * n, d.charge * n, d.temperature * n⟩ + pow d n := ⟨d.length * n, d.time * n, d.mass * n, d.charge * n, d.temperature * n, + d.information * n⟩ + +@[simp] +lemma qpow_length (d : Dimension) (n : ℚ) : (d ^ n).length = d.length * n := rfl + +@[simp] +lemma qpow_time (d : Dimension) (n : ℚ) : (d ^ n).time = d.time * n := rfl + +@[simp] +lemma qpow_mass (d : Dimension) (n : ℚ) : (d ^ n).mass = d.mass * n := rfl + +@[simp] +lemma qpow_charge (d : Dimension) (n : ℚ) : (d ^ n).charge = d.charge * n := rfl + +@[simp] +lemma qpow_temperature (d : Dimension) (n : ℚ) : + (d ^ n).temperature = d.temperature * n := rfl + +@[simp] +lemma qpow_information (d : Dimension) (n : ℚ) : + (d ^ n).information = d.information * n := rfl /-- The dimension corresponding to length. -/ -def L𝓭 : Dimension := ⟨1, 0, 0, 0, 0⟩ +def L𝓭 : Dimension := ⟨1, 0, 0, 0, 0, 0⟩ @[simp] lemma L𝓭_length : L𝓭.length = 1 := by rfl @@ -208,8 +269,11 @@ lemma L𝓭_charge : L𝓭.charge = 0 := by rfl @[simp] lemma L𝓭_temperature : L𝓭.temperature = 0 := by rfl +@[simp] +lemma L𝓭_information : L𝓭.information = 0 := by rfl + /-- The dimension corresponding to time. -/ -def T𝓭 : Dimension := ⟨0, 1, 0, 0, 0⟩ +def T𝓭 : Dimension := ⟨0, 1, 0, 0, 0, 0⟩ @[simp] lemma T𝓭_length : T𝓭.length = 0 := by rfl @@ -226,13 +290,60 @@ lemma T𝓭_charge : T𝓭.charge = 0 := by rfl @[simp] lemma T𝓭_temperature : T𝓭.temperature = 0 := by rfl +@[simp] +lemma T𝓭_information : T𝓭.information = 0 := by rfl + /-- The dimension corresponding to mass. -/ -def M𝓭 : Dimension := ⟨0, 0, 1, 0, 0⟩ +def M𝓭 : Dimension := ⟨0, 0, 1, 0, 0, 0⟩ /-- The dimension corresponding to charge. -/ -def C𝓭 : Dimension := ⟨0, 0, 0, 1, 0⟩ +def C𝓭 : Dimension := ⟨0, 0, 0, 1, 0, 0⟩ /-- The dimension corresponding to temperature. -/ -def Θ𝓭 : Dimension := ⟨0, 0, 0, 0, 1⟩ +def Θ𝓭 : Dimension := ⟨0, 0, 0, 0, 1, 0⟩ + +/-- The dimension corresponding to information (bits / nats / qubits). + +Justification: the ISO/ISQ basis `{L, T, M, C, Θ}` has no slot to +distinguish a *dimensionless count of information* (a number of bits, +nats, or qubits) from a generic dimensionless ratio. This is the +Brillouin (1956) / Landauer (1961) / Bennett (1982) gap: Shannon +entropy `H = − Σ pᵢ log pᵢ` and Boltzmann entropy `S = k_B ln Ω` +should be the same physical quantity (Boltzmann's `k_B` converts +between them), but in the SI basis they are forced to share a slot +with all other dimensionless numbers. + +With `I𝓭` as an independent base, `[k_B] = E·Θ⁻¹·I⁻¹`, +`[S_Boltzmann] = I`, and `S/ℏ` becomes a *typed* dimensionless ratio +(both numerator and denominator encode `I`). -/ +def I𝓭 : Dimension := ⟨0, 0, 0, 0, 0, 1⟩ + +@[simp] lemma M𝓭_length : M𝓭.length = 0 := rfl +@[simp] lemma M𝓭_time : M𝓭.time = 0 := rfl +@[simp] lemma M𝓭_mass : M𝓭.mass = 1 := rfl +@[simp] lemma M𝓭_charge : M𝓭.charge = 0 := rfl +@[simp] lemma M𝓭_temperature : M𝓭.temperature = 0 := rfl +@[simp] lemma M𝓭_information : M𝓭.information = 0 := rfl + +@[simp] lemma C𝓭_length : C𝓭.length = 0 := rfl +@[simp] lemma C𝓭_time : C𝓭.time = 0 := rfl +@[simp] lemma C𝓭_mass : C𝓭.mass = 0 := rfl +@[simp] lemma C𝓭_charge : C𝓭.charge = 1 := rfl +@[simp] lemma C𝓭_temperature : C𝓭.temperature = 0 := rfl +@[simp] lemma C𝓭_information : C𝓭.information = 0 := rfl + +@[simp] lemma Θ𝓭_length : Θ𝓭.length = 0 := rfl +@[simp] lemma Θ𝓭_time : Θ𝓭.time = 0 := rfl +@[simp] lemma Θ𝓭_mass : Θ𝓭.mass = 0 := rfl +@[simp] lemma Θ𝓭_charge : Θ𝓭.charge = 0 := rfl +@[simp] lemma Θ𝓭_temperature : Θ𝓭.temperature = 1 := rfl +@[simp] lemma Θ𝓭_information : Θ𝓭.information = 0 := rfl + +@[simp] lemma I𝓭_length : I𝓭.length = 0 := rfl +@[simp] lemma I𝓭_time : I𝓭.time = 0 := rfl +@[simp] lemma I𝓭_mass : I𝓭.mass = 0 := rfl +@[simp] lemma I𝓭_charge : I𝓭.charge = 0 := rfl +@[simp] lemma I𝓭_temperature : I𝓭.temperature = 0 := rfl +@[simp] lemma I𝓭_information : I𝓭.information = 1 := rfl end Dimension diff --git a/Physlib/Units/InformationDimensionCollision.lean b/Physlib/Units/InformationDimensionCollision.lean new file mode 100644 index 000000000..07d9bea1e --- /dev/null +++ b/Physlib/Units/InformationDimensionCollision.lean @@ -0,0 +1,148 @@ +/- +Copyright (c) 2026 Jorge A. Garcia. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Jorge A. Garcia +-/ +module + +public import Physlib.Units.Dimension +public import Mathlib.Tactic.NormNum + +/-! +# Forgetting the information dimension forces a collision + +The dimension of a physical quantity is an element of the free abelian group on the +base axes; "a collision" is two *distinct* dimensions that become *equal* — the +dimension map failing to be injective. This file proves that **dropping the +information axis `[I]` is a quotient with non-trivial kernel**, so collisions are +guaranteed: + +* `forgetInfo` zeros the information component (the 6-base → 5-base SI projection); it + is a homomorphism (`forgetInfo_mul`, `forgetInfo_one`) but **not injective** + (`forgetInfo_not_injective`). +* `shannon_collides_dimensionless` — its kernel already contains `I𝓭`: Shannon + entropy `I` and a pure dimensionless number become the same dimension. +* `boltzmann_collides_thermoEntropy` — the physically relevant collision: without + `[I]`, the **Boltzmann constant** `k_B = E·Θ⁻¹·I⁻¹` and **thermodynamic entropy** + `E·Θ⁻¹` are indistinguishable. That is exactly the Brillouin/Landauer point, now as + a forced collision: any theory containing an information-dependent quantity collapses + it onto an information-free one the moment `[I]` is dropped. +* `collision_of_info_differ` — the general criterion: any two dimensions agreeing off + the information axis but differing on it collide under `forgetInfo`. + +## The collisions `[I]` does *not* resolve (your examples) + +Adding `[I]` is **necessary** for the information collision but **not sufficient** to +make dimension injective. Collisions that are information-free survive in *both* the +5- and 6-base structures — they are orthogonal to `[I]`: + +* `action_eq_angularMomentum` — action and angular momentum are both `M·L²·T⁻¹`. +* `torque_eq_energy` — torque and energy are both `M·L²·T⁻²`. + +These are *geometric* collisions (a scalar vs a pseudovector, etc.): dimensional +analysis tracks only the `{M,L,T,…}` scaling, not tensor character, so no base axis +separates them. The information axis fixes precisely one identification — information +vs dimensionless — and leaves these untouched. + +References: Brillouin (1956); Landauer (1961). +-/ + +set_option autoImplicit false + +open Dimension + +@[expose] public section + +namespace Physlib.Units.InformationDimensionCollision + +/-- **The 6-base → 5-base projection**: forget the information exponent. -/ +def forgetInfo (d : Dimension) : Dimension := + ⟨d.length, d.time, d.mass, d.charge, d.temperature, 0⟩ + +@[simp] theorem forgetInfo_length (d : Dimension) : (forgetInfo d).length = d.length := rfl +@[simp] theorem forgetInfo_time (d : Dimension) : (forgetInfo d).time = d.time := rfl +@[simp] theorem forgetInfo_mass (d : Dimension) : (forgetInfo d).mass = d.mass := rfl +@[simp] theorem forgetInfo_charge (d : Dimension) : (forgetInfo d).charge = d.charge := rfl +@[simp] theorem forgetInfo_temperature (d : Dimension) : + (forgetInfo d).temperature = d.temperature := rfl +@[simp] theorem forgetInfo_information (d : Dimension) : (forgetInfo d).information = 0 := rfl + +/-- `forgetInfo` is multiplicative (a group homomorphism on dimensions). -/ +theorem forgetInfo_mul (d e : Dimension) : + forgetInfo (d * e) = forgetInfo d * forgetInfo e := by ext <;> simp + +theorem forgetInfo_one : forgetInfo 1 = 1 := by ext <;> simp + +/-! ## The guaranteed collision: `forgetInfo` is not injective -/ + +theorem forgetInfo_I𝓭 : forgetInfo I𝓭 = 1 := by ext <;> simp + +theorem I𝓭_ne_one : (I𝓭 : Dimension) ≠ 1 := by + intro h; have := congrArg Dimension.information h; simp at this + +/-- **Shannon entropy collides with a dimensionless number.** `I𝓭` is a non-trivial +element of the kernel of `forgetInfo`: forgetting `[I]`, one bit of information and a +pure number are the same dimension. -/ +theorem shannon_collides_dimensionless : + forgetInfo I𝓭 = forgetInfo (1 : Dimension) ∧ I𝓭 ≠ (1 : Dimension) := + ⟨by rw [forgetInfo_I𝓭, forgetInfo_one], I𝓭_ne_one⟩ + +/-- **Forgetting `[I]` is not injective** — collisions are guaranteed. -/ +theorem forgetInfo_not_injective : ¬ Function.Injective forgetInfo := fun hinj => + I𝓭_ne_one (hinj (by rw [forgetInfo_I𝓭, forgetInfo_one])) + +/-! ## The physically relevant collision: `k_B` vs thermodynamic entropy -/ + +/-- Energy dimension `E = M·L²·T⁻²`. -/ +def energy_dim : Dimension := M𝓭 * L𝓭 ^ (2 : ℚ) * T𝓭 ^ (-2 : ℚ) + +/-- Framework Boltzmann constant `[k_B] = E·Θ⁻¹·I⁻¹`. -/ +def boltzmann_dim : Dimension := energy_dim * Θ𝓭⁻¹ * I𝓭⁻¹ + +/-- Thermodynamic (Clausius) entropy `[S] = E·Θ⁻¹`. -/ +def thermoEntropy_dim : Dimension := energy_dim * Θ𝓭⁻¹ + +/-- **Without `[I]`, the Boltzmann constant and thermodynamic entropy collide.** They +agree off the information axis (`forgetInfo k_B = forgetInfo S = E·Θ⁻¹`) but are +distinct dimensions (`k_B` has exponent `-1` on `[I]`, `S` has exponent `0`). So the 5-base SI structure +*cannot* tell `k_B` from an entropy — the Brillouin/Landauer collision, forced. -/ +theorem boltzmann_collides_thermoEntropy : + forgetInfo boltzmann_dim = forgetInfo thermoEntropy_dim ∧ + boltzmann_dim ≠ thermoEntropy_dim := by + refine ⟨by ext <;> simp [boltzmann_dim, thermoEntropy_dim, energy_dim], fun h => ?_⟩ + have := congrArg Dimension.information h + simp [boltzmann_dim, thermoEntropy_dim, energy_dim] at this + +/-- **The general collision criterion.** Any two dimensions that agree off the +information axis but differ on it collide under `forgetInfo` (same image, distinct +sources) — so every information-dependent quantity has a collision partner once `[I]` +is dropped. -/ +theorem collision_of_info_differ {d e : Dimension} + (hoff : forgetInfo d = forgetInfo e) (hinfo : d.information ≠ e.information) : + forgetInfo d = forgetInfo e ∧ d ≠ e := + ⟨hoff, fun h => hinfo (congrArg Dimension.information h)⟩ + +/-! ## Collisions orthogonal to `[I]` (your examples) -/ + +/-- Action `M·L²·T⁻¹`. -/ +def action_dim : Dimension := M𝓭 * L𝓭 ^ (2 : ℚ) * T𝓭⁻¹ + +/-- Angular momentum `r × p = L · (M·L·T⁻¹)`. -/ +def angularMomentum_dim : Dimension := L𝓭 * (M𝓭 * L𝓭 * T𝓭⁻¹) + +/-- Torque `r × F = L · (M·L·T⁻²)`. -/ +def torque_dim : Dimension := L𝓭 * (M𝓭 * L𝓭 * T𝓭 ^ (-2 : ℚ)) + +/-- **Action and angular momentum collide** — both `M·L²·T⁻¹`. This collision is +information-free, so it is present with *and* without `[I]`: the information axis does +not resolve it. -/ +theorem action_eq_angularMomentum : action_dim = angularMomentum_dim := by + ext <;> norm_num [action_dim, angularMomentum_dim] + +/-- **Torque and energy collide** — both `M·L²·T⁻²` — again orthogonal to `[I]`. -/ +theorem torque_eq_energy : torque_dim = energy_dim := by + ext <;> norm_num [torque_dim, energy_dim] + +end Physlib.Units.InformationDimensionCollision + +end diff --git a/QuantumInfo.lean b/QuantumInfo.lean index 6fa9744d9..321977e84 100644 --- a/QuantumInfo.lean +++ b/QuantumInfo.lean @@ -39,6 +39,8 @@ public import QuantumInfo.Entropy.VonNeumann public import QuantumInfo.Entropy.SSA public import QuantumInfo.Entropy.Relative public import QuantumInfo.Entropy.DPI +public import QuantumInfo.Entropy.EntropicProperTime.Basic +public import QuantumInfo.Entropy.EntropicProperTime public import QuantumInfo.States.Mixed.MState public import QuantumInfo.Channels.Pinching public import QuantumInfo.Measurements.POVM diff --git a/QuantumInfo/Entropy/EntropicProperTime.lean b/QuantumInfo/Entropy/EntropicProperTime.lean new file mode 100644 index 000000000..1ad01aa31 --- /dev/null +++ b/QuantumInfo/Entropy/EntropicProperTime.lean @@ -0,0 +1,18 @@ +/- +Copyright (c) 2026 Jorge A. Garcia. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Jorge A. Garcia +-/ +module + +public import QuantumInfo.Entropy.EntropicProperTime.Basic + +/-! +# Entropic proper time (aggregator) + +Re-exports the dimensionless entropic-proper-time core from +`QuantumInfo.Finite.Entropy.EntropicProperTime.Basic`. This path is kept as a +stable import target. It records **no spacetime or units dependencies** — the +dimensional lift and spacetime coupling live in +`Physlib.SpaceAndTime.EntropicProperTime`. +-/ diff --git a/QuantumInfo/Entropy/EntropicProperTime/Basic.lean b/QuantumInfo/Entropy/EntropicProperTime/Basic.lean new file mode 100644 index 000000000..dcca65939 --- /dev/null +++ b/QuantumInfo/Entropy/EntropicProperTime/Basic.lean @@ -0,0 +1,108 @@ +/- +Copyright (c) 2026 Jorge A. Garcia. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Jorge A. Garcia +-/ +module + +public import QuantumInfo.Entropy.Relative +public import QuantumInfo.Entropy.VonNeumann + +@[expose] public section + +noncomputable section + +namespace QuantumInfo.Finite + +open scoped HermitianMat InnerProductSpace RealInnerProductSpace + +variable {d : Type*} [Fintype d] [DecidableEq d] + +/-! +# Entropic proper time (dimensionless core) + +The **entropic proper time** of a state pair is the finite quantum relative +entropy `qRelativeEnt ρ σ`. This file contains only the pure +information-theoretic core — a dimensionless `ENNReal`-valued quantity and its +basic facts — with **no spacetime or units dependencies**, so it is safe to +re-export through `QuantumInfo.Finite.Entropy`. + +The dimensional lift to a metric time and the spacetime coupling live in +`Physlib.SpaceAndTime.EntropicProperTime`. + +## Source and equation map + +* H. Umegaki, *Conditional expectation in an operator algebra. IV. Entropy and information*, + Kodai Mathematical Seminar Reports 14 (1962), 59-85, doi:10.2996/kmj/1138844604. + This is the finite-density-matrix relative entropy used here: + `D(ρ‖σ) = Tr(ρ(log ρ - log σ))`. +* H. Araki, *Relative Entropy of States of von Neumann Algebras*, Publications of the + Research Institute for Mathematical Sciences 11 (1976), 809-833, + doi:10.2977/prims/1195191148. This is the von-Neumann-algebra extension whose + faithful finite-dimensional specialization is the same logarithmic relative entropy. +* A. Connes and C. Rovelli, *Von Neumann algebra automorphisms and time-thermodynamics + relation in generally covariant quantum theories*, Classical and Quantum Gravity 11 + (1994), 2899-2918, doi:10.1088/0264-9381/11/12/007. This branch does **not** identify + `τ_ent` with the Connes-Rovelli modular flow; it uses only the relative-entropy scalar + that later modules scale into a metric time. + +The formal correspondence in this file is: + +* `entropicProperTime ρ σ = qRelativeEnt ρ σ` (`entropicProperTime_eq_qRelativeEnt`); +* `τ_ent(ρ‖ρ) = 0` (`entropicProperTime_self`); +* `τ_ent = -S_vN(ρ) - ⟪ρ, log σ⟫` for nonsingular `σ` + (`entropicProperTime_toReal_modular_form`); +* `0 ≤ τ_ent` as a real number (`entropicProperTime_toReal_nonneg`). +-/ + +/-- Dimensionless **entropic proper time**: the finite quantum relative +entropy of the state pair `(ρ, σ)`. -/ +def entropicProperTime (ρ σ : MState d) : ENNReal := + qRelativeEnt ρ σ + +/-- Definitional reduction: `entropicProperTime = qRelativeEnt`. -/ +theorem entropicProperTime_eq_qRelativeEnt (ρ σ : MState d) : + entropicProperTime ρ σ = qRelativeEnt ρ σ := + rfl + +/-- `entropicProperTime` is a function of the state pair. -/ +theorem entropicProperTime_congr + {ρ σ ρ' σ' : MState d} (hρ : ρ = ρ') (hσ : σ = σ') : + entropicProperTime ρ σ = entropicProperTime ρ' σ' := by + rw [hρ, hσ] + +/-- Vanishing on the diagonal: `τ_ent(ρ‖ρ) = 0`. -/ +@[simp] theorem entropicProperTime_self (ρ : MState d) : + entropicProperTime ρ ρ = 0 := + qRelEntropy_self ρ + +/-- Finiteness under a non-singular reference state. -/ +theorem entropicProperTime_ne_top + {ρ σ : MState d} [σ.M.NonSingular] : + entropicProperTime ρ σ ≠ ⊤ := + qRelativeEnt_ne_top + +/-- Closed (modular) form `τ_ent = -Sᵥₙ(ρ) - ⟪ρ, log σ⟫` under a non-singular +reference state. -/ +theorem entropicProperTime_toReal_modular_form + {ρ σ : MState d} [σ.M.NonSingular] : + (entropicProperTime ρ σ).toReal = + -Sᵥₙ ρ - ⟪ρ.M, σ.M.log⟫ := by + unfold entropicProperTime + have h_ereal : (qRelativeEnt ρ σ : EReal) = + ⟪ρ.M, ρ.M.log - σ.M.log⟫ := qRelativeEnt_rank + have h_real : (qRelativeEnt ρ σ).toReal = + ⟪ρ.M, ρ.M.log - σ.M.log⟫ := by + rw [← EReal.toReal_coe_ennreal, h_ereal] + exact EReal.toReal_coe _ + rw [h_real, inner_sub_right, Sᵥₙ_eq_neg_trace_log, real_inner_comm] + ring + +/-- Non-negativity of the real-valued entropic proper time. -/ +theorem entropicProperTime_toReal_nonneg (ρ σ : MState d) : + 0 ≤ (entropicProperTime ρ σ).toReal := + ENNReal.toReal_nonneg + +end QuantumInfo.Finite + +end