Pith. sign in
module module low

IndisputableMonolith.Physics.CPViolationFromRS

show as:
view Lean formalization →

The Physics.CPViolationFromRS module defines CP violation processes and certificates in the Recognition Science framework. It depends on the Constants module supplying the RS time quantum τ₀ = 1 tick. The module introduces CPProcess, cpProcess_count, CPViolationCert, and cpViolationCert as its core objects. This is a definition module containing no proofs.

claimThe module defines $\mathrm{CPProcess}$ and $\mathrm{CPViolationCert}$ (with associated count and certificate functions) for CP violation arising in Recognition Science.

background

The module resides in the Physics domain and imports Mathlib together with IndisputableMonolith.Constants. The upstream Constants module supplies the fundamental RS time quantum (RS-native) τ₀ = 1 tick. The module introduces the sibling definitions CPProcess, cpProcess_count, CPViolationCert, and cpViolationCert. The local theoretical setting is the derivation of particle-physics features such as CP violation from the single RS functional equation.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

This module supplies the structures needed to address CP violation inside the Recognition Science framework. It supports the overall derivation of physics from the forcing chain T0 to T8. No parent theorems appear in the supplied used_by block.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (4)