structure definition def or abbrev

`Phys`

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

formal statement (Lean)

  17structure Phys where
  18  G : ℝ
  19  deriving Repr
  20
  21/- Generic kernel placeholder `W` (the ILG kernel `w(k,a)`). -/

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

is in IndisputableMonolith.Foundation.SimplicialLedger.EdgeLengthFromPsi decl_use
effectiveSource in IndisputableMonolith.ILG.PressureForm decl_use
effectiveSource_pressure in IndisputableMonolith.ILG.PressureForm decl_use
source_equiv in IndisputableMonolith.ILG.PressureForm decl_use
metric_matrix_invertible_at in IndisputableMonolith.Relativity.Geometry.DiscreteBridge decl_use

Lean names referenced from this declaration's body.

G in IndisputableMonolith.Constants decl_use
G in IndisputableMonolith.Constants.Codata decl_use
kernel in IndisputableMonolith.Cosmology.BITKernelFamilies decl_use
G in IndisputableMonolith.Cost.FunctionalEquation decl_use
G in IndisputableMonolith.Gravity.JCostInflaton decl_use
kernel in IndisputableMonolith.ILG.Kernel decl_use
W in IndisputableMonolith.Masses.Anchor decl_use
W in IndisputableMonolith.Physics.LeptonGenerations.TauStepDerivation decl_use
W in IndisputableMonolith.Physics.MassTopology decl_use