pith. sign in
module module high

IndisputableMonolith.UnitMapping

show as:
view Lean formalization →

The UnitMapping module sets up an abstract integer placeholder system for the subgroup generated by δ to handle unit conversions in Recognition Science. It supplies conversion functions fromZ and toZ plus specialized maps for charge, time, and action. The module consists of definitions for affine maps over Z together with consistency relations. Researchers handling discrete tick-based quantities from the Constants module would reference these mappings when translating between abstract units and physical ladders.

claimLet $\Delta$ denote the subgroup generated by an abstract $\delta$. The module defines maps $\mathrm{fromZ}:\mathbb{Z}\to\Delta$ and $\mathrm{toZ}:\Delta\to\mathbb{Z}$ satisfying the round-trip identity, together with affine maps over $\mathbb{Z}$ for charge, time, and action quantities.

background

The module imports Constants, whose sole content is the definition of the fundamental RS time quantum $\tau_0=1$ tick. It introduces DeltaSub as the subgroup generated by $\delta$, treated strictly as an abstract placeholder that uses integers for mapping purposes only. Sibling definitions include AffineMapZ, apply, mapDelta, chargeMap, timeMap, actionMap, and mapDeltaCharge, which extend the integer mappings to the listed physical quantities.

proof idea

This is a definition module, no proofs. The structure consists of a sequence of definitions establishing the integer-to-delta conversions and the specialized maps for charge, time, and action.

why it matters in Recognition Science

The module supplies the abstract unit-conversion layer that supports consistent handling of charge, time, and action quantities throughout the Recognition Science framework. It connects the integer placeholders directly to the $\delta$-subgroup, providing the infrastructure needed for any later constructions that translate between tick units and the phi-ladder or mass formulas. No downstream theorems are listed, confirming its role as foundational scaffolding rather than a terminal result.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (21)