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)
150def visualBeautyCert : VisualBeautyCert where
151 symmetric_max := beautyScore_at_one
proof body
Definition body.
152 golden_ratio_score := beautyScore_at_phi
153 Jphi_band := Jphi_numerical_band
154 rule_of_thirds_eq_45 := ruleOfThirds_lattice_period_eq
155 cortical_lattice_match := rfl
156
157/-! ## §5. Single-statement summary -/
158
159/-- **VISUAL BEAUTY: ONE-STATEMENT THEOREM.**
160
161 Beauty score `B(a, b) = −J(a/b)`:
162 (1) `B(a, a) = 0` for any `a ≠ 0` (perfect symmetry).
163 (2) `B(φ, 1) = 3/2 − φ ≈ −0.118` (golden-ratio composition).
164 (3) `J(φ) ∈ (0.11, 0.12)` (numerical band).
165 (4) Rule-of-thirds lattice = 45 (the consciousness gap). -/
depends on (18)
Lean names referenced from this declaration's body.
-
beautyScore_at_one
in IndisputableMonolith.Aesthetics.VisualBeauty
decl_use
-
beautyScore_at_phi
in IndisputableMonolith.Aesthetics.VisualBeauty
decl_use
-
Jphi_numerical_band
in IndisputableMonolith.Aesthetics.VisualBeauty
decl_use
-
ruleOfThirds_lattice_period_eq
in IndisputableMonolith.Aesthetics.VisualBeauty
decl_use
-
VisualBeautyCert
in IndisputableMonolith.Aesthetics.VisualBeauty
decl_use
-
of
in IndisputableMonolith.Astrophysics.NucleosynthesisTiers
decl_use
-
score
in IndisputableMonolith.Ethics.CostModel
decl_use
-
of
in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization
decl_use
-
of
in IndisputableMonolith.Foundation.PhiForcingDerived
decl_use
-
band
in IndisputableMonolith.Foundation.PreLogicalCost
decl_use
-
of
in IndisputableMonolith.Foundation.SpectralEmergence
decl_use
-
for
in IndisputableMonolith.Foundation.UniversalForcingSelfReference
decl_use
-
gap
in IndisputableMonolith.Gap45.Derivation
decl_use
-
of
in IndisputableMonolith.Information.PhysicsComplexityStructure
decl_use
-
gap
in IndisputableMonolith.Masses.AnchorPolicy
decl_use
-
gap
in IndisputableMonolith.Masses.RSBridge.Anchor
decl_use
-
score
in IndisputableMonolith.Measurement
decl_use
-
gap
in IndisputableMonolith.RSBridge.Anchor
decl_use