Masses Sector Primitive

Sector primitives

Masses sector primitive is a recognition structure in the Recognition Science account of particle masses. It pairs a ribbon word with a reduction condition: the word must already be in normal form. The structure is called primitive because it is the smallest unit the mass-sector account intends to build on, a witness record for ribbon-based mass ladders.

The module that defines it is explicit about its own status. Every declaration in the module concludes in True or another tautology, so none of them is a result. The docstring states this directly: the module records what the account intends to establish, and the intent is not the establishment. The structure and its delta function are documentation, not proof.

What the module does establish, in plain language, is a shape for future work. A primitive is a ribbon word in normal form, and deltaOf reads the rung offset of that word for a given generator class. These definitions give the mass-sector account a vocabulary for stating claims, but they do not yet state any claim about actual masses. The upgrade path is recorded alongside the definitions: replace a placeholder with a target proposition that states the real claim, then prove it.

MODEL Primitive · IndisputableMonolith/Masses/SectorPrimitive.lean

MODEL deltaOf · IndisputableMonolith/Masses/SectorPrimitive.lean

What this page does not claim

No mass value is derived or predicted by this module. No theorem about particle masses is established here. The physical recognition-to-linking bridge is not established by these definitions.

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/SectorPrimitive.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: