uniform_step_cost
plain-language theorem explainer
Uniform spacing of pulses at ratio 1 incurs zero J-cost per step. Researchers comparing phi-spaced sequences to uniform ones in the ALEXIS Experiment A prediction cite this baseline to isolate boundary effects. The proof is a direct one-line term application of the unit-cost lemma for J.
Claim. The J-cost of a unit ratio satisfies $J(1)=0$, where $J(x)=(x-1)^2/(2x)$.
background
The J-cost function measures recognition cost for a multiplicative ratio x and is defined by the squared-ratio formula $J(x)=(x-1)^2/(2x)$. This module develops the ALEXIS Experiment A prediction that phi-spaced intervals minimize total J-cost for fixed total time, contrasting them against uniform spacing. Uniform steps supply the reference case in which internal increments carry zero cost while endpoints may still contribute positive terms. The upstream lemma Jcost_unit0 establishes the identity by direct simplification of the J definition.
proof idea
The proof is a one-line wrapper that applies the Jcost_unit0 lemma from the Cost module.
why it matters
This anchors the uniform baseline inside the PhiVsUniformPulseSpacingCert, enabling the contrast with phi-spacing that reduces boundary penalties. It supports the Experiment A claim that phi minimizes J(r) among natural ratios and connects to the forcing chain at T5 J-uniqueness and the phi fixed point. The result feeds directly into higher certificates such as PhiVsUniformCert.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.