Pith. sign in
module module moderate

IndisputableMonolith.Foundation.GoldenAngle_RS

show as:
view Lean formalization →

Module formalizing the golden-angle threshold in Recognition Science: a domain cost built from the J-functional, its nonnegativity, a positive canonical threshold, and an inhabited certificate package. Cited by anyone linking angular selection or the alpha band to the forced self-similar scale. Mostly definitional scaffolding plus elementary positivity and equality lemmas.

claimThe module introduces a domain cost $C$ derived from the Recognition cost $J$, proves $C\ge 0$ and an evaluation identity, defines a positive canonical threshold $\tau_\ast$, and packages a golden-angle certificate (inhabited) that records the threshold data in RS-native units.

background

Recognition Science forces the unique symmetric cost $J(x)=(x+x^{-1})/2-1$ (T5) and the self-similar fixed point $\varphi$ (T6). Angular and packing phenomena in the framework are expected to sit at golden-ratio multiples; the classical golden angle is $2\pi\varphi^{-2}$ (or $360^\circ\cdot\varphi^{-2}$).

This module sits in Foundation and imports the RS constants (including the tick $\tau_0=1$) together with the Cost layer that supplies $J$. It defines a domain-level cost functional, records its value at a distinguished point, and isolates a canonical positive threshold intended to mark the golden-angle scale.

The certificate bundle simply assembles those facts so downstream geometry or spectroscopy developments can assume a single inhabited record rather than re-proving nonnegativity and positivity.

proof idea

Definition module with light lemma support. Domain cost is introduced by a direct formula from $J$; the evaluation identity is definitional unfolding. Nonnegativity follows from the known nonnegativity of $J$ (Cost layer). The canonical threshold is a closed-form positive real; positivity is a short arithmetic check. The certificate is a structure whose fields are exactly those lemmas; inhabitation is by packaging the already-proved components.

why it matters in Recognition Science

Gives Foundation a named home for the golden-angle threshold that links the forced scale $\varphi$ to angular selection. Downstream work on packing, phyllotaxis analogues, or the $\alpha^{-1}$ band near $137$ can import one certificate rather than rebuilding cost nonnegativity. No external used-by edges are recorded yet; the module is preparatory scaffolding inside the forcing chain neighbourhood of T5–T6 and the RS-native constants. It does not itself derive $D=3$ or the eight-tick octave.

scope and limits

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (8)