Measurement — Recognition explainer

formal statement (Lean)

 117structure Measurement (α : Type) where
 118  value : α
 119  window : Option Window := none

proof body

Definition body.

 120  protocol : Protocol
 121  uncertainty : Option Uncertainty := none
 122  notes : List String := []
 123
 124namespace Measurement
 125
 126/-- Map the value of a measurement, preserving window/protocol/uncertainty/notes. -/

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
Measurement 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

… and 10 more

depends on (13)

Lean names referenced from this declaration's body.

of in IndisputableMonolith.Astrophysics.NucleosynthesisTiers decl_use
Window in IndisputableMonolith.Complexity.CellularAutomata decl_use
Measurement in IndisputableMonolith.Data.Import decl_use
of in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization decl_use
of in IndisputableMonolith.Foundation.PhiForcingDerived decl_use
of in IndisputableMonolith.Foundation.SpectralEmergence decl_use
of in IndisputableMonolith.Information.PhysicsComplexityStructure decl_use
Map in IndisputableMonolith.Measurement decl_use
Protocol in IndisputableMonolith.Measurement.RSNative.Core decl_use
Uncertainty in IndisputableMonolith.Measurement.RSNative.Core decl_use
Window in IndisputableMonolith.Measurement.RSNative.Core decl_use
value in IndisputableMonolith.QFT.SpinStatistics decl_use
Measurement in IndisputableMonolith.Quantum.NonlocalityNoSignaling decl_use