ModelLayer
plain-language theorem explainer
ModelLayer enumerates three layers for assigning quark coordinate conventions in Recognition Science. Researchers reconciling integer-rung core masses with quarter-ladder phenomenology cite it to keep the parameter-free geometric derivation separate from exploratory adjustments. The declaration is a plain inductive definition with three constructors and no proof content.
Claim. An inductive type with three constructors: Core (parameter-free derivation from geometry), Hypothesis (phenomenological placement not yet derived), and Empirical (input taken directly from experiment).
background
The module resolves two quark coordinate conventions by explicit layer assignment rather than forcing equivalence. IntegerRung places all particles on integer rungs of the phi-ladder with sector yardsticks; QuarterLadder places quarks on quarter-integer residues relative to the electron structural mass. ModelLayer supplies the target type for that assignment. Upstream, the PrimitiveDistinction.from theorem reduces seven axioms to four structural conditions plus three definitional facts, while the CPM2D.Hypothesis structure bundles the projection-defect and energy-control data needed for model construction.
proof idea
Inductive definition with three named constructors. No lemmas or tactics are applied; the declaration simply introduces the type and its cases for later use in pattern-matching functions such as convention_layer.
why it matters
ModelLayer supplies the codomain for convention_layer, which maps IntegerRung to Core and QuarterLadder to Hypothesis. It thereby closes the gap-resolution step described in the module header, keeping the canonical integer-rung derivation (T5 J-uniqueness, T6 phi fixed point, T8 D=3) distinct from the exploratory quarter-ladder. The definition touches the open question whether the quarter-ladder residues can be derived from geometry without additional hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.