`IndisputableMonolith.TruthCore.TimeKernel`

IndisputableMonolith/TruthCore/TimeKernel.lean · 16 lines · 1 declarations

Explainer status: pending

   1import Mathlib
   2import IndisputableMonolith.Gravity.ILG
   3
   4namespace IndisputableMonolith
   5namespace TruthCore
   6
   7/-- Alias: time-kernel ratio is dimensionless (invariant under common rescaling). -/
   8theorem time_kernel_dimensionless (c T τ : ℝ) (hc : 0 < c) :
   9  IndisputableMonolith.Gravity.ILG.w_time_ratio (c * T) (c * τ)
  10    = IndisputableMonolith.Gravity.ILG.w_time_ratio T τ := by
  11  simpa using IndisputableMonolith.Gravity.ILG.w_time_ratio_rescale (c:=c) (Tdyn:=T) (τ0:=τ) hc
  12
  13end TruthCore
  14end IndisputableMonolith
  15
  16

source mirrored from github.com/jonwashburn/shape-of-logic