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)
120noncomputable def G_derived (c hbar lambda_rec : ℝ) : ℝ :=
proof body
Definition body.
121 Real.pi * c^3 * lambda_rec^2 / hbar
122
123/-! ## The K-Gate Identity -/
124
125/-- K = 2π / (8 ln φ) — the universal dimensionless ratio.
126
127This ratio appears in:
128- τ_rec / τ₀ = K
129- λ_kin / ℓ₀ = K
130-/
used by (3)
From the project-wide theorem graph. These declarations reference this one in their body.
depends on (11)
Lean names referenced from this declaration's body.
-
lambda_rec
in IndisputableMonolith.Bridge.DataCore
decl_use
-
Gate
in IndisputableMonolith.Complexity.CircuitLedger
decl_use
-
hbar
in IndisputableMonolith.Constants
decl_use
-
K
in IndisputableMonolith.Constants
decl_use
-
lambda_rec
in IndisputableMonolith.Constants
decl_use
-
hbar
in IndisputableMonolith.Constants.Codata
decl_use
-
G_derived
in IndisputableMonolith.Constants.Derivation
decl_use
-
K
in IndisputableMonolith.Constants.LambdaRecDerivation
decl_use
-
Identity
in IndisputableMonolith.Foundation.LogicAsFunctionalEquation
decl_use
-
hbar
in IndisputableMonolith.Information.ComputationLimitsStructure
decl_use
-
hbar
in IndisputableMonolith.Quantum.EntanglementEntropy
decl_use