theorem proved term proof

`self_similar_forces_golden_constraint`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

 151theorem self_similar_forces_golden_constraint (S : SelfSimilar) :
 152    satisfies_golden_constraint S.ratio := by

proof body

Term-mode proof.

 153  rcases S.scale_invariant with ⟨G, hratio, hclosed⟩
 154  unfold satisfies_golden_constraint
 155  rw [← hratio]
 156  exact PhiForcingDerived.closure_forces_golden_equation G hclosed
 157
 158/-- φ satisfies the golden constraint. -/

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

phi_forced in IndisputableMonolith.Foundation.PhiForcing decl_use

depends on (8)

Lean names referenced from this declaration's body.

G in IndisputableMonolith.Constants decl_use
G in IndisputableMonolith.Constants.Codata decl_use
G in IndisputableMonolith.Cost.FunctionalEquation decl_use
satisfies_golden_constraint in IndisputableMonolith.Foundation.PhiForcing decl_use
SelfSimilar in IndisputableMonolith.Foundation.PhiForcing decl_use
closure_forces_golden_equation in IndisputableMonolith.Foundation.PhiForcingDerived decl_use
G in IndisputableMonolith.Gravity.JCostInflaton decl_use
S in IndisputableMonolith.Relativity.ILG.Action decl_use