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)
123theorem J_phi : LawOfExistence.J φ = φ - 3/2 := by
proof body
Term-mode proof.
124 simp only [LawOfExistence.J]
125 rw [phi_inv]
126 ring
127
128/-! ## Self-Similarity -/
129
130/-- A self-similar structure with scale ratio r. -/
used by (3)
From the project-wide theorem graph. These declarations reference this one in their body.
-
J_phi
in IndisputableMonolith.Foundation.SpectralEmergence
decl_use
-
J_phi_pos
in IndisputableMonolith.Foundation.SpectralEmergence
decl_use
-
phi_cost_eq
in IndisputableMonolith.Foundation.StillnessGenerative
decl_use
depends on (10)
Lean names referenced from this declaration's body.
-
phi_inv
in IndisputableMonolith.Algebra.PhiRing
decl_use
-
scale
in IndisputableMonolith.Cosmology.LargeScaleStructureFromRS
decl_use
-
phi_inv
in IndisputableMonolith.Foundation.Inequalities
decl_use
-
A
in IndisputableMonolith.Foundation.IntegrationGap
decl_use
-
phi_inv
in IndisputableMonolith.Foundation.PhiForcing
decl_use
-
J_phi
in IndisputableMonolith.Foundation.SpectralEmergence
decl_use
-
phi_inv
in IndisputableMonolith.Linguistics.LexiconRatio
decl_use
-
A
in IndisputableMonolith.Masses.Anchor
decl_use
-
A
in IndisputableMonolith.Modal.Actualization
decl_use
-
self
in IndisputableMonolith.RecogSpec.Core
decl_use