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)
213theorem phi_forced (L : DiscreteLedger) (r : ℝ) (hr : is_self_similar L r) : r = φ := by
proof body
Term-mode proof.
214 rcases hr with ⟨S, rfl⟩
215 exact golden_constraint_unique S.ratio_pos (self_similar_forces_golden_constraint S)
216
217/-! ## Consequences of φ -/
218
219/-- The minimum non-trivial cost: J_bit = ln(φ). -/
used by (3)
From the project-wide theorem graph. These declarations reference this one in their body.
depends on (14)
Lean names referenced from this declaration's body.
-
of
in IndisputableMonolith.Astrophysics.NucleosynthesisTiers
decl_use
-
of
in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization
decl_use
-
cost
in IndisputableMonolith.Foundation.MultiplicativeRecognizerL4
decl_use
-
cost
in IndisputableMonolith.Foundation.ObserverForcing
decl_use
-
DiscreteLedger
in IndisputableMonolith.Foundation.PhiForcing
decl_use
-
golden_constraint_unique
in IndisputableMonolith.Foundation.PhiForcing
decl_use
-
is_self_similar
in IndisputableMonolith.Foundation.PhiForcing
decl_use
-
self_similar_forces_golden_constraint
in IndisputableMonolith.Foundation.PhiForcing
decl_use
-
of
in IndisputableMonolith.Foundation.PhiForcingDerived
decl_use
-
of
in IndisputableMonolith.Foundation.SpectralEmergence
decl_use
-
of
in IndisputableMonolith.Information.PhysicsComplexityStructure
decl_use
-
L
in IndisputableMonolith.Recognition
decl_use
-
L
in IndisputableMonolith.Recognition.Cycle3
decl_use
-
S
in IndisputableMonolith.Relativity.ILG.Action
decl_use