pith. sign in
module module moderate

IndisputableMonolith.Masses.Exponent.Gauge

show as:
view Lean formalization →

The Gauge module in Masses.Exponent establishes the gauge equivalence relation for handling equivalent mass exponent representations in Recognition Science. It defines GaugeEq along with its reflexive, symmetric, and transitive properties via the listed siblings. This supports consistent mass calculations across different phi-ladder rungs without altering physical outcomes. The structure is purely definitional with no complex proofs.

claimThe module defines an equivalence relation $GaugeEq$ on real numbers representing mass exponents, satisfying reflexivity $GaugeEq(x,x)$, symmetry $GaugeEq(x,y) implies GaugeEq(y,x)$, and transitivity.

background

This module operates within the Masses domain of Recognition Science, where masses are assigned via yardstick * phi^(rung - 8 + gap(Z)) on the phi-ladder. Gauge equivalence allows different exponent choices that yield equivalent physical predictions under the Recognition Composition Law. The module imports Mathlib for basic relation properties and introduces GaugeEq as the core definition.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module provides foundational equivalence for mass exponent handling, feeding into parent theorems on mass formulas and phi-ladder assignments in the broader Masses.Exponent namespace. It supports the T6 phi fixed point and mass calculations in the framework.

scope and limits

declarations in this module (4)