pulseSpacing_band
pulseSpacing_band pins the device pulse interval inside (0.123, 0.125) s. Hardware designers specifying transcranial stimulators would reference the interval when matching the 5φ carrier. The tactic proof unfolds the two definitions then applies the phi bounds and linarith.
claim$0.123 < 1/(5φ) < 0.125$ where φ is the golden ratio.
background
The module defines carrier frequency as 5φ Hz and pulse spacing as its reciprocal 1/(5φ) s. This supplies the timing parameter for the φ-rational pulse schedule in the transcranial neuromodulation device. The local setting is the engineering derivation of RS_PAT_025 operating at cortical-column resonance. Upstream lemmas phi_gt_onePointSixOne and phi_lt_onePointSixTwo supply the numerical bounds 1.61 < φ < 1.62 that convert the symbolic expression into the concrete interval.
proof idea
The proof unfolds pulseSpacing and carrier to reach 1/(5φ). It obtains the two phi bounds as hypotheses and proves positivity of the denominator via linarith. The lower bound is dispatched by rewriting with lt_div_iff₀ followed by linarith; the upper bound by rewriting with div_lt_iff₀ followed by linarith.
why it matters in Recognition Science
The bound is assembled into corticalNeuromodulationDeviceCert and appears inside neuromod_one_statement. It supplies the concrete timing interval required by the device specification in the Recognition Science engineering derivation. The result confirms operation near 124 ms, consistent with the phi-ladder structure.
scope and limits
- Does not derive the carrier frequency from the Recognition Composition Law.
- Does not prove that 5φ maximizes entrainment.
- Does not incorporate electrode impedance or tissue effects.
- Does not address regulatory or safety margins.
Lean usage
have h : (0.123 : ℝ) < pulseSpacing ∧ pulseSpacing < 0.125 := pulseSpacing_bandformal statement (Lean)
49theorem pulseSpacing_band :
50 (0.123 : ℝ) < pulseSpacing ∧ pulseSpacing < 0.125 := by
proof body
Tactic-mode proof.
51 unfold pulseSpacing carrier
52 have h1 := phi_gt_onePointSixOne
53 have h2 := phi_lt_onePointSixTwo
54 have h_pos : (0 : ℝ) < 5 * phi := by linarith [phi_pos]
55 refine ⟨?_, ?_⟩
56 · rw [lt_div_iff₀ h_pos]; linarith
57 · rw [div_lt_iff₀ h_pos]; linarith
58
59/-! ## §2. Entrainment-confidence ladder -/
60
61/-- Confidence at φ-rung `k` (relative to baseline 1): `1 / φ^k`. -/