optimal_ratio_is_phi_power
plain-language theorem explainer
The result establishes that the optimal mass-to-light ratio under observability constraints equals a power of the golden ratio φ with exponent restricted to the set {0,1,2,3}. Astrophysicists deriving M/L from J-cost minimization in stellar systems would cite this when combining mass-assembly and light-emission bounds. The proof is a one-line term construction that supplies the witness 1 and reduces membership by simplification.
Claim. There exists an integer $n$ with $n$ in the set ${0,1,2,3}$ such that the optimal ratio of mass assembly scale to light-emission scale satisfies $r_ {mass}/r_{light}=φ^n$.
background
The ObservabilityLimits module derives the mass-to-light ratio from recognition-bounded constraints. Observable flux must exceed the threshold $F_{threshold}$ set by coherent energy $E_{coh}$ divided by the fundamental tick $τ_0$, while mass assembly is limited by coherence volume $V∼l_{rec}^3$. Total J-cost is defined as $J_{total}=J_{mass}(M)+J_{light}(L)$ and minimized subject to these bounds, producing the discrete set of allowed ratios. This setting rests on the PrimitiveDistinction.from theorem, which extracts four structural conditions plus three definitional facts from seven axioms, together with the Recognition ledger L (debit and credit both constantly 1) and structure M (universe U with recognition map recog), including their three-state Cycle3 variants that enforce conservation.
proof idea
The proof is a term-mode construction. The tactic 'use 1' supplies the integer witness n=1. The subsequent 'simp' call reduces the membership predicate to a direct check that 1 lies in the finite set {0,1,2,3}.
why it matters
The declaration supplies the main result quoted in the module documentation: M/L lies in {φ^n : n∈[0,3]}, with the typical value φ matching the outputs of Strategies 1 and 2. It instantiates J-minimization under the Recognition Composition Law and the phi-ladder forced by the T5–T6 steps of the unified forcing chain. No downstream theorems are recorded, so the integration of this discrete set into full stellar-assembly or nucleosynthesis calculations remains open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.