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

HealingProtocol

show as:
view Lean formalization →

The HealingProtocol structure records parameters for testing distance-independent coherence transfer between healer and patient, defaulting to 50 pairs, distances from 1 m to 10 km, patient blinding, and outcomes such as HRV coherence plus EEG phase locking. Experimental groups checking Recognition Science predictions on Θ-coupling would cite these defaults when designing double-blind trials. It is realized as a Lean structure that simply enumerates the fields with their preset values.

claimA distance-independent healing protocol is a record containing a natural number $n$ of healer-patient pairs (default 50), a finite list of test distances in meters, a boolean flag for patient double-blinding (default true), and a list of outcome measures that includes subjective wellbeing, HRV coherence, and EEG phase locking.

background

The declaration lives inside the Experiments.Protocols module, whose module doc states that all predictions are hypotheses with explicit falsification criteria derived from voxel theory. Core items listed there include EEG φ-frequencies, mode ratios classifying consciousness states, and healing via coherence transfer through Θ-coupling. Upstream structures supply the supporting machinery: PhiForcingDerived.of encodes J-cost minimization, SpectralEmergence.of forces the gauge content and three generations, and DAlembert.LedgerFactorization.of calibrates the underlying J function.

proof idea

This is a structure definition that directly lists four fields together with their default values. No lemmas or tactics are invoked; the body is a straightforward record construction.

why it matters in Recognition Science

HealingProtocol supplies the concrete parameters that feed the healing_falsified check inside theoryConfirmed. It thereby turns the voxel-theory prediction of coherence transfer into a reproducible experimental design. The protocol closes the path from the Recognition Science forcing chain (T5 J-uniqueness to T8 D=3) to an empirical test whose quantitative backbone is the phi-ladder and the alpha band.

scope and limits

formal statement (Lean)

 136structure HealingProtocol where
 137  /-- Number of healer-patient pairs -/
 138  n_pairs : ℕ := 50

proof body

Definition body.

 139  /-- Distances to test (meters) -/
 140  distances : List ℝ := [1, 10, 100, 1000, 10000]
 141  /-- Blinding: healer knows when sending, patient does not -/
 142  double_blind_patient : Bool := true
 143  /-- Outcome measures -/
 144  outcomes : List String := ["subjective_wellbeing", "HRV_coherence", "EEG_phase_locking"]
 145
 146/-- Healing coherence transfer prediction -/

used by (1)

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

depends on (7)

Lean names referenced from this declaration's body.