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)
86theorem residual_action_invariant (rot : TwoBranchRotation) :
87 residualAction rot = π/2 - rot.θ_s := rfl
proof body
Term-mode proof.
88
89end Measurement
90end IndisputableMonolith
depends on (5)
Lean names referenced from this declaration's body.
-
Measurement
in IndisputableMonolith.Data.Import
decl_use
-
Measurement
in IndisputableMonolith.Measurement.RSNative.Core
decl_use
-
residualAction
in IndisputableMonolith.Measurement.TwoBranchGeodesic
decl_use
-
TwoBranchRotation
in IndisputableMonolith.Measurement.TwoBranchGeodesic
decl_use
-
Measurement
in IndisputableMonolith.Quantum.NonlocalityNoSignaling
decl_use