nuclear_tier_local
plain-language theorem explainer
nuclear_tier_local assigns the integer 12 as the nuclear tier index on the φ-ladder inside the stellar scale window. Astrophysicists computing mass-to-light ratios from nucleosynthesis tiers cite this constant to obtain Δn = 1. The assignment is a direct constant definition that feeds tier difference calculations without invoking lemmas.
Claim. The canonical nuclear tier index on the φ-ladder is the integer $12$.
background
Recognition Science places nuclear densities on discrete φ-tiers with ρ_nuc ~ φ^{n_nuclear} × ρ_Planck. The module derives M/L from the tier difference between nuclear and photon luminosities under the eight-tick cycle, which forces integer Δn and yields M/L ∈ {φ^n : n ∈ [0, 3]} with typical value φ^1. A φ-tier is an integer index on the φ-ladder. Upstream results include the scale function computing φ^k and bandwidth constraints from RecognitionBandwidth.
proof idea
This is a direct definition that assigns the constant 12 to nuclear_tier_local with type ascription to PhiTier. No lemmas or tactics are applied beyond the one-line constant binding.
why it matters
This definition supplies the nuclear tier to tier_difference and ml_nucleosynthesis_eq_phi, which prove the nucleosynthesis M/L equals φ. It fills the eight-tick nucleosynthesis step in the Recognition framework, where the eight-tick octave and φ-ladder quantize energy release and close the M/L match between strategies. The value aligns with the local stellar window from eight-tick analysis of the nuclear-to-Planck density ratio.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.