kappaA_pos
plain-language theorem explainer
The lemma establishes positivity of the scale factor kappaA in the binary scales construction. Researchers building phi-exponential wrappers or phi-ladder mass formulas cite this result to guarantee positive growth factors. The proof is a one-line wrapper that unfolds the definition of kappaA and invokes the phi positivity lemma from the constants bundle.
Claim. $0 < k_A$ where $k_A := phi$ and $phi$ is the self-similar fixed point supplied by the CPM constants structure.
background
The RecogSpec.Scales module develops binary scales and phi-exponential wrappers. kappaA is defined as the value of phi drawn from the abstract Constants structure, which packages the core CPM constants Knet, Cproj, Ceng, Cdisp together with the nonnegativity axiom on Knet. The upstream Constants bundle supplies the foundational real numbers used throughout the Recognition Science forcing chain, with phi serving as the self-similar fixed point (T6).
proof idea
One-line wrapper proof. The tactic unfolds kappaA to Constants.phi and then applies simpa to the lemma Constants.phi_pos that already records 0 < phi.
why it matters
The result anchors positivity for every subsequent phi-powered scale in the module, including the PhiPow and B_of families. It directly supports the eight-tick octave and D = 3 constructions that rely on positive exponential factors. Within the Recognition Science framework it closes the elementary positivity step required before mass formulas of the form yardstick * phi^(rung - 8 + gap(Z)) can be stated.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.