def definition def or abbrev

`beta`

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

formal statement (Lean)

  15noncomputable def beta  (_C_lag _α : ℝ) : ℝ := 1

proof body

Definition body.

  16
  17/-- PPN γ definition (for paper reference). -/

used by (40)

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

cubicConstraint in IndisputableMonolith.Chemistry.CrystalSymmetry decl_use
hexagonalConstraint in IndisputableMonolith.Chemistry.CrystalSymmetry decl_use
LatticeParams in IndisputableMonolith.Chemistry.CrystalSymmetry decl_use
orthorhombicConstraint in IndisputableMonolith.Chemistry.CrystalSymmetry decl_use
tetragonalConstraint in IndisputableMonolith.Chemistry.CrystalSymmetry decl_use
trigonalConstraint in IndisputableMonolith.Chemistry.CrystalSymmetry decl_use
rescaleEnergy in IndisputableMonolith.Chemistry.EnvPressure decl_use
scaleFactor in IndisputableMonolith.Chemistry.EnvPressure decl_use
tritium_concentration in IndisputableMonolith.Experimental.Xenon1TExcess decl_use
a_baryon_keplerian in IndisputableMonolith.Gravity.BTFREmergence decl_use
btfr_mass_velocity_relation in IndisputableMonolith.Gravity.BTFREmergence decl_use
btfr_slope_deep in IndisputableMonolith.Gravity.BTFREmergence decl_use
btfr_slope_naive in IndisputableMonolith.Gravity.BTFREmergence decl_use
f_growth in IndisputableMonolith.Gravity.ILGGrowthFactor decl_use
G_ratio_at_self_lt_31 in IndisputableMonolith.Gravity.RunningG decl_use
G_ratio_at_self_pos in IndisputableMonolith.Gravity.RunningG decl_use
grav_casimir_ratio_negligible in IndisputableMonolith.Gravity.RunningG decl_use
H_GravitationalRunning_certificate in IndisputableMonolith.Gravity.RunningG decl_use
r_ref_exact_gt_r in IndisputableMonolith.Gravity.RunningG decl_use
r_ref_exact_pos in IndisputableMonolith.Gravity.RunningG decl_use
beta_running_derived in IndisputableMonolith.Gravity.RunningGDerivation decl_use
voxel_density_scaling in IndisputableMonolith.Gravity.RunningGDerivation decl_use
CausalClosureForced in IndisputableMonolith.Papers.DIF.CausalClosure decl_use
syncPeriod_3_eq_360 in IndisputableMonolith.Papers.DraftV1 decl_use
stationary_at_anchor in IndisputableMonolith.Physics.AnchorPolicy decl_use
all_harmonics_match in IndisputableMonolith.Physics.EarthBrainResonance decl_use
EarthBrainResonanceCert in IndisputableMonolith.Physics.EarthBrainResonance decl_use
FalsificationCriteria in IndisputableMonolith.Physics.EarthBrainResonance decl_use
fundamental_near_theta_alpha_boundary in IndisputableMonolith.Physics.EarthBrainResonance decl_use
harmonic2_in_beta in IndisputableMonolith.Physics.EarthBrainResonance decl_use

… and 10 more

depends on (2)

Lean names referenced from this declaration's body.

for in IndisputableMonolith.Foundation.UniversalForcingSelfReference decl_use
beta in IndisputableMonolith.Thermodynamics.PartitionFunction decl_use