phiCost_nonneg
plain-language theorem explainer
The nonnegativity of phiCost holds for every real u, where phiCost(u) equals cosh((log φ) u) minus one. Analysts establishing coercivity bounds for annular samples in the Recognition Science cost framework cite this result when proving that topological floors remain nonnegative. The proof reduces directly to the elementary inequality cosh x ≥ 1 via unfolding and linear arithmetic.
Claim. $0 ≤ cosh((log φ) · u) - 1$ for all real $u$.
background
In the annular J-cost framework the function phiCost is defined by phiCost(u) := cosh((log φ) u) - 1, which coincides with the J-cost of φ^u. This construction supports Jensen-based coercivity arguments for phase increments on concentric rings, ensuring that nonzero winding numbers force quadratic-logarithmic cost growth. The module establishes several properties of phiCost, including its value at zero and symmetry, as prerequisites for the topological floor and excess decomposition.
proof idea
The proof unfolds the definition of phiCost to obtain cosh((log φ) u) - 1 and invokes linarith on the library fact that cosh x ≥ 1 for all real x, instantiated at x = (log φ) u.
why it matters
This nonnegativity result is invoked directly in the proof of topologicalFloor_nonneg, which asserts that the topological floor is nonnegative for natural n and integer m. It forms part of the basic properties of the φ-cost needed for the annular sampling machinery and the RS topological cost-covering bridge. Within the Recognition Science framework it underpins the coercivity estimates that connect to the eight-tick octave and the derivation of three spatial dimensions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.