Resolution
plain-language theorem explainer
The declaration records the formal resolution of Gap 6 by assigning quark coordinate conventions to distinct layers: integer rungs as the parameter-free core and quarter-ladder as an exploratory hypothesis. Mass-derivation work in the Recognition framework cites it to mark which results stay inside the canonical phi-ladder and which remain phenomenological. The structure is assembled by direct field assignment of status strings and convention tags with no lemmas or reductions required.
Claim. Gap 6 is resolved by the record whose status field equals the string RESOLVED_BY_LAYER_SEPARATION, whose method field equals Layer separation (Core vs Hypothesis), whose core convention is the integer-rung convention, whose hypothesis convention is the quarter-ladder convention, whose equivalence-proved flag is false, and whose summary states that integer rungs belong to the core while the quarter-ladder remains a hypothesis with no equivalence required.
background
Recognition Science places all particle masses on the phi-ladder via the formula m = yardstick(Sector) × φ^(r − 8 + gap(Z)), where r is an integer rung and the yardstick is sector-specific. Two quark conventions appear: integer rungs (core, parameter-free, derived from cube geometry) and quarter-integer residues (hypothesis layer, tuned for <2 % accuracy on heavy quarks). The module states explicitly that these conventions serve different purposes and are not required to be equivalent.
proof idea
The declaration is a structure definition whose fields receive literal default values. Core convention is set to IntegerRung, hypothesis convention to QuarterLadder, equivalence proved to false, and the summary string is concatenated directly; no tactics, lemmas, or upstream results are invoked.
why it matters
It closes Gap 6 by layer separation, allowing downstream theorems such as the proton-electron mass ratio and alpha-lock numerical bounds to depend only on the core integer-rung convention. The structure feeds cosmological-constant derivations and electron-mass positivity statements while keeping quarter-ladder adjustments marked as hypothesis. It supports the phi-ladder mass formula and the eight-tick octave without introducing new parameters.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.