ratioInRange
plain-language theorem explainer
ratioInRange defines a boolean predicate that returns true precisely when a measured M2/M4 ratio lies inside the closed interval supplied by a ModeRatioPrediction record. Experimental groups testing voxel-derived consciousness classifications would apply it to decide whether EEG data supports or falsifies a predicted state. The implementation is a direct one-line interval membership test on the low and high bounds of the input structure.
Claim. Let $p$ be a ModeRatioPrediction carrying bounds $r_0$ and $r_1$. For measured value $m$, the predicate holds if and only if $r_0 ≤ m ≤ r_1$.
background
The Experiments.Protocols module supplies concrete, falsifiable protocols derived from the voxel/meaning framework. Its core predictions include EEG peaks at φ^n Hz and M2/M4 mode ratios that classify consciousness states. ModeRatioPrediction is the record type that packages one such prediction: a ConsciousnessState together with an expected ratio interval (ratio_low, ratio_high) and a default confidence of 0.95. Upstream dependencies include the independent spatial semantics from LNALSemantics and the independent axis primitives from RSCoupledAxis, both of which underwrite the separation of modes used to generate the ratio bounds.
proof idea
The definition is a one-line wrapper that applies the standard real-number interval test directly to the ratio_low and ratio_high fields of the supplied ModeRatioPrediction.
why it matters
This definition supplies the membership test required by ModeRatioProtocol and modeRatioPredictions to turn raw EEG ratios into state classifications. It operationalizes the second core prediction listed in the module documentation and thereby supports the falsification criteria that the entire experimental suite is required to carry. The construction sits downstream of the phi-ladder and eight-tick octave machinery that fix the numerical values of the predicted bounds.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.