convention_layer
plain-language theorem explainer
convention_layer assigns quark coordinate conventions to model layers, sending the integer-rung convention to the core layer and the quarter-ladder convention to the hypothesis layer. Mass-derivation researchers cite it to separate parameter-free geometric results from phenomenological adjustments. The definition is realized by exhaustive pattern matching on the two constructors of the Convention type.
Claim. The function mapping conventions to layers satisfies $convention_layer(IntegerRung) = Core$ and $convention_layer(QuarterLadder) = Hypothesis$.
background
The Quark Coordinate Conventions module resolves two coexisting placements of quarks on the phi-ladder by explicit layer separation. Integer Rungs (Convention A) place all particles on integer rungs with sector yardsticks derived from cube geometry and form the canonical core. Quarter-Ladder (Convention B) places quarks on quarter-integer residues relative to electron structural mass and is treated as exploratory.
proof idea
Defined by direct pattern matching on the Convention inductive type: IntegerRung maps to Core and QuarterLadder maps to Hypothesis. No lemmas or tactics are invoked.
why it matters
This definition supplies the layer assignment used by the downstream theorems core_uses_integer_rungs and quarter_ladder_is_hypothesis. It fills the documented resolution of Gap 6 by recording that the integer-rung convention belongs to the parameter-free core while the quarter-ladder convention remains a hypothesis, consistent with the phi-ladder mass formula and the distinction between core and exploratory layers.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.