HealingTrialData
plain-language theorem explainer
HealingTrialData records measurements from one healing trial as distance, effect size, and PLV change. Experimental physicists testing coherence transfer predictions would cite it when logging data for distance-decay checks. The declaration is a plain record type with three real fields and no computational content or axioms.
Claim. A healing trial datum is a triple $(d, e, p)$ with $d, e, p : ℝ$, where $d$ is distance, $e$ is effect size, and $p$ is PLV change.
background
The structure sits inside the experimental protocols module, which formalizes testable predictions from voxel theory. Core items include EEG φ-frequency peaks, mode-ratio classification of consciousness states, and healing via coherence transfer through Θ-coupling. All entries are treated as hypotheses equipped with explicit falsification criteria rather than derived theorems.
proof idea
The declaration is a structure definition introducing three fields of type ℝ. No lemmas or tactics are applied; it functions solely as a data container passed to downstream predicates such as isHealingFalsified.
why it matters
HealingTrialData supplies the input type for isHealingFalsified, which tests whether effect size decays with distance to falsify the coherence-transfer prediction. It implements the healing protocol listed in the module doc-comment and connects to the broader set of empirical checks derived from the phi-ladder and eight-tick octave, though it does not invoke any T0-T8 forcing steps directly.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.