No prose has been written for this declaration yet. The Lean source and graph data below render
without it.
generate prose now
formal statement (Lean)
97theorem p_preserves_cost (e : LedgerEntry) :
98 (applyP e).cost = e.cost := rfl
proof body
Term-mode proof.
99
100/-! ## T Symmetry: Time Reversal from 8-Tick Reversal -/
101
102/-- Reverse a tick in the 8-tick cycle: t ↦ 7 - t (mod 8). -/
depends on (15)
Lean names referenced from this declaration's body.
-
tick
in IndisputableMonolith.Constants
decl_use
-
tick
in IndisputableMonolith.Constants.RSNativeUnits
decl_use
-
Time
in IndisputableMonolith.Constants.RSNativeUnits
decl_use
-
T
in IndisputableMonolith.Foundation.Breath1024
decl_use
-
cost
in IndisputableMonolith.Foundation.MultiplicativeRecognizerL4
decl_use
-
cost
in IndisputableMonolith.Foundation.ObserverForcing
decl_use
-
from
in IndisputableMonolith.Foundation.PrimitiveDistinction
decl_use
-
LedgerEntry
in IndisputableMonolith.Foundation.QuantumLedger
decl_use
-
Tick
in IndisputableMonolith.Foundation.TimeEmergence
decl_use
-
T
in IndisputableMonolith.Gap45.SyncMinimization
decl_use
-
Tick
in IndisputableMonolith.Masses.Ribbons
decl_use
-
Tick
in IndisputableMonolith.Masses.Ribbons.Tick
decl_use
-
Tick
in IndisputableMonolith.Measurement.RSNative.Core
decl_use
-
applyP
in IndisputableMonolith.QFT.CPTInvariance
decl_use
-
LedgerEntry
in IndisputableMonolith.QFT.CPTInvariance
decl_use