ZeroParametersClaim
The ZeroParametersClaim structure asserts that the golden ratio φ serves as the sole input, with the full set of physical constants obtained strictly as functions of φ. Researchers deriving parameter-free models in Recognition Science would cite this to record that no external scales or free parameters enter the constant chain. The declaration is realized directly as a structure whose three fields are the trivial proposition True, a reference to the DerivedConstants bundle, and the trivial proposition True.
claimLet φ be the golden ratio satisfying φ² = φ + 1. All constants E_coh, τ₀, c, ℏ, G, and α⁻¹ are obtained as functions of φ alone via the gate identities, with no additional free parameters introduced.
background
The module RRF.Foundation.Constants packages the claim that every physical constant descends from φ through a fixed derivation chain φ → E_coh → τ₀ → c → ℏ → G → α⁻¹. DerivedConstants is the structure that bundles these quantities together with the golden-ratio relation phi_golden : phi² = phi + 1. The local setting is the RRF interface, a non-sealed recognition field (Fin 4 → ℝ) → ℝ, whose constants are required to satisfy the IR gate ℏ = E_coh · τ₀ and the Planck gate (c³ λ_rec²) / (ℏ G) = 1/π.
proof idea
This declaration is a structure definition with no proof body. Its three fields are filled by the propositions True, the DerivedConstants bundle, and True; no lemmas or tactics are invoked.
why it matters in Recognition Science
The structure records the zero-parameters claim that anchors the entire constant derivation in the Recognition framework. It supports the downstream identities listed in the module (IR gate, Planck gate, K-gates) and the eight-tick octave that forces D = 3. The open question it touches is the completion of the full derivation chain from φ to the numerical SI values.
scope and limits
- Does not supply explicit functional forms for E_coh(φ) or the remaining constants.
- Does not perform numerical calibration against measured SI values.
- Does not prove the gate identities themselves.
- Does not address stability of the derived constants under small perturbations of φ.
formal statement (Lean)
180structure ZeroParametersClaim where
181 /-- φ is the only input. -/
182 input_is_phi : True
183 /-- All constants are functions of φ. -/
184 constants_from_phi : DerivedConstants
185 /-- No additional parameters were introduced. -/
186 no_free_params : True
187
188end RRF.Foundation
189end IndisputableMonolith