carrier — Recognition explainer

formal statement (Lean)

  33def carrier : ℝ := 5 * phi

proof body

Definition body.

used by (40)

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

H_dAlembert in IndisputableMonolith.Algebra.CostAlgebra decl_use
admissibleFlows in IndisputableMonolith.Algebra.RecognitionCategory decl_use
canonicalLedgerAlgObj in IndisputableMonolith.Algebra.RecognitionCategory decl_use
LedgerAlgHom in IndisputableMonolith.Algebra.RecognitionCategory decl_use
LedgerAlgObj in IndisputableMonolith.Algebra.RecognitionCategory decl_use
fastRadioBurstFromBITCert in IndisputableMonolith.Astrophysics.FastRadioBurstFromBIT decl_use
fast_radio_burst_one_statement in IndisputableMonolith.Astrophysics.FastRadioBurstFromBIT decl_use
FRB_period_strict_increasing in IndisputableMonolith.Astrophysics.FastRadioBurstFromBIT decl_use
empirical_below_predicted_upper in IndisputableMonolith.Astrophysics.SchumannResonanceFromBIT decl_use
schumannResonanceCert in IndisputableMonolith.Astrophysics.SchumannResonanceFromBIT decl_use
phi_critical_numeric in IndisputableMonolith.CondensedMatter.JCostPhaseTransition decl_use
fractions_sum in IndisputableMonolith.Cosmology.VacuumUniformity decl_use
harmonics_nonneg in IndisputableMonolith.CrossDomain.DFTHarmonicSpectrum decl_use
mode_seven in IndisputableMonolith.CrossDomain.DFTHarmonicSpectrum decl_use
carrier_frequency_band in IndisputableMonolith.Engineering.AsteroidTrajectoryShaping decl_use
carrier in IndisputableMonolith.Engineering.CorticalNeuromodulationDevice decl_use
carrier_band in IndisputableMonolith.Engineering.CorticalNeuromodulationDevice decl_use
carrier_pos in IndisputableMonolith.Engineering.CorticalNeuromodulationDevice decl_use
corticalNeuromodulationDeviceCert in IndisputableMonolith.Engineering.CorticalNeuromodulationDevice decl_use
CorticalNeuromodulationDeviceCert in IndisputableMonolith.Engineering.CorticalNeuromodulationDevice decl_use
neuromod_one_statement in IndisputableMonolith.Engineering.CorticalNeuromodulationDevice decl_use
pulseSpacing in IndisputableMonolith.Engineering.CorticalNeuromodulationDevice decl_use
pulseSpacing_band in IndisputableMonolith.Engineering.CorticalNeuromodulationDevice decl_use
carrier_band in IndisputableMonolith.Engineering.PhantomCoupledGWAntennaSensitivity decl_use
carrier_pos in IndisputableMonolith.Engineering.PhantomCoupledGWAntennaSensitivity decl_use
gw_antenna_one_statement in IndisputableMonolith.Engineering.PhantomCoupledGWAntennaSensitivity decl_use
h_0 in IndisputableMonolith.Engineering.PhantomCoupledGWAntennaSensitivity decl_use
phantomCoupledGWAntennaSensitivityCert in IndisputableMonolith.Engineering.PhantomCoupledGWAntennaSensitivity decl_use
PhantomCoupledGWAntennaSensitivityCert in IndisputableMonolith.Engineering.PhantomCoupledGWAntennaSensitivity decl_use
sensitivity in IndisputableMonolith.Engineering.PhantomCoupledGWAntennaSensitivity decl_use

… and 10 more

depends on (1)

Lean names referenced from this declaration's body.

carrier in IndisputableMonolith.Engineering.CorticalNeuromodulationDevice decl_use