pith. sign in
module module high

IndisputableMonolith.RecogSpec.Core

show as:
view Lean formalization →

RecogSpec.Core supplies the foundational ledger carrier augmented with optional bookkeeping data. Downstream modules RSBridge and RSLedger import it to derive mixing angles from geometric couplings and mass ratios from generation torsion. The module enables projection of canonical states without extra structure. It is a definition module containing no theorems.

claimThe module defines a ledger carrier type augmented with optional bookkeeping data, written as ledger carrier with bookkeeping data, to support projection of canonical states.

background

This module occupies the base layer of the RecogSpec domain. It imports ObservablePayloads, which supplies strongly typed records for dimensionless mass-ratio and mixing-angle payloads that replace raw List ℝ fields. The supplied doc-comment states the purpose: basic ledger carrier augmented with optional bookkeeping data so downstream modules can project canonical states without introducing additional structure.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module is imported by RSBridge, which defines the rich bridge structure for deriving mixing angles from geometric couplings where CKM mixing angles come from ledger geometry. It is also imported by RSLedger, which defines the rich ledger structure for deriving mass ratios from generation torsion where particle masses occupy discrete rungs on the φ-ladder. It supplies the base carrier for the entire RecogSpec specification layer.

scope and limits

used by (2)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (26)