Pith. sign in
module module moderate

IndisputableMonolith.Physics.StringLengthFromPhiLadder

show as:
view Lean formalization →

Packages a certificate that recovers a string length scale from a domain cost on the Recognition Science phi-ladder. Length-scale and RS-units workers cite the certificate record and its inhabited instance. The module is definitional: cost evaluation identities, nonnegativity, a positive canonical threshold, and a thin cert wrapper.

claimDefines a domain cost $C$ on the $\varphi$-ladder, proves $C\ge 0$ and an evaluation identity, introduces a canonical threshold $\theta>0$, and packages a certificate type asserting that a string length is recovered from $(C,\theta)$ in RS-native units.

background

Recognition Science places masses and length scales on a discrete $\varphi$-ladder fixed by the self-similar cost fixed point. The Cost import supplies the underlying $J$-cost structure; Constants fixes the RS time quantum $\tau_0=1$ tick and the usual RS-native units ($c=1$, $\hbar=\varphi^{-5}$, etc.).

This module specializes those ingredients to string length. Sibling definitions introduce a domain cost, its pointwise evaluation identity and nonnegativity, a positive canonical threshold, and a StringLengthCert record with an inhabited instance. The setting is certificate packaging, not a new forcing step.

proof idea

Definition-and-certificate module, not a multi-lemma derivation. It defines the domain cost and records elementary facts (evaluation identity, nonnegativity), defines the canonical threshold and proves positivity, then bundles those data into a string-length certificate with a trivial inhabited instance. No forcing-chain or RCL algebra is invoked here.

why it matters in Recognition Science

Gives physics code a single inhabited certificate that a string length sits on the same $\varphi$-ladder used for the mass formula and the eight-tick octave. That keeps length scales in RS-native units rather than as free SI inputs. The mirror graph currently lists no downstream used-by edges, so the module is a leaf packaging layer for later length-scale claims rather than a step in T0–T8.

scope and limits

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (8)