priceSignificanceThreshold_gt_one
plain-language theorem explainer
The theorem asserts that the significant price deviation threshold exceeds unity in the J-cost market model. Economists analyzing arbitrage corrections in commodity markets would cite this to confirm the threshold lies above equilibrium at the golden ratio. The proof is a direct one-line application of the established inequality for phi.
Claim. $1 < phi$, where $phi$ is the golden ratio serving as the significant departure threshold for price ratios in the market equilibrium model.
background
The module models market equilibrium as the point where price clears with supply equal to demand. Any departure incurs a J-cost: overshooting costs J(p/p*) while undershooting costs J(p*/p), which equals J(p/p*) by symmetry of the Recognition Composition Law. The significant departure threshold is defined as phi, corresponding to a roughly 62 percent price change from equilibrium that matches empirical observations of strong arbitrage responses.
proof idea
The proof is a one-line wrapper that applies the lemma one_lt_phi from Constants (and its duplicates in PhiSupport).
why it matters
This result is assembled into the MarketEquilibriumCert definition, which packages the equilibrium deviation properties together with the threshold inequality. It supports the Recognition Science claim that the minimum noticeable price deviation occurs at J(phi) approximately 0.118 on the phi-ladder. The construction ties directly to the T5 J-uniqueness and T6 phi fixed-point landmarks.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.