def definition def or abbrev

`cert`

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

formal statement (Lean)

 102noncomputable def cert : GoldenSectionCert where
 103  ratio_gt_one := preferredAspectRatio_gt_one

proof body

Definition body.

 104  ratio_in_band := preferredAspectRatio_in_aesthetic_band
 105  golden_recursion := phi_golden_recursion
 106  cost_at_ideal := proportionCost_at_ideal
 107  cost_nonneg := proportionCost_nonneg
 108

depends on (7)

Lean names referenced from this declaration's body.

GoldenSectionCert in IndisputableMonolith.Architecture.GoldenSectionInProportion decl_use
phi_golden_recursion in IndisputableMonolith.Architecture.GoldenSectionInProportion decl_use
preferredAspectRatio_gt_one in IndisputableMonolith.Architecture.GoldenSectionInProportion decl_use
preferredAspectRatio_in_aesthetic_band in IndisputableMonolith.Architecture.GoldenSectionInProportion decl_use
proportionCost_at_ideal in IndisputableMonolith.Architecture.GoldenSectionInProportion decl_use
proportionCost_nonneg in IndisputableMonolith.Architecture.GoldenSectionInProportion decl_use
cost_nonneg in IndisputableMonolith.Foundation.ObserverForcing decl_use