ZeroParametersClaim
plain-language theorem explainer
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.
Claim. Let φ 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.