from

used by (40)

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

• SpeechIntelligibilityCert in IndisputableMonolith.Acoustics.SpeechIntelligibilityFromJCost decl_use
• applied in IndisputableMonolith.Action.EnergyConservationDomainCert decl_use
• costRateEL_const_one in IndisputableMonolith.Action.EulerLagrange decl_use
• actionJ_local_min_is_global in IndisputableMonolith.Action.FunctionalConvexity decl_use
• Jcost_convex_combination in IndisputableMonolith.Action.FunctionalConvexity decl_use
• hamilton_equations_from_EL in IndisputableMonolith.Action.Hamiltonian decl_use
• hamiltonPDotEquation in IndisputableMonolith.Action.Hamiltonian decl_use
• standardHamiltonian in IndisputableMonolith.Action.Hamiltonian decl_use
• spaceTranslationFlow in IndisputableMonolith.Action.Noether decl_use
• timeTranslationFlow in IndisputableMonolith.Action.Noether decl_use
• Jcost_taylor_quadratic in IndisputableMonolith.Action.QuadraticLimit decl_use
• newton_first_law in IndisputableMonolith.Action.QuadraticLimit decl_use
• standardEL in IndisputableMonolith.Action.QuadraticLimit decl_use
• booker_count_eq_F2Power3_nonzero in IndisputableMonolith.Aesthetics.NarrativeGeodesic decl_use
• booker_seven_eq_2_pow_3_minus_1 in IndisputableMonolith.Aesthetics.NarrativeGeodesic decl_use
• narrativeGeodesicCert in IndisputableMonolith.Aesthetics.NarrativeGeodesic decl_use
• three_act_resolution_below_climax in IndisputableMonolith.Aesthetics.NarrativeGeodesic decl_use
• Jcost_anti_mono_on_unit_interval in IndisputableMonolith.Aesthetics.SymmetryGroupPreference decl_use
• preference_anti_mono_in_orbits in IndisputableMonolith.Aesthetics.SymmetryGroupPreference decl_use
• WallpaperGroup in IndisputableMonolith.Aesthetics.SymmetryGroupPreference decl_use
• beautyScore_at_phi in IndisputableMonolith.Aesthetics.VisualBeauty decl_use
• Jphi_numerical_band in IndisputableMonolith.Aesthetics.VisualBeauty decl_use
• costCompose_left_cancel in IndisputableMonolith.Algebra.CostAlgebra decl_use
• defectDist_le_J_of_ratio_bounds in IndisputableMonolith.Algebra.CostAlgebra decl_use
• H_dAlembert in IndisputableMonolith.Algebra.CostAlgebra decl_use
• RecognitionCostSystem in IndisputableMonolith.Algebra.CostAlgebra decl_use
• seqShift in IndisputableMonolith.Algebra.CostAlgebra decl_use
• shiftedHValueOf in IndisputableMonolith.Algebra.CostAlgebra decl_use
• windowSums_shift_equivariant in IndisputableMonolith.Algebra.CostAlgebra decl_use
• axis123_weight in IndisputableMonolith.Algebra.F2Power decl_use

… and 10 more