IndisputableMonolith.Chemistry.EnvPressure
IndisputableMonolith/Chemistry/EnvPressure.lean · 32 lines · 3 declarations
show as:
view math explainer →
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