def definition def or abbrev

`Defect`

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

formal statement (Lean)

  17def Defect (src : String) : Nat := if Structured src then 0 else 1

proof body

Definition body.

  18
  19end CPM
  20end IndisputableMonolith

used by (40)

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

defectDist in IndisputableMonolith.Algebra.CostAlgebra decl_use
defectDist_nonneg in IndisputableMonolith.Algebra.CostAlgebra decl_use
defectDist_self in IndisputableMonolith.Algebra.CostAlgebra decl_use
defectDist_symm in IndisputableMonolith.Algebra.CostAlgebra decl_use
J_nonneg in IndisputableMonolith.Algebra.CostAlgebra decl_use
shiftedHValueOf in IndisputableMonolith.Algebra.CostAlgebra decl_use
Hypothesis in IndisputableMonolith.ClassicalBridge.Fluids.CPM2D decl_use
poly_circuit_poly_capacity in IndisputableMonolith.Complexity.CircuitLedger decl_use
cosmological_constant_resolution in IndisputableMonolith.Cosmology.EarlyUniverse decl_use
Model in IndisputableMonolith.CPM.LawOfExistence decl_use
defect_must_be_small in IndisputableMonolith.Experimental.ANITAUpgoing decl_use
cost_stability_calibrated in IndisputableMonolith.Foundation.DAlembert.Stability decl_use
defect_symmetric in IndisputableMonolith.Foundation.DAlembert.Stability decl_use
discrete_minimum_stable in IndisputableMonolith.Foundation.DiscretenessForcing decl_use
unity_unique_minimizer in IndisputableMonolith.Foundation.InitialCondition decl_use
defect in IndisputableMonolith.Foundation.LawOfExistence decl_use
defect_at_one in IndisputableMonolith.Foundation.LawOfExistence decl_use
DefectCollapse in IndisputableMonolith.Foundation.LawOfExistence decl_use
defect_one in IndisputableMonolith.Foundation.LawOfExistence decl_use
Exists in IndisputableMonolith.Foundation.LawOfExistence decl_use
logic_from_cost in IndisputableMonolith.Foundation.LogicFromCost decl_use
rung_separation in IndisputableMonolith.Foundation.SpectralEmergence decl_use
before in IndisputableMonolith.Foundation.TimeEmergence decl_use
variational_dynamics_certificate in IndisputableMonolith.Foundation.VariationalDynamics decl_use
variational_dynamics_deterministic in IndisputableMonolith.Foundation.VariationalDynamics decl_use
variational_step_unique in IndisputableMonolith.Foundation.VariationalDynamics decl_use
ExternalPhaseField in IndisputableMonolith.Gravity.AcousticPhaseLevitation decl_use
C_proj_value in IndisputableMonolith.Gravity.CoerciveProjection decl_use
coherence_defect_simplify in IndisputableMonolith.Gravity.CoherenceFall decl_use
total_potential_in_frame in IndisputableMonolith.Gravity.CoherenceFall decl_use

… and 10 more

depends on (1)

Lean names referenced from this declaration's body.

Structured in IndisputableMonolith.CPM.LNALBridge decl_use