topologicalFloor_pos_of_charge_ne_zero
plain-language theorem explainer
Nonzero integer charge on a ring of positive integer radius forces the topological floor to be strictly positive. Researchers deriving annular coercivity bounds in Recognition Science cite this to guarantee positive cost from nonzero winding numbers. The proof unfolds the floor definition, verifies the scaled argument to phiCost is nonzero, invokes the quadratic lower bound to obtain positivity of phiCost, and multiplies by the positive prefactor 8n.
Claim. For every positive integer $n$ and every nonzero integer $m$, the topological floor satisfies $8n · ϕCost(-2πm/(8n)) > 0$, where $ϕCost(u) := cosh((log φ) u) - 1$.
background
The Annular J-Cost Framework defines phiCost(u) := cosh((log φ)·u) − 1 = J(φ^u) and constructs annular samples as phase increments on concentric rings. The topological floor on ring n with charge m is the product of the scaling factor 8n and phiCost evaluated at the normalized phase -2πm/(8n). This sits inside the module that certifies Jensen-based coercivity, ring bounds, and the trace-based carrier-budget interface for the RS topological cost-covering bridge.
proof idea
The tactic proof unfolds topologicalFloor, introduces positivity of 8n by norm_num, shows the argument u = -2πm/(8n) is nonzero by factoring out the nonzero charge and π, then applies phiCost_quadratic_lb to obtain a positive quadratic lower bound involving kappa. It concludes by chaining the two strict inequalities via lt_of_lt_of_le and mul_pos.
why it matters
The result is invoked directly by annularTopologicalFloor_one_pos_of_charge_ne_zero to settle the unit-ring case. It supplies the base positivity step in the annular cost-covering bridge, aligning with J-uniqueness (T5) and the eight-tick octave (T7) by ensuring nonzero winding produces strictly positive cost on every ring. It closes one link in the scaffolding toward the holomorphic nonvanishing carrier budget.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.