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)
82theorem parameters_from_phi :
83 alpha_locked = (1 - 1/phi) / 2 ∧
84 upsilon_locked = phi ∧
85 clag_locked = phi ^ (-(5 : ℝ)) := by
proof body
Term-mode proof.
86 unfold alpha_locked upsilon_locked clag_locked alphaLock cLagLock
87 exact ⟨rfl, rfl, rfl⟩
88
89/-- The number of per-galaxy free parameters is exactly zero. -/
used by (2)
From the project-wide theorem graph. These declarations reference this one in their body.
depends on (16)
Lean names referenced from this declaration's body.
-
of
in IndisputableMonolith.Astrophysics.NucleosynthesisTiers
decl_use
-
alphaLock
in IndisputableMonolith.Constants
decl_use
-
cLagLock
in IndisputableMonolith.Constants
decl_use
-
alpha_locked
in IndisputableMonolith.Constants.ILG
decl_use
-
of
in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization
decl_use
-
is
in IndisputableMonolith.Foundation.OptionAEmpiricalProgram
decl_use
-
of
in IndisputableMonolith.Foundation.PhiForcingDerived
decl_use
-
is
in IndisputableMonolith.Foundation.SimplicialLedger.EdgeLengthFromPsi
decl_use
-
of
in IndisputableMonolith.Foundation.SpectralEmergence
decl_use
-
is
in IndisputableMonolith.GameTheory.MechanismDesignFromSigma
decl_use
-
alpha_locked
in IndisputableMonolith.Gravity.SPARCFalsifier
decl_use
-
clag_locked
in IndisputableMonolith.Gravity.SPARCFalsifier
decl_use
-
upsilon_locked
in IndisputableMonolith.Gravity.SPARCFalsifier
decl_use
-
of
in IndisputableMonolith.Information.PhysicsComplexityStructure
decl_use
-
is
in IndisputableMonolith.Mathematics.RamanujanBridge.MockThetaPhantom
decl_use
-
alpha_locked
in IndisputableMonolith.Physics.CouplingLockIn
decl_use