structure definition def or abbrev

`KGateMeasurement`

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

formal statement (Lean)

 178structure KGateMeasurement where
 179  /-- Measured τ_rec (time-first route) -/
 180  tau_rec_measured : ℝ
 181  /-- Measured λ_kin (length-first route) -/
 182  lambda_kin_measured : ℝ
 183  /-- RS units pack used for normalization -/
 184  units : RSUnits
 185  /-- Measurement uncertainties -/
 186  sigma_tau : ℝ
 187  sigma_lambda : ℝ
 188  /-- Derived: K from each route -/
 189  K_from_tau : ℝ := tau_rec_measured / units.tau0

proof body

Definition body.

 190  K_from_lambda : ℝ := lambda_kin_measured / units.ell0
 191
 192/-- K-gate validation: routes agree within uncertainty -/

used by (2)

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

falsifier_K_gate_mismatch in IndisputableMonolith.Constants.KDisplay decl_use
validateKGate in IndisputableMonolith.Constants.KDisplay decl_use

depends on (14)

Lean names referenced from this declaration's body.

tau0 in IndisputableMonolith.Compat.Constants decl_use
ell0 in IndisputableMonolith.Constants decl_use
K in IndisputableMonolith.Constants decl_use
RSUnits in IndisputableMonolith.Constants decl_use
tau0 in IndisputableMonolith.Constants decl_use
ell0 in IndisputableMonolith.Constants.Derivation decl_use
tau0 in IndisputableMonolith.Constants.Derivation decl_use
K in IndisputableMonolith.Constants.LambdaRecDerivation decl_use
Measurement in IndisputableMonolith.Data.Import decl_use
from in IndisputableMonolith.Foundation.PrimitiveDistinction decl_use
for in IndisputableMonolith.Foundation.UniversalForcingSelfReference decl_use
Measurement in IndisputableMonolith.Measurement.RSNative.Core decl_use
Measurement in IndisputableMonolith.Quantum.NonlocalityNoSignaling decl_use
RSUnits in IndisputableMonolith.TruthCore.Display decl_use