optimal_chain
plain-language theorem explainer
The theorem states that J-cost vanishes for the unit supply chain. Economists working in Recognition Science models cite it as the zero-disruption baseline for optimal configurations. The proof is a direct one-line application of the core Jcost unit lemma.
Claim. $J(1) = 0$, where $J(x) = (x-1)^2/(2x)$ measures deviation from optimality.
background
The module develops supply chain models from Recognition Science, with five canonical tiers (raw materials through retail) set equal to configDim D = 5. Disruption equals positive J-cost and optimality equals J = 0; the bullwhip effect is described as J-amplification upstream along the phi-ladder scaling of variance. J-cost itself is defined in the Cost module by the squared-ratio formula J(x) = (x-1)^2/(2x).
proof idea
This is a one-line wrapper that applies the lemma Jcost_unit0 from IndisputableMonolith.Cost (and its duplicate in JcostCore), which reduces the claim by simp on the Jcost definition.
why it matters
The result supplies the zero point required by supplyChainCert, which packages the five-tier count together with this optimality statement to certify an RS-derived supply chain. It aligns with T5 J-uniqueness in the forcing chain and the framework landmark that optimal configurations have vanishing J-cost. No open questions or scaffolding are touched.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.