structure definition def or abbrev

`BridgeData`

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

formal statement (Lean)

  20structure BridgeData where
  21  G     : ℝ
  22  hbar  : ℝ
  23  c     : ℝ
  24  tau0  : ℝ
  25  ell0  : ℝ
  26
  27/-- Minimal physical assumptions on bridge anchors reused by analytical lemmas. -/

used by (8)

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

lambda_rec in IndisputableMonolith.Bridge.DataCore decl_use
lambda_rec_dimensionless_id in IndisputableMonolith.Bridge.DataCore decl_use
lambda_rec_dimensionless_id_physical in IndisputableMonolith.Bridge.DataCore decl_use
lambda_rec_pos in IndisputableMonolith.Bridge.DataCore decl_use
Physical in IndisputableMonolith.Bridge.DataCore decl_use
BridgeData in IndisputableMonolith.Gravity.ILG decl_use
w_t_display in IndisputableMonolith.Gravity.ILG decl_use
ILG_w_t_display in IndisputableMonolith.TruthCore.ILGDisplay decl_use

depends on (15)

Lean names referenced from this declaration's body.

bridge in IndisputableMonolith.ClassicalBridge.Fluids.CPM2D decl_use
tau0 in IndisputableMonolith.Compat.Constants decl_use
ell0 in IndisputableMonolith.Constants decl_use
G in IndisputableMonolith.Constants decl_use
hbar in IndisputableMonolith.Constants decl_use
tau0 in IndisputableMonolith.Constants decl_use
G in IndisputableMonolith.Constants.Codata decl_use
hbar in IndisputableMonolith.Constants.Codata decl_use
ell0 in IndisputableMonolith.Constants.Derivation decl_use
tau0 in IndisputableMonolith.Constants.Derivation decl_use
G in IndisputableMonolith.Cost.FunctionalEquation decl_use
BridgeData in IndisputableMonolith.Gravity.ILG decl_use
G in IndisputableMonolith.Gravity.JCostInflaton decl_use
hbar in IndisputableMonolith.Information.ComputationLimitsStructure decl_use
hbar in IndisputableMonolith.Quantum.EntanglementEntropy decl_use