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

WaterMeasurement

show as:
view Lean formalization →

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.

claimA 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 in Recognition Science

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.

scope and limits

formal statement (Lean)

 190structure WaterMeasurement where
 191  condition : String
 192  tau_gate : ℝ
 193  domain_size : ℝ
 194
 195/-- The water prediction is falsified if τ_gate is far from 65 ps OR no change near intention -/

used by (1)

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

depends on (5)

Lean names referenced from this declaration's body.