pith. machine review for the scientific record. sign in
module module high

IndisputableMonolith.UnitMapping

show as:
view Lean formalization →

The UnitMapping module supplies an abstract integer placeholder for the subgroup generated by the unit δ in Recognition Science. It equips charge, time, and action mappings with conversion functions between Z and this cyclic subgroup. The module consists entirely of definitions and basic lemmas drawn from group theory, with no derivations or numerical content.

claimLet $G$ be a group and let $δ ∈ G$. The module defines the cyclic subgroup $⟨δ⟩$ together with maps fromZ : ℤ → ⟨δ⟩ and toZ : ⟨δ⟩ → ℤ satisfying toZ ∘ fromZ = id, plus derived maps for charge, time, and action.

background

Recognition Science takes the fundamental time quantum τ₀ = 1 tick from the Constants module as its RS-native unit. The present module introduces an abstract placeholder for physical units by treating δ as a generator and using the integers Z solely as a mapping device. It defines DeltaSub as the subgroup generated by δ, supplies the bidirectional maps fromZ and toZ, and builds auxiliary maps including chargeMap, timeMap, actionMap, and mapDeltaCharge.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the integer scaffolding required for unit transformations that appear throughout the Recognition framework. It directly enables the sibling definitions of chargeMap, timeMap, and actionMap, which in turn support mass formulas on the phi-ladder and the eight-tick octave structure. No downstream theorems are listed, indicating this layer remains foundational rather than terminal.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (21)