Convention
The Convention inductive type enumerates the integer-rung convention for the core parameter-free quark mass model and the quarter-ladder convention for the exploratory hypothesis layer. Mass hierarchy researchers cite it to keep geometry-derived results separate from phenomenological adjustments on the phi-ladder. The declaration is a plain inductive enumeration with two constructors and deriving clauses for Repr and DecidableEq.
claimThe inductive type of quark coordinate conventions consisting of the constructor for integer rungs on the phi-ladder (core model) and the constructor for quarter-integer residues relative to the electron mass base (hypothesis layer).
background
Recognition Science places particle masses on the phi-ladder by the formula m = yardstick(S) * phi^(r-8 + gap(Z)), with integer rungs derived from cube geometry for the core model. The module resolves Gap 6 by documenting that the two conventions serve distinct purposes and are assigned to different layers rather than being equivalent. Upstream structures include the mass anchor in Masses.Anchor for integer rungs, PhiForcingDerived for J-cost, and SpectralEmergence for the gauge and generation content that fixes D=3 and the eight-tick octave.
proof idea
The declaration is an inductive definition with two constructors IntegerRung and QuarterLadder, plus deriving Repr and DecidableEq. No lemmas or tactics are invoked; it functions as a type-level tag for layer separation.
why it matters in Recognition Science
This definition supplies the domain for convention_layer, which maps IntegerRung to Core and QuarterLadder to Hypothesis, and for the Resolution structure that records Gap 6 as resolved by layer separation. It supports downstream applications in BornRule.born_rule_from_C and RecognitionThermodynamics.ProbabilityDistribution by clarifying which mass formula applies in each context. The separation preserves the canonical integer-rung status tied to T6 phi fixed point and D=3 while isolating the quarter-ladder hypothesis.
scope and limits
- Does not claim the two conventions are mathematically equivalent.
- Does not derive the specific quarter-rung values or their error bounds.
- Does not compute any mass values or gap corrections.
- Does not interface directly with J-cost minimization or forcing chain steps.
Lean usage
def convention_layer : Convention → ModelLayer | .IntegerRung => .Core | .QuarterLadder => .Hypothesisformal statement (Lean)
99inductive Convention
100 | IntegerRung -- Convention A: integer rungs, sector yardsticks
101 | QuarterLadder -- Convention B: quarter rungs, electron mass base
102 deriving Repr, DecidableEq
103
104/-- Formal assignment of conventions to layers -/