structure definition def or abbrev

`Measurement`

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

formal statement (Lean)

   6structure Measurement where
   7  name : String
   8  value : ℝ
   9  error : ℝ
  10
  11/-- Hardcoded measurements for now (JSON parsing blocked by Mathlib version). -/

used by (40)

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

LedgerComputation in IndisputableMonolith.Complexity.ComputationBridge decl_use
displays_invariant_under_equivalence in IndisputableMonolith.Constants.KDisplay decl_use
KGateMeasurement in IndisputableMonolith.Constants.KDisplay decl_use
w_mass_cdf_measurement in IndisputableMonolith.Cosmology.WMassAnomalyStructure decl_use
w_mass_sm_prediction in IndisputableMonolith.Cosmology.WMassAnomalyStructure decl_use
import_measurements in IndisputableMonolith.Data.Import decl_use
CQ in IndisputableMonolith.Ethics.CostModel decl_use
improves_comp_left in IndisputableMonolith.Ethics.CostModel decl_use
score in IndisputableMonolith.Ethics.CostModel decl_use
ModeRatioProtocol in IndisputableMonolith.Experiments.Protocols decl_use
WaterProtocol in IndisputableMonolith.Experiments.Protocols decl_use
requiresExperience in IndisputableMonolith.Gap45.Beat decl_use
quantum_parallelism_from_8tick in IndisputableMonolith.Information.ChurchTuring decl_use
quantumSpeedups in IndisputableMonolith.Information.ChurchTuring decl_use
no_cloning_from_ledger in IndisputableMonolith.Information.NoCloning decl_use
score in IndisputableMonolith.Measurement decl_use
born_rule_normalized in IndisputableMonolith.Measurement.BornRule decl_use
born_rule_normalized in IndisputableMonolith.Measurement.BornRuleLight decl_use
amplitude_modulus_bridge in IndisputableMonolith.Measurement.C2ABridge decl_use
weight_equals_born in IndisputableMonolith.Measurement.C2ABridge decl_use
C_equals_2A in IndisputableMonolith.Measurement.C2ABridgeLight decl_use
kernel_integral_match in IndisputableMonolith.Measurement.KernelMatch decl_use
amplitude_mod_sq_eq_weight in IndisputableMonolith.Measurement.PathAction decl_use
infeasible_below_thetaMin in IndisputableMonolith.Measurement.RecognitionAngle.ActionSmallAngle decl_use
cos_satisfies_regularity in IndisputableMonolith.Measurement.RecognitionAngle.AngleFunctionalEquation decl_use
theta_min_le_pi_half in IndisputableMonolith.Measurement.RecognitionAngle.BlindCone decl_use
trivialParams in IndisputableMonolith.Measurement.RecognitionAngle.TemporalGating decl_use
apply in IndisputableMonolith.Measurement.RSNative.Alignment decl_use
measure_to_joules in IndisputableMonolith.Measurement.RSNative.Calibration.SI decl_use
measure_to_joule_seconds in IndisputableMonolith.Measurement.RSNative.Calibration.SI decl_use

… and 10 more

depends on (5)

Lean names referenced from this declaration's body.

for in IndisputableMonolith.Foundation.UniversalForcingSelfReference decl_use
Measurement in IndisputableMonolith.Measurement.RSNative.Core decl_use
value in IndisputableMonolith.QFT.SpinStatistics decl_use
Measurement in IndisputableMonolith.Quantum.NonlocalityNoSignaling decl_use
measurements in IndisputableMonolith.StandardModel.WeinbergAngle decl_use