pith. machine review for the scientific record. sign in

IndisputableMonolith.Chemistry.EnvPressure

IndisputableMonolith/Chemistry/EnvPressure.lean · 32 lines · 3 declarations

show as:
view math explainer →

open module explainer GitHub source

Explainer status: pending

   1import Mathlib
   2import IndisputableMonolith.Constants
   3
   4/-!
   5# Environment Display Rescale (scaffold)
   6
   7Display-only rescale for environment-dependent observables: E → E · φ^{β P},
   8leaving integer scaffolding intact. β is a fixed constant determined by
   9neutrality tests; this file exposes helpers and diagnostics only.
  10-/
  11
  12namespace IndisputableMonolith
  13namespace Chemistry
  14namespace EnvPressure
  15
  16open scoped Real
  17
  18/‑ Environment scale factor: φ^{β P}. -/
  19def scaleFactor (beta P : ℝ) : ℝ :=
  20  Real.rpow IndisputableMonolith.Constants.phi (beta * P)
  21
  22/‑ Display rescale: E' = E · φ^{β P}. -/
  23def rescaleEnergy (E beta P : ℝ) : ℝ := E * scaleFactor beta P
  24
  25/‑ Eight-window neutrality diagnostic on a display observable stream x. -/
  26def neutral8 (x : ℕ → ℝ) (t0 : ℕ) : ℝ :=
  27  (Finset.range 8).sum (fun i => x (t0 + i))
  28
  29end EnvPressure
  30end Chemistry
  31end IndisputableMonolith
  32

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