KGateMeasurement
plain-language theorem explainer
KGateMeasurement packages measured recurrence time τ_rec and kinetic length λ_kin with an RS units pack and uncertainties to derive the bridge ratio K from each route. Experimental tests of the predicted dimensionless K = φ^{1/2} would cite this structure when comparing time-first and length-first determinations. The definition is a direct field projection that normalizes each measured quantity by the corresponding fundamental unit from the supplied RSUnits pack.
Claim. A record containing measured recurrence time τ_rec, kinetic length λ_kin, an RS units structure, and uncertainties σ_τ, σ_λ, from which the bridge ratios are obtained by K_τ = τ_rec / τ₀ and K_λ = λ_kin / ℓ₀.
background
RSUnits is the minimal structure holding fundamental time unit τ₀, length unit ℓ₀, and speed c satisfying c τ₀ = ℓ₀. The bridge ratio K is defined non-circularly as φ^{1/2}. This structure sits in the module on dimensionless bridge ratio K and display equalities, providing the data container for comparing the two routes to K. Upstream, tau0 supplies the fundamental tick duration, ell0 the voxel length, and K the dimensionless ratio derived as the square root of phi.
proof idea
The structure is introduced by direct field definitions that compute K_from_tau as the ratio of measured recurrence time to the fundamental tau0 and K_from_lambda as measured kinetic length over ell0.
why it matters
This structure supplies the input type for validateKGate and falsifier_K_gate_mismatch, which check whether the two routes to K agree within uncertainty. It closes the measurement protocol for the dimensionless K = φ^{1/2} in the constants derivation chain, allowing experimental tests of the Recognition Science prediction for the bridge factor.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.