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)
87theorem c_preserves_cost (e : LedgerEntry) :
88 (applyC e).cost = e.cost := rfl
proof body
Term-mode proof.
89
90/-! ## P Symmetry: Parity from Voxel Reflection -/
91
92/-- Apply parity (spatial reflection) to a ledger entry. -/
depends on (8)
Lean names referenced from this declaration's body.
-
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
-
parity
in IndisputableMonolith.LedgerPostingAdjacency
decl_use
-
Voxel
in IndisputableMonolith.Measurement.RSNative.Core
decl_use
-
applyC
in IndisputableMonolith.QFT.CPTInvariance
decl_use
-
LedgerEntry
in IndisputableMonolith.QFT.CPTInvariance
decl_use