def definition def or abbrev

`rrfFormalizationOctave`

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

formal statement (Lean)

 112def rrfFormalizationOctave : FormalizationAsOctave := {

proof body

Definition body.

 113  octave_type := "logical",
 114  strain := fun c => c.source.length,  -- Simplistic: length as complexity
 115  elegance := fun c => 1.0 / (c.source.length : ℝ)
 116}
 117
 118
 119/-! ## Fixed Point Structure -/
 120
 121/-- A fixed point: the description describes itself accurately. -/

depends on (8)

Lean names referenced from this declaration's body.

Structure in IndisputableMonolith.Chemistry.CrystalStructure decl_use
A in IndisputableMonolith.Foundation.IntegrationGap decl_use
as in IndisputableMonolith.Foundation.SimplicialLedger.ContinuumBridge decl_use
A in IndisputableMonolith.Masses.Anchor decl_use
A in IndisputableMonolith.Modal.Actualization decl_use
point in IndisputableMonolith.Numerics.Interval.Basic decl_use
Point in IndisputableMonolith.Relativity.Geometry.Manifold decl_use
FormalizationAsOctave in IndisputableMonolith.RRF.Foundation.SelfReference decl_use