def definition def or abbrev

`default`

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

formal statement (Lean)

  21def default : Flags := {}

proof body

Definition body.

  22
  23end Config
  24end IndisputableMonolith

used by (20)

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

phi_cubed_in_theta_band in IndisputableMonolith.Applied.PhotobiomodulationDevice decl_use
default in IndisputableMonolith.Chemistry.PeriodicTable decl_use
Flags in IndisputableMonolith.Config.Flags decl_use
EmpiricalAnchors in IndisputableMonolith.Constants.ExternalAnchors decl_use
AczelRegularityKernel in IndisputableMonolith.Cost.AczelClassification decl_use
defect_eq_ortho_of_subspace_case in IndisputableMonolith.CPM.LawOfExistence decl_use
gcic_existence_of_global_phase in IndisputableMonolith.Foundation.GlobalCoIdentityConstraint decl_use
canonicalEuclideanEnrichment in IndisputableMonolith.Foundation.SimplicialLedger.InteriorFlat decl_use
defaultEuclideanInterior in IndisputableMonolith.Foundation.SimplicialLedger.InteriorFlat decl_use
FlatInteriorLedger in IndisputableMonolith.Foundation.SimplicialLedger.InteriorFlat decl_use
foldl_add_eq_sum in IndisputableMonolith.Modal.Actualization decl_use
acceptable_all_mono in IndisputableMonolith.PDG.Fits decl_use
f_residue in IndisputableMonolith.Physics.AnchorPolicy decl_use
mixingFromCycles in IndisputableMonolith.RecogSpec.BridgeDerivation decl_use
RSBridge in IndisputableMonolith.RecogSpec.RSBridge decl_use
substrate_ok in IndisputableMonolith.Relativity.ILG.Substrate decl_use
enumOfCountable in IndisputableMonolith.Shims.CountableEquiv decl_use
flags in IndisputableMonolith.VM.State decl_use
MassGap in IndisputableMonolith.YM.OS decl_use
OSPositivity_default in IndisputableMonolith.YM.OS decl_use

depends on (4)

Lean names referenced from this declaration's body.

default in IndisputableMonolith.Chemistry.PeriodicTable decl_use
Flags in IndisputableMonolith.Config.Flags decl_use
Config in IndisputableMonolith.Gravity.ILG decl_use
Config in IndisputableMonolith.Modal.Possibility decl_use