priceDeviation_at_phi
plain-language theorem explainer
The declaration shows that the J-cost evaluated at the price significance threshold equals phi minus three halves. Economists applying Recognition Science to market models cite it to quantify the canonical significant price departure as a 62 percent shift from equilibrium. The proof is a one-line wrapper that unfolds the threshold definition and invokes the pre-proved Jcost_phi_val lemma.
Claim. $J(p) = p - 3/2$ where $p = phi$ is the significant departure threshold (price ratio of approximately 1.618).
background
The Market Equilibrium from J-Cost module derives price clearing from the J-cost function, where departure from equilibrium price p* incurs cost J(p/p*) for overshooting or J(p*/p) for undershooting. The significant departure threshold is defined as phi, matching the phi-ladder rung that produces J-cost approximately 0.118 and a 62 percent price shift. This rests on the upstream lemma Jcost_phi_val, which states J(phi) = phi - 3/2 exactly via the identity phi squared equals phi plus one.
proof idea
The proof is a one-line wrapper. It unfolds the definition of priceSignificanceThreshold (which equals phi) and applies the exact lemma Jcost_phi_val from Constants.
why it matters
This anchors the economic application of J-cost to the Recognition Science forcing chain by equating the observable price threshold directly to the phi value. It supports the module's structural theorem on market equilibrium and the prediction that deviations beyond roughly 62 percent trigger arbitrage corrections. No downstream uses are recorded, but it closes the link between the phi-ladder and commodity-market behavior.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.