Encyclopedia Astrophysics Astrophysics Nucleosynthesis Tiers Tiers Are Quantized
ARTICLE 4 claims 4 theorems
Astrophysics Nucleosynthesis Tiers Tiers Are Quantized
A machine-checked theorem states that nuclear and luminosity tiers differ by an integer, a claim far narrower than its name suggests.
The quantized tier theorem
In the Recognition Science framework, physical quantities such as nuclear density and photon luminosity are assigned to discrete tiers, each a power of the golden ratio φ. The theorem tiers_are_quantized states that for any two such tiers, their difference is an integer. In plain terms, the framework proves that the gap between a nuclear tier and a luminosity tier is a whole number, not a fraction. This is a statement about the framework's own model, not an empirical law of astrophysics.
The theorem is a formal consequence of a definition. The framework defines a property called eight_tick_quantizes_tiers, which asserts that for any two integer tiers, their difference is an integer. The proof is immediate: for any integers ρ and L, the difference ρ − L is itself an integer. The declaration therefore establishes a tautology within the framework's type system. It does not derive the value of any tier, nor does it connect tiers to any measured physical quantity.
The framework's library does contain further theorems that give the tier difference a specific value. A separate theorem, tier_difference_value, proves that the difference between the local nuclear tier 12 and the local luminosity tier 11 equals 1. This yields a mass-to-light ratio of φ^1, approximately 1.618 in solar units. Another theorem, strategies_agree, shows that this nucleosynthesis-derived ratio matches a value obtained from a different stellar assembly model. These are all internal consistency results within the framework.
What the theorem does not claim is broader. It does not assert that any real astrophysical object has a mass-to-light ratio of exactly φ. It does not prove that nuclear reactions occur in eight-tick windows; that statement appears only in a docstring as an informal description. The theorem does not establish that the golden ratio is the unique possible scaling for nucleosynthesis. It only proves a trivial algebraic identity about integer differences, within a framework that chooses to represent physical quantities as φ-powers.
The practical consequence is modest but clear: within the Recognition Science model, the mass-to-light ratio derived from tier differences is constrained to a small set of φ-powers. The framework's own theorems bound this ratio between 1 and 5, and the specific local computation fixes it at φ. A reader can verify that the formal statement is true, and equally verify that its scope is limited to the framework's definitions.
THEOREM tiers_are_quantized · IndisputableMonolith/Astrophysics/NucleosynthesisTiers.lean
theorem tiers_are_quantized : eight_tick_quantizes_tiers := by
intro ρ L
use ρ - L
THEOREM tier_difference_value · IndisputableMonolith/Astrophysics/NucleosynthesisTiers.lean
theorem tier_difference_value : tier_difference = 1 := by
unfold tier_difference nuclear_tier_local luminosity_tier_local
norm_num
THEOREM strategies_agree · IndisputableMonolith/Astrophysics/NucleosynthesisTiers.lean
/-- Nucleosynthesis M/L agrees with stellar assembly M/L -/
theorem strategies_agree :
ml_nucleosynthesis = StellarAssembly.ml_stellar := by
rw [ml_nucleosynthesis_eq_phi, StellarAssembly.ml_stellar_value]
rfl
THEOREM ml_from_phi_tier_structure · ml_matches_stellar_observations · IndisputableMonolith/Astrophysics/NucleosynthesisTiers.lean
/-- **Main Theorem**: The stellar M/L ratio is derived from φ-tier structure
of nucleosynthesis, quantized by the eight-tick cycle.
This provides an independent derivation matching Strategy 1. -/
theorem ml_from_phi_tier_structure :
∃ Δn : ℤ, Δn ∈ population_tiers ∧
ml_nucleosynthesis = φ ^ Δn ∧
1 ≤ ml_nucleosynthesis ∧ ml_nucleosynthesis < 5 := by
use 1
refine ⟨?_, ?_, ?_, ?_⟩
· simp only [population_tiers, Set.mem_insert_iff, Set.mem_singleton_iff]
simp
· rw [ml_nucleosynthesis_eq_phi]; simp [zpow_one]
· rw [ml_nucleosynthesis_eq_phi]; exact le_of_lt Constants.one_lt_phi
· rw [ml_nucleosynthesis_eq_phi]
calc φ < 2 := Constants.phi_lt_two
_ < 5 := by norm_num
/-- The nucleosynthesis M/L matches observations.
Observed stellar M/L:
- Main sequence: 0.5 - 3 solar units
- Giants: 2 - 10 solar units
- Population averages: 1 - 5 solar units
Predicted: φ^1 ≈ 1.618 solar units (typical)
φ^2 ≈ 2.618 solar units (evolved)
This is within the observed range. -/
theorem ml_matches_stellar_observations :
1 < ml_nucleosynthesis ∧ ml_nucleosynthesis < 5 := by
rw [ml_nucleosynthesis_eq_phi]
constructor
· exact Constants.one_lt_phi
· calc φ < 2 := Constants.phi_lt_two
_ < 5 := by norm_num
What this page does not claim
The theorem does not assert that any real astrophysical object has a mass-to-light ratio of exactly φ. The theorem does not prove that nuclear reactions occur in eight-tick windows; that statement appears only in a docstring as an informal description. The theorem does not establish that the golden ratio is the unique possible scaling for nucleosynthesis.
Verify this page
Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:
$ lake env lean IndisputableMonolith/Astrophysics/NucleosynthesisTiers.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)
A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.
Derived articles
This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red:
- What empirical evidence, if any, connects the framework's φ-power tiers to measured nuclear densities or stellar luminosities?
- How does the framework derive the specific local tier values 12 and 11 from physical principles rather than choosing them?
- Does the eight-tick cycle, mentioned in the docstring, have a formal theorem that connects it to nuclear reaction timing?
- What distinguishes the framework's discrete φ-tier model from a continuous scaling model in making testable predictions?
MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND
THEOREM tiers_are_quantized · IndisputableMonolith/Astrophysics/NucleosynthesisTiers.lean
theorem tiers_are_quantized : eight_tick_quantizes_tiers := by intro ρ L use ρ - LThe theorem tiers_are_quantized states that for any two such tiers, their difference is an integer. tiers_are_quantized · IndisputableMonolith/Astrophysics/NucleosynthesisTiers.leanTHEOREM tier_difference_value · IndisputableMonolith/Astrophysics/NucleosynthesisTiers.lean
theorem tier_difference_value : tier_difference = 1 := by unfold tier_difference nuclear_tier_local luminosity_tier_local norm_numA separate theorem, tier_difference_value, proves that the difference between the local nuclear tier 12 and the local luminosity tier 11 equals 1. tier_difference_value · IndisputableMonolith/Astrophysics/NucleosynthesisTiers.leanTHEOREM strategies_agree · IndisputableMonolith/Astrophysics/NucleosynthesisTiers.lean
/-- Nucleosynthesis M/L agrees with stellar assembly M/L -/ theorem strategies_agree : ml_nucleosynthesis = StellarAssembly.ml_stellar := by rw [ml_nucleosynthesis_eq_phi, StellarAssembly.ml_stellar_value] rflAnother theorem, strategies_agree, shows that this nucleosynthesis-derived ratio matches a value obtained from a different stellar assembly model. strategies_agree · IndisputableMonolith/Astrophysics/NucleosynthesisTiers.leanTHEOREM ml_from_phi_tier_structure · ml_matches_stellar_observations · IndisputableMonolith/Astrophysics/NucleosynthesisTiers.lean
/-- **Main Theorem**: The stellar M/L ratio is derived from φ-tier structure of nucleosynthesis, quantized by the eight-tick cycle. This provides an independent derivation matching Strategy 1. -/ theorem ml_from_phi_tier_structure : ∃ Δn : ℤ, Δn ∈ population_tiers ∧ ml_nucleosynthesis = φ ^ Δn ∧ 1 ≤ ml_nucleosynthesis ∧ ml_nucleosynthesis < 5 := by use 1 refine ⟨?_, ?_, ?_, ?_⟩ · simp only [population_tiers, Set.mem_insert_iff, Set.mem_singleton_iff] simp · rw [ml_nucleosynthesis_eq_phi]; simp [zpow_one] · rw [ml_nucleosynthesis_eq_phi]; exact le_of_lt Constants.one_lt_phi · rw [ml_nucleosynthesis_eq_phi] calc φ < 2 := Constants.phi_lt_two _ < 5 := by norm_num/-- The nucleosynthesis M/L matches observations. Observed stellar M/L: - Main sequence: 0.5 - 3 solar units - Giants: 2 - 10 solar units - Population averages: 1 - 5 solar units Predicted: φ^1 ≈ 1.618 solar units (typical) φ^2 ≈ 2.618 solar units (evolved) This is within the observed range. -/ theorem ml_matches_stellar_observations : 1 < ml_nucleosynthesis ∧ ml_nucleosynthesis < 5 := by rw [ml_nucleosynthesis_eq_phi] constructor · exact Constants.one_lt_phi · calc φ < 2 := Constants.phi_lt_two _ < 5 := by norm_numThe framework's own theorems bound this ratio between 1 and 5, and the specific local computation fixes it at φ. ml_from_phi_tier_structure · ml_matches_stellar_observations · IndisputableMonolith/Astrophysics/NucleosynthesisTiers.lean