phi_pos
plain-language theorem explainer
The lemma asserts that the golden ratio constant phi is strictly positive. It is invoked in any derivation that scales quantities along the phi-ladder or invokes the eight-tick octave to keep all subsequent expressions positive. The proof is a one-line term that delegates directly to the corresponding lemma in the core Constants module.
Claim. $0 < phi$, where $phi$ denotes the golden ratio constant.
background
The module collects project-wide constants together with minimal structural lemmas. The upstream Constants structure from CPM.LawOfExistence supplies an abstract bundle of CPM quantities that includes a non-negative Knet field. Phi itself is introduced as the self-similar fixed point forced by the UnifiedForcingChain at step T6.
proof idea
The proof is a one-line term wrapper that applies the phi_pos lemma from IndisputableMonolith.Constants.
why it matters
This supplies the basic positivity fact required for the phi constant before any mass formula of the form yardstick * phi^(rung - 8 + gap(Z)) or Berry threshold phi^-1 can be stated. It closes a minimal structural obligation in the Compat layer and is a prerequisite for later theorems that assume positive scaling factors. No downstream uses are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.