StellarConfig
plain-language theorem explainer
StellarConfig packages two positive real scale ratios r_emit and r_store for photon emission and mass storage events, together with the associated recognition costs δ_emit = J(r_emit) and δ_store = J(r_store) and their difference Δδ. Modelers of stellar collapse who minimize total J-cost to obtain equilibrium mass-to-light ratios on the phi-ladder would cite this structure. The definition is a direct packaging of the J function applied to the two ratios with positivity guards.
Claim. A stellar configuration consists of positive reals $r_>0$ (emission scale) and $s_>0$ (storage scale) together with the recognition costs $J(r)$, $J(s)$ and the differential $J(r)-J(s)$, where $J(x)=½(x+1/x)-1$.
background
J is the recognition cost function J(x) = ½(x + 1/x) - 1, minimized at x=1 with value 0, imported from Cost.Jcost. The module derives stellar mass-to-light ratios from the recognition cost differential between photon emission and mass storage during collapse. Upstream, cost is the J-cost of a recognition event or the derived cost of a multiplicative recognizer comparator; the eight-tick octave and phi-ladder supply the integer steps that turn a cost differential n·J_bit into M/L = phi^n.
proof idea
One-line wrapper that applies the J definition to each scale ratio and subtracts the results; the structure fields simply record the two positive inputs and the three derived reals.
why it matters
This structure supplies the input data for the equilibrium M/L derivation stated in the module doc-comment: when the cost differential equals n·J_bit the partition yields M/L = phi^n with n fixed by the eight-tick structure. It therefore sits inside the Recognition Science strategy that obtains observed stellar M/L values from J-minimization on the phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.