ZeroParamScaleFree
plain-language theorem explainer
The structure encodes the proposition that the closure-delay survival law is scale-free, taking a power-law form in dimensionless time ratios. Researchers formalizing the A6 step in the Recognition Science framework would cite it when bridging zero-parameter closure to the absence of any characteristic timescale. The declaration is a one-field structure whose Prop field is instantiated directly from the no-characteristic-time property supplied by zero-parameter closure.
Claim. The structure asserts that the survival law of the closure delay obeys a power-law dependence on the dimensionless time ratio, i.e., $P(t_1/t_2) = (t_1/t_2)^{ - n}$ for some index $n$, with no preferred scale present.
background
This module formalizes the A6 step as a proposition-level bridge: zero-parameter closure excludes a characteristic timescale, so the closure-delay survival law must be scale-free. The local setting records the dimensional argument that forces scale invariance once all dimensionful parameters are removed by closure.
proof idea
The declaration is a structure definition that introduces the single proposition field encoding the power-law form. It functions as a packaging wrapper; the field is supplied downstream by the no-characteristic-time property of zero-parameter closure.
why it matters
This structure is the target type for the zero-parameter-forces-scale-free definition that packages the dimensional argument. It fills the A6 step by recording that the survival law must be scale-free, connecting directly to the power definition that supplies the observed best-fit spectrum $P(k) = A (k/k_p)^{n_s-1}$. It touches the forcing chain by enforcing the scale-free requirement that precedes the eight-tick octave and spatial dimension count.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.