def definition def or abbrev

`reparamDiagonal`

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

formal statement (Lean)

  28def reparamDiagonal (s : ℝ) : ℝ :=

proof body

Definition body.

  29  4 * s + 18 * s^2 + 16 * s^3 + 4 * s^4
  30
  31/-- The diagonal of any degree-2 RCL-family combiner with boundary
  32`Phi(a,0)=2a`, written in the same local coordinate `a=s+s^2`. -/

used by (4)

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

reparam_coefficients_obstruct_degree_two in IndisputableMonolith.Foundation.LogicAsFunctionalEquation.AnalyticCounterexample decl_use
reparam_diagonal_not_degree_two in IndisputableMonolith.Foundation.LogicAsFunctionalEquation.AnalyticCounterexample decl_use
analytic_reparameterization_not_counted_once in IndisputableMonolith.Foundation.LogicAsFunctionalEquation.CountOnceComparison decl_use
analytic_composition_not_enough in IndisputableMonolith.Foundation.LogicAsFunctionalEquation.FiniteLogicalComparison decl_use

depends on (7)

Lean names referenced from this declaration's body.

of in IndisputableMonolith.Astrophysics.NucleosynthesisTiers decl_use
Phi in IndisputableMonolith.Cost.AczelProof decl_use
Phi in IndisputableMonolith.Cost.AczelTheorem decl_use
of in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization decl_use
of in IndisputableMonolith.Foundation.PhiForcingDerived decl_use
of in IndisputableMonolith.Foundation.SpectralEmergence decl_use
of in IndisputableMonolith.Information.PhysicsComplexityStructure decl_use