GlobalOnlyPolicy
plain-language theorem explainer
GlobalOnlyPolicy encodes the requirement that all ILG parameters are fixed by phi alone with zero per-galaxy adjustments. Researchers running the SPARC chi-squared falsification test cite it to guarantee the model uses only catalog-level constants derived from the golden ratio. The declaration is a plain structure definition whose four fields assert the required equalities.
Claim. The global-only policy requires that the locked fine-structure parameter satisfies $alpha_locked = (1 - phi^{-1})/2$, the locked mass-to-light ratio satisfies $upsilon_locked = phi$, the locked lag coupling satisfies $clag_locked = phi^{-5}$, and the number of per-galaxy free parameters equals zero.
background
In the SPARC falsifier module the ILG rotation-curve model is evaluated with every parameter locked to a value computed from phi. Upstream definitions supply the concrete locks: alpha_locked equals (1 - 1/phi)/2, upsilon_locked equals phi, clag_locked equals phi to the power -5, and per_galaxy_free_parameters is the constant zero. These locks originate in Constants.ILG and CouplingLockIn, where the same alpha expression is introduced as the geometric lock-in condition at the recognition scale.
proof idea
This is a structure definition with an empty proof body. The four fields are written directly as the required equalities; no lemmas or tactics are applied.
why it matters
The structure supplies the global-only constraint demanded by the downstream SPARCFalsifierCert certificate and the global_only_policy theorem. It formalizes the module's claim that ILG predictions depend only on phi-derived constants, thereby enabling the zero-free-parameter median-chi-squared test across the SPARC sample. In the Recognition framework it completes the parameter-locking step that precedes any falsification decision.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.