agrees_with_nucleosynthesis
plain-language theorem explainer
The geometric mass-to-light ratio derived from recognition length and coherence constraints equals the nucleosynthesis-derived mass-to-light ratio. Astrophysicists modeling stellar assembly from recognition science would cite this to establish cross-strategy consistency. The proof is a term reduction that unfolds the geometric definition to the golden ratio and rewrites the nucleosynthesis side via its equality theorem before reflexivity.
Claim. Let $M/L$ denote the stellar mass-to-light ratio. The value obtained from geometric observability constraints on recognition length $l_{rec}$ and coherence energy equals the value obtained from nucleosynthesis tier differences: $M/L_{geometric} = M/L_{nucleosynthesis}$.
background
The module derives the stellar mass-to-light ratio under Strategy 3 from observability constraints: photon flux must exceed the recognition threshold $E_{coh}/τ_0$ and mass assembly is bounded by coherence volume $V ~ l_{rec}^3$. Here $l_{rec}$ is the recognition length defined as the square root of $1/π$ (Planck-scale proxy). The geometric mass-to-light ratio is defined directly as the golden ratio φ. The nucleosynthesis mass-to-light ratio is defined as the phi-ladder evaluated at the tier difference between nuclear and luminosity tiers. An upstream theorem states that this nucleosynthesis ratio equals φ.
proof idea
The proof is a term-mode reduction. It unfolds the geometric mass-to-light definition, applies the nucleosynthesis equality theorem that reduces the right-hand side to φ, and closes by reflexivity.
why it matters
This equality supplies one of the required identities in the main theorem ml_from_geometry_only, which asserts existence of an M/L ratio equal to φ that simultaneously matches the geometric, stellar-assembly, and nucleosynthesis derivations. It thereby closes the consistency loop for Strategy 3 within the Recognition Science framework and supports the phi-ladder mass formula together with eight-tick quantization.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.