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)
349theorem hbar_action_identity : hbar = E_coh * tau0 := rfl
proof body
Term-mode proof.
350
351/-- **THEOREM C-004.5**: Bounds on ℏ from φ bounds.
352
353 With φ ∈ (1.61, 1.62), we get ℏ ∈ (0.088, 0.093). -/
depends on (9)
Lean names referenced from this declaration's body.
-
tau0
in IndisputableMonolith.Compat.Constants
decl_use
-
hbar
in IndisputableMonolith.Constants
decl_use
-
tau0
in IndisputableMonolith.Constants
decl_use
-
hbar
in IndisputableMonolith.Constants.Codata
decl_use
-
tau0
in IndisputableMonolith.Constants.Derivation
decl_use
-
from
in IndisputableMonolith.Foundation.PrimitiveDistinction
decl_use
-
hbar
in IndisputableMonolith.Information.ComputationLimitsStructure
decl_use
-
hbar
in IndisputableMonolith.Quantum.EntanglementEntropy
decl_use
-
get
in IndisputableMonolith.RRF.Core.Vantage
decl_use