phi_pos
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 in Recognition Science
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.
scope and limits
- Does not compute the numerical value of phi.
- Does not relate phi to the Recognition Composition Law.
- Does not prove positivity for sibling constants such as E_coh or tau0.
formal statement (Lean)
17lemma phi_pos : 0 < phi := IndisputableMonolith.Constants.phi_pos
proof body
Term-mode proof.
18
19/-- Cohesion energy (placeholder) -/