Masses Kernel Types

Masses kernel types

Masses kernel types are the formal data structures in Recognition Science that describe a particle's gauge quantum numbers and its position on the mass ladder. The module KernelTypes defines these structures in Lean 4, giving a precise language for talking about particle masses without yet assigning any numerical value.

The central structure is GaugeSkeleton, which records three gauge properties: the hypercharge Y as a rational number, a Boolean flag for color representation, and a Boolean flag for weak isospin doublet status. A second structure, Completion, stores three integers nY, n3, and n2, which together encode the completed gauge data. A third structure, WordLength, maps a GaugeSkeleton and a Completion to a natural number, giving the length of a word in the mass ladder.

The module also defines a generation class GenClass with three values g1, g2, and g3. Each generation has a fixed integer offset tauOf: 0 for g1, 11 for g2, and 17 for g3. A RungSpec combines a natural number ell with a GenClass, and the function rungOf adds the generation offset to ell, yielding the total rung integer. This rung is the position on the phi-power ladder that determines the particle's mass.

These definitions establish the scaffolding for the mass ladder but do not by themselves derive any particle mass. They are the vocabulary in which later theorems about the phi-power scaling law are stated. The structures are definitional choices, not established results.

MODEL GaugeSkeleton · IndisputableMonolith/Masses/KernelTypes.lean

MODEL Completion · IndisputableMonolith/Masses/KernelTypes.lean

MODEL tauOf · IndisputableMonolith/Masses/KernelTypes.lean

MODEL rungOf · IndisputableMonolith/Masses/KernelTypes.lean

What this page does not claim

No particle mass is derived in this module. No claim that the gauge quantum numbers are forced by the framework. No claim that the generation offsets are derived rather than chosen.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Masses/KernelTypes.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: