phiSpaced_ratio
plain-language theorem explainer
The theorem shows that successive intervals in a φ-spaced pulse sequence maintain a constant ratio equal to the golden ratio φ, for any positive initial interval τ₀. Researchers modeling the ALEXIS Experiment A prediction cite it to confirm the geometric progression needed for J-cost comparisons against uniform spacing. The proof is a short algebraic reduction that unfolds the interval definition, secures positivity, and cancels via the ring tactic.
Claim. For any real number τ₀ > 0 and natural number k, if τ_k denotes the k-th φ-spaced interval starting from τ₀, then τ_{k+1} / τ_k = φ.
background
The module sets up the ALEXIS Experiment A comparison between φ-spaced pulses with intervals τ_k = τ₀ · φ^k and uniform pulses with constant spacing T. The J-cost is the derived cost of a multiplicative recognizer on positive ratios, per MultiplicativeRecognizerL4.cost, and equals the cost of any recognition event, per ObserverForcing.cost. Upstream structures include PhiForcingDerived.of for the J-cost definition and DAlembert.LedgerFactorization.of for the underlying (ℝ₊, ×) calibration.
proof idea
Unfolds the definition of the interval function to expose the power of φ. Applies mul_pos and pow_pos to obtain positivity of the product in the denominator. Rewrites the division equation via div_eq_iff and concludes with the ring tactic.
why it matters
Supplies the ratio substitution used in experiment_a_prediction_holds to establish positive J-cost per step for φ-spacing, and appears directly in the PhiVsUniformCert structure. This fills the structural claim that adjacent φ-ratio intervals carry J(φ) > 0, supporting the boundary J-cost reduction in the RS prediction for Experiment A. It connects to the phi fixed point forced in the T5-T6 steps of the unified forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.