phiLadder_pos
plain-language theorem explainer
Every element on the φ-ladder is strictly positive for any integer rung. Researchers deriving the Yang-Mills mass gap in Recognition Science cite this to guarantee that non-vacuum excitations carry positive J-cost. The proof is a one-line wrapper applying positivity preservation under integer exponentiation to the positive base φ from the constants bundle.
Claim. For every integer $n$, $0 < φ^n$, where $φ > 0$ is the constant supplied by the Recognition Science constants structure.
background
The module resolves the Yang-Mills mass gap from the J-cost functional $J(x) = ½(x + x^{-1}) - 1$ on the discrete φ-lattice. The φ-ladder consists of all positions $φ^n$ for $n ∈ ℤ$, with vacuum at $n=0$ where $J=0$. Upstream results record that the ladder arises as the set of stable positions forced by the φ-emergence construction, and the constants bundle supplies the base positivity of φ. The module doc-comment states that φ-ladder elements are positive, consistent with the upstream note that φ^n is always positive for any integer n.
proof idea
The proof is a one-line wrapper that applies the general positivity of integer powers to the positive base φ supplied by the constants structure.
why it matters
It is invoked by the downstream lemma bond_cost_nonneg to establish that per-bond J-costs are nonnegative. This supports the central theorem that the spectral gap Δ = J(φ) = φ - 3/2 > 0 emerges from the J-cost functional and the T5-T6 forcing chain. The result closes the basic positivity step required before proving monotonicity and the exact gap value in the module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.