DimlessPack
plain-language theorem explainer
DimlessPack defines a record structure that collects dimensionless observables such as the fine-structure constant, lepton mass ratios, CKM mixing angles, muon g-2, and three propositions for strong CP neutrality, eight-tick minimality, and the Born rule, all extracted relative to a given ledger and bridge. Particle physicists comparing Recognition Science outputs to data would cite this packaging to organize predictions for matching. The definition is a direct structure declaration with no proof obligations or computational content.
Claim. Let $L$ be a ledger (a carrier type with optional state and tick bookkeeping) and $B$ a bridge over $L$ (a minimal wrapper with unit dummy). Then DimlessPack$(L,B)$ is the structure whose fields are the fine-structure constant $α ∈ ℝ$, lepton mass ratios, CKM mixing angles, the muon $g-2$ value, and propositions asserting strong CP neutrality, eight-tick minimality, and the Born rule.
background
RecogSpec.Core defines auxiliary structures for packaging dimensionless predictions that arise once a ledger and bridge are fixed. Ledger supplies a basic carrier type augmented with optional state and tick functions so that downstream modules can project canonical states. Bridge is a minimal wrapper over any ledger, carrying only a unit dummy field to serve as an interface point for equivalence relations and matching propositions.
proof idea
This is a structure definition that directly declares the seven fields with no tactics, reductions, or lemmas applied.
why it matters
DimlessPack supplies the concrete data type consumed by the downstream Matches definition, which asserts that a bridge matches a universal dimensionless set by exhibiting an instance of this structure. It organizes the observable predictions that follow from the forcing chain (T5 J-uniqueness through T7 eight-tick octave) and the Recognition Composition Law, including the alpha band and the eight-tick minimal condition. The structure therefore closes the interface between the abstract ledger-bridge formalism and concrete particle-physics quantities.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.