StellarConfig
StellarConfig introduces a structure holding two positive real scale ratios for photon emission and mass storage events during stellar collapse, along with their J-costs. Researchers modeling mass-to-light ratios via recognition cost minimization cite this as the input object. It is supplied directly as a Lean structure definition whose namespace fields apply the J function to each ratio.
claimA stellar configuration consists of positive real numbers $r_>0$ and $r_>0$ for the scale ratios of emission and storage events, together with the associated recognition costs $J(r_)$ and $J(r_)$ where $J(x)=½(x+1/x)-1$.
background
The module derives stellar mass-to-light ratios from the recognition cost differential between photon emission and bound-mass storage under stellar collapse. Emission carries cost $J(r_emit)$ and storage carries $J(r_store)$, with the equilibrium partition fixed by minimizing total ledger cost. The function $J$ is the convex recognition cost $J(x)=½(x+1/x)-1$ minimized at unity, taken from the multiplicative recognizer cost and the observer-forcing cost definitions.
proof idea
The declaration is a structure definition with four fields (two ratios and their positivity witnesses) followed by a namespace that directly applies the J function to each ratio to obtain δ_emit, δ_store and their difference Δδ.
why it matters in Recognition Science
The structure supplies the concrete input for the module's derivation that equilibrium M/L lies on the phi-ladder as φ^n for integer n in [0,3], matching observed stellar values near 1.618. It links the J-cost from the multiplicative recognizer and observer forcing to astrophysical observables, closing one step in the recognition-weighted collapse strategy.
scope and limits
- Does not assign numerical values to the scale ratios.
- Does not prove existence of an equilibrium partition.
- Does not fix the integer rung n on the phi-ladder.
- Does not incorporate observational constraints or fitting.
formal statement (Lean)
81structure StellarConfig where
82 /-- Scale ratio for photon emission events -/
83 r_emit : ℝ
84 /-- Scale ratio for mass storage events -/
85 r_store : ℝ
86 /-- Both ratios must be positive -/
87 emit_pos : 0 < r_emit
88 store_pos : 0 < r_store
89
90namespace StellarConfig
91
92/-- Recognition cost for emission -/
93noncomputable def δ_emit (cfg : StellarConfig) : ℝ := J cfg.r_emit
proof body
Definition body.
94
95/-- Recognition cost for storage -/
96noncomputable def δ_store (cfg : StellarConfig) : ℝ := J cfg.r_store
97
98/-- Cost differential: Δδ = δ_emit - δ_store -/
99noncomputable def Δδ (cfg : StellarConfig) : ℝ := cfg.δ_emit - cfg.δ_store
100
101end StellarConfig
102
103/-! ## Equilibrium M/L from Cost Minimization -/
104
105/-- The equilibrium mass-to-light ratio from J-minimization.
106
107When the cost differential is n · J_bit = n · log(φ), the equilibrium partition gives:
108 M/L = exp(n · log(φ)) = φ^n
109
110This is because the optimal allocation minimizes total J-cost, and the
111exponential weighting exp(-J) on paths gives Boltzmann-like statistics. -/