priceSignificanceThreshold
plain-language theorem explainer
priceSignificanceThreshold sets the significant departure threshold for price deviations in J-cost market models to the golden ratio phi. Market equilibrium analyses in Recognition Science cite it when establishing the minimum noticeable overshoot at approximately 62 percent above equilibrium. The definition is a direct abbreviation to phi that enables unfolding in downstream J-cost calculations and inequality proofs.
Claim. The significant price departure threshold is defined as the golden ratio $phi$, corresponding to a price ratio of approximately 1.618 (62 percent above equilibrium).
background
In the Market Equilibrium from J-Cost module, market equilibrium occurs when price clears at supply equals demand. Any departure incurs a J-cost given by J(p/p*) for overshooting and the symmetric J(p*/p) for undershooting, where J satisfies the Recognition Composition Law J(xy) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y) and takes the explicit form J(x) = (x + x^{-1})/2 - 1. The module states that the minimum noticeable deviation corresponds to J(phi) approximately 0.118, aligning with empirical arbitrage corrections for deviations larger than 50-60 percent reported by Fama 1970 and Lo 1999.
proof idea
Direct definition that equates priceSignificanceThreshold to phi. No lemmas or tactics are invoked; the abbreviation is unfolded in priceDeviation_at_phi to obtain the J-cost identity and in priceSignificanceThreshold_gt_one to apply one_lt_phi.
why it matters
This definition supplies the threshold value required by MarketEquilibriumCert (which asserts deviation_at_eq, deviation_nonneg, and threshold_gt_one) and by priceDeviation_at_phi (which computes Jcost of the threshold as phi - 3/2). Within Recognition Science it instantiates the self-similar fixed point phi from T6 of the forcing chain and anchors the one-rung level of the phi-ladder for noticeable departures. The module falsifier concerns median reversion times falling outside the predicted phi-ladder window.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.