phiSpacedInterval
plain-language theorem explainer
phiSpacedInterval supplies the explicit formula for the k-th timing interval in a geometric pulse sequence with ratio phi, starting from initial interval tau_0. Researchers modeling the ALEXIS Experiment A prediction cite this definition when comparing total J-cost for phi-spaced versus uniform sequences in Recognition Science. It is a direct definition that expands immediately to the product of tau_0 and the k-th power of phi with no lemmas invoked.
Claim. The k-th φ-spaced pulse interval is given by $τ_k = τ_0 φ^k$ for initial interval $τ_0 > 0$ and natural number $k$.
background
In the Phi vs Uniform Pulse Spacing module, this definition encodes the geometric timing sequence τ_k = τ_0 · φ^k used for Experiment A. The J-cost function J(x) = (x + 1/x)/2 - 1 is strictly convex with unique minimum at x = 1, as established in the upstream PhysicsComplexityStructure structure. The local theoretical setting contrasts φ-spaced pulses against uniform spacing, with the prediction that the geometric sequence reduces boundary J-cost contributions when total duration is fixed.
proof idea
This is a direct definition that expands to the product of the initial interval and the k-th power of phi. No lemmas or tactics are applied beyond standard real arithmetic and the power operation.
why it matters
This definition is the base object feeding the PhiVsUniformCert structure and the ExperimentAPrediction proposition, which assert that φ-spacing yields lower global J-cost than uniform alternatives. It instantiates the self-similar fixed point phi from the T5-T6 forcing chain and supports the claim that J(φ) < J(2) among natural ratios. The definition closes the gap between the abstract phi-ladder and concrete pulse-timing predictions in the module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.