gap6_resolved
plain-language theorem explainer
The declaration establishes that gap 6 in quark coordinate conventions is resolved by separating the canonical integer-rung layer from the exploratory quarter-ladder hypothesis, with the status fixed as RESOLVED_BY_LAYER_SEPARATION. Model builders deriving parameter-free masses from geometry would cite it to confirm the core ladder remains integer-valued. The proof is a one-line reflexivity that matches the declared status string directly.
Claim. The status of the gap-6 resolution equals the string ``RESOLVED_BY_LAYER_SEPARATION''.
background
The module QuarkCoordinateReconciliation documents two distinct quark coordinate conventions that are not required to be mathematically equivalent. Convention A places all fermions on integer rungs of the phi-ladder, with up and down quarks using r in {4,15,21} and the mass formula m = yardstick(Sector) * phi^(r-8+gap(Z)). Convention B places quarks on quarter-integer residues relative to the electron structural mass for phenomenological fits under 2 percent for heavy flavors. Upstream rung definitions in Masses.RSBridge.Anchor and Masses.AnchorPolicy supply the integer assignments (e.g., u at 4, c at 15, t at 21) while Constants.RSNativeUnits.status records the phi-ladder base units.
proof idea
The proof is a one-line reflexivity that applies rfl to the definition of gap6_resolution.status, confirming it equals the string RESOLVED_BY_LAYER_SEPARATION by construction.
why it matters
This theorem closes the explicit documentation of gap 6 inside the Recognition framework by separating the canonical core (integer rungs, parameter-free) from the hypothesis layer (quarter-ladder). It feeds the mass-law derivations that rely on the integer phi-ladder and the eight-tick octave structure. No downstream theorems are recorded yet; the result stands as a terminal resolution marker for the quark coordinate conventions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.