Pith. sign in
module module moderate

IndisputableMonolith.Physics.BlackHoleMassGapFromPhi

show as:
view Lean formalization →

Defines a phi-derived domain cost and a canonical positive threshold that encode a black hole mass gap in RS-native units. Supplies a certificate structure (BHMassFuncCert) witnessing nonnegativity and threshold positivity. Physicists tracing the mass ladder to horizon scales would cite it. The module is mostly definitions plus short positivity lemmas from the Cost and Constants imports.

claimIntroduce a domain cost $C$ on a black-hole mass parameter, a canonical threshold $\theta>0$ built from $\varphi$, and a certificate that $C\ge 0$ with $\theta$ strictly positive, so the admissible mass spectrum sits above a $\varphi$-forced gap.

background

Recognition Science fixes the golden ratio $\varphi$ as the self-similar fixed point of the J-cost (forcing step T6) and places particle and horizon masses on a discrete $\varphi$-ladder. The Cost import supplies the nonnegative J-cost $J(x)=(x+x^{-1})/2-1$; Constants supplies the RS tick $\tau_0$ and related native units.

This module specializes that cost language to a black-hole mass domain. It defines a domain cost functional, records its value at a reference point, and proves nonnegativity. A canonical threshold is then cut from $\varphi$ (and shown positive), marking the minimal admissible mass scale in the gap picture.

The certificate bundle packages these facts so downstream physics layers can assume a certified mass-gap witness without re-deriving the inequalities.

proof idea

Definition-heavy module. domainCost and canonicalThreshold are introduced as defs; domainCost_nonneg and canonicalThreshold_pos are short positivity arguments that reduce to nonnegativity of the imported J-cost and positivity of powers of $\varphi$. BHMassFuncCert is a structure bundling those facts; cert and cert_inhabited build and inhabit a default instance. No deep tactic proof: algebraic reduction to Cost/Constants lemmas.

why it matters in Recognition Science

Places a black-hole mass gap on the same $\varphi$-ladder that governs particle masses (yardstick $\cdot\varphi^{\mathrm{rung}-8+\mathrm{gap}(Z)}$) and the eight-tick octave (T7). The certificate is the local interface other Physics modules can import when they need a forced minimal horizon mass rather than an ad hoc cutoff. No downstream edges are recorded yet in the mirror graph, so this sits as a leaf ready for horizon thermodynamics or information-bound arguments that require a discrete mass floor.

scope and limits

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (8)