pith. machine review for the scientific record. sign in
def definition def or abbrev high

F_threshold

show as:
view Lean formalization →

The declaration defines the observability threshold flux as coherence energy divided by the fundamental tick. Recognition Science astrophysicists cite it when imposing minimum photon flux for a stellar system to register as recognizable under J-cost constraints. The definition is a direct quotient of the two pre-established constants E_coh and τ_0.

claimThe observability threshold flux is defined by $F_0 := E_0 / τ_0$, where $E_0 = φ^{-5}$ (in eV) is the coherence energy and $τ_0 = 1/(8 J_b)$ is the fundamental recognition tick.

background

The ObservabilityLimits module derives mass-to-light ratios from the requirement that photon flux must exceed a recognition threshold set by coherence energy and the fundamental tick. Coherence energy is fixed at $φ^{-5}$ in electron-volts; the tick is the reciprocal of eight times the per-bit J-cost. These enter the flux bound $F ≥ E_0/τ_0$ that, together with coherence volume $V ~ l_rec^3$, constrains observable stellar assemblies.

proof idea

This is a direct definition that performs the division of the coherence energy constant by the fundamental tick constant. No lemmas or tactics are invoked beyond the referenced sibling definitions of E_coh and τ_0.

why it matters in Recognition Science

The definition supplies the flux lower bound required by Strategy 3 to close the observability constraint on the mass-to-light ratio. It supports the result that M/L lies in the set of phi powers from 0 to 3, with typical value φ, and aligns with the eight-tick octave and phi-ladder structure of the framework. No downstream uses are recorded yet.

scope and limits

formal statement (Lean)

  71noncomputable def F_threshold : ℝ := E_coh / τ_0

proof body

Definition body.

  72
  73/-- Coherence volume: maximum assembly volume -/

depends on (1)

Lean names referenced from this declaration's body.