phiVsUniformCert
plain-language theorem explainer
This definition assembles the PhiVsUniformCert structure asserting that phi-spaced intervals maintain ratio phi, that Jcost(phi) is strictly less than Jcost(2), and that the ALEXIS Experiment A prediction holds under RS. Physicists validating geometric versus uniform pulse timing would cite it to confirm the J-cost advantage of the golden ratio. The definition is formed by direct field assignment from the ratio theorem, the J-cost comparison, and the prediction theorem.
Claim. The structure is instantiated by the assertions that for every positive initial interval τ₀ and every natural k the ratio of successive φ-spaced intervals equals φ, that Jcost(φ) < Jcost(2), and that the Experiment A prediction holds.
background
The module formalizes the RS prediction for ALEXIS Experiment A, which compares φ-spaced pulses (intervals τ_k = τ₀ · φ^k) against uniform spacing. Jcost is the convex energy proxy minimized at the golden ratio (imported from Cost and Constants modules). The structure PhiVsUniformCert packages three fields: the ratio property, the inequality Jcost(φ) < Jcost(2), and the ExperimentAPrediction theorem. Upstream, phiSpaced_ratio proves the constant ratio equals φ by unfolding the interval definition and applying ring arithmetic; phi_beats_2 proves the J-cost inequality by rewriting both sides as squares and applying nlinarith with the bounds on φ; experiment_a_prediction_holds reduces the prediction to the positive per-step J-cost.
proof idea
This is a definition that constructs the PhiVsUniformCert structure by direct field assignment: phi_ratio is set to phiSpaced_ratio, phi_beats_2 to phi_beats_2, and prediction to experiment_a_prediction_holds.
why it matters
The definition supplies the concrete certificate for the RS Experiment A prediction that φ-spacing minimizes boundary J-cost relative to uniform spacing. It supports the parent structure PhiVsUniformCert and aligns with framework landmarks T5 (J-uniqueness) and T6 (phi as self-similar fixed point) by confirming phi beats the ratio 2. The module doc notes that full optimality among arbitrary ratios remains a model claim, so this instance closes the formal packaging while leaving the general comparison open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.