def definition def or abbrev

`total`

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

formal statement (Lean)

  70def total (E : ErrorBudget) : ℝ := E.det2Err + E.tailErr + E.winErr

proof body

Definition body.

used by (40)

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

applied in IndisputableMonolith.Action.EnergyConservationDomainCert decl_use
energyConservationCert in IndisputableMonolith.Action.EnergyConservationDomainCert decl_use
hamilton_equations_from_EL in IndisputableMonolith.Action.Hamiltonian decl_use
totalEnergy in IndisputableMonolith.Action.Hamiltonian decl_use
spaceTranslationFlow in IndisputableMonolith.Action.Noether decl_use
space_translation_invariance_implies_momentum_conservation in IndisputableMonolith.Action.Noether decl_use
timeTranslationFlow in IndisputableMonolith.Action.Noether decl_use
DoubleEntryAlgebra in IndisputableMonolith.Algebra.LedgerAlgebra decl_use
StellarConfig in IndisputableMonolith.Astrophysics.StellarAssembly decl_use
uncatalyzedBarrier in IndisputableMonolith.Chemistry.EnzymeCatalysis decl_use
H_SATTMRuntime in IndisputableMonolith.Complexity.CellularAutomata decl_use
sat_computation_time in IndisputableMonolith.Complexity.CellularAutomata decl_use
tm_simulation_bound in IndisputableMonolith.Complexity.CellularAutomata decl_use
CircuitDecides in IndisputableMonolith.Complexity.CircuitLedger decl_use
p_neq_np_conditional in IndisputableMonolith.Complexity.CircuitLowerBound decl_use
consistent in IndisputableMonolith.Complexity.SAT.Backprop decl_use
completeStateFrom in IndisputableMonolith.Complexity.SAT.Completeness decl_use
twoSystems_length in IndisputableMonolith.Complexity.SAT.SmallBias decl_use
cone_bound_export in IndisputableMonolith.ConeExport.Theorem decl_use
active_edges_per_tick in IndisputableMonolith.Constants.AlphaDerivation decl_use
gauss_bonnet_Q3 in IndisputableMonolith.Constants.AlphaDerivation decl_use
geometric_seed_factor_eq_11 in IndisputableMonolith.Constants.AlphaDerivation decl_use
passive_edges_at_D3 in IndisputableMonolith.Constants.AlphaDerivation decl_use
per_face_solid_angle_eq in IndisputableMonolith.Constants.AlphaDerivation decl_use
vertex_deficit_eq in IndisputableMonolith.Constants.AlphaDerivation decl_use
active_edges in IndisputableMonolith.Constants.AlphaHigherOrder decl_use
angular_contribution_per_dim in IndisputableMonolith.Constants.CurvatureSpaceDerivation decl_use
balance_constraint_codim_1 in IndisputableMonolith.Constants.CurvatureSpaceDerivation decl_use
balance_determines_lambda in IndisputableMonolith.Constants.LambdaRecDerivation decl_use
lambda_rec_is_forced in IndisputableMonolith.Constants.LambdaRecDerivation decl_use

… and 10 more

depends on (3)

Lean names referenced from this declaration's body.

E in IndisputableMonolith.Foundation.SpectralEmergence decl_use
total in IndisputableMonolith.NavierStokes.DiscreteVorticity decl_use
ErrorBudget in IndisputableMonolith.NumberTheory.RiemannHypothesis.ErrorBudget decl_use