J_cost
plain-language theorem explainer
The declaration defines the J-cost function as J(x) = (x + x^{-1})/2 - 1 for real x. Condensed matter modelers in the Recognition Science program cite it when computing energy gaps and locating phase transitions on the phi-ladder. The definition is a direct transcription of the T5 J-uniqueness condition.
Claim. The J-cost function satisfies $J(x) = (x + x^{-1})/2 - 1$ for all real $x$.
background
Recognition Science derives the J-cost from the forcing chain at step T5, where J-uniqueness fixes the form J(x) = (x + x^{-1})/2 - 1, also expressible as cosh(log x) - 1. This module applies it to condensed matter phase transitions, building on the scale function that generates phi^k ladders from cosmology and the point constructor for interval arithmetic in numerics. The setting assumes positive real arguments for physical quantities like energy scales.
proof idea
The definition is the base algebraic expression. It requires no lemmas or tactics; downstream results unfold it to prove J_cost 1 = 0 and positivity for x ≠ 1.
why it matters
J_cost supplies the core expression for the entire JCostPhaseTransition module, enabling proofs of its minimum at unity, positivity elsewhere, and symmetry under inversion. It directly implements the T5 landmark and feeds into phi_critical_energy for superconducting gap scales. The definition appears in thermodynamics results on reaction_equilibrium and heatCapacity, closing the loop from forcing chain to observable predictions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.