ExperimentAPrediction
plain-language theorem explainer
The Experiment A Prediction defines the statement that every consecutive pair of φ-spaced pulse intervals carries strictly positive J-cost. Modelers of recognition-driven pulse sequences cite it when formalizing the ALEXIS experiment forecast. The declaration is a direct abbreviation of the quantified positivity condition on the J-cost of the φ-ratio.
Claim. The proposition that for every positive real initial interval τ₀ and every natural number k, the J-cost of the ratio of consecutive φ-spaced intervals τ_{k+1}/τ_k is strictly positive, where the intervals form the geometric sequence τ_k = τ₀ φ^k.
background
Recognition Science defines J-cost as the recognition cost of a state transition induced by a multiplicative recognizer, vanishing exactly when the ratio equals 1. The phiSpacedInterval function builds geometric sequences with common ratio φ, the self-similar fixed point. Upstream results include the equilibrium theorem establishing Jcost 1 = 0 and the cost function on recognition events.
proof idea
This is a direct definition that packages the universal quantification over positive τ₀ and step index k into a single Prop asserting positivity of J-cost on each φ-ratio.
why it matters
It supplies the prediction field inside the PhiVsUniformCert structure and is discharged in experiment_a_prediction_holds by reduction to phiSpacing_jcost_pos. The definition encodes the RS model claim that φ-spacing reduces boundary J-cost relative to uniform spacing, linking to the phi-ladder optimality in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.