WaterMeasurement
plain-language theorem explainer
WaterMeasurement records experimental data on water coherence with fields for a condition label, gate time tau_gate in reals, and domain size. Physicists testing Recognition Science predictions on altered water structure near intention would cite this record to log measurements for falsification checks. The declaration is a plain structure definition introducing the three-field record type with no further computation.
Claim. A water measurement consists of a condition string, a real number $tau_{gate}$ for the gate time, and a real number for the domain size.
background
The structure sits in the Experiments.Protocols module, which encodes testable predictions from voxel theory including altered coherence domains in water near intention. The module states that all such predictions remain hypotheses equipped with explicit falsification criteria. Upstream results supply the surrounding framework: OptionAEmpiricalProgram.is enforces collision-free empirical programs, PrimitiveDistinction.from derives four structural conditions from seven axioms, and EdgeLengthFromPsi.is supplies algebraic relations for simplicial edges.
proof idea
The declaration is a structure definition. It introduces the record type directly with the three fields condition, tau_gate, and domain_size; no tactics or lemmas are applied.
why it matters
WaterMeasurement supplies the input type for isWaterFalsified, which declares the water prediction falsified when tau_gate lies outside (60,70) ps or shows less than 1 ps change under intention. This places the definition inside the unified falsification framework of the experimental protocols, addressing the water-structure item among the module's core predictions derived from the Recognition Science forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.