pith. machine review for the scientific record. sign in
structure definition def or abbrev high

Measurement

show as:
view Lean formalization →

The Measurement structure records experimental data points using a string identifier together with a real-valued result and its uncertainty. Data import and validation modules throughout the framework cite it to anchor theoretical predictions against observation. The definition consists of a direct structure declaration requiring no lemmas or reduction steps.

claimA measurement record consists of a string name, a real number value, and a real number error bound.

background

The Data.Import module supplies a lightweight record type for measurements while full JSON support remains unavailable in the current Mathlib version. This structure differs from the protocol-aware Measurement in RSNative.Core, which adds optional windows, protocols, and uncertainty objects. Upstream references point to analogous structures in QFT.SpinStatistics (spin values), Quantum.NonlocalityNoSignaling (axis and outcome pairs), and StandardModel.WeinbergAngle (electroweak fit lists).

proof idea

The declaration is a bare structure definition. No tactics or lemmas are applied; the three fields are introduced directly in the structure syntax.

why it matters in Recognition Science

This type is consumed by import_measurements to provide hardcoded values for alpha inverse, Weinberg angle, and electron g-2. It feeds into LedgerComputation for cost modeling, KDisplay for unit-invariant displays, and WMassAnomalyStructure for CDF and SM comparisons. The structure closes the data interface that lets the Recognition framework compare phi-ladder predictions against experiment.

scope and limits

Lean usage

def import_measurements : List Measurement := [{ name := 'AlphaInvPrediction', value := 137.035999084, error := 0.000000084 }]

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.

… and 10 more

depends on (5)

Lean names referenced from this declaration's body.