pith. sign in
module module moderate

IndisputableMonolith.Bridge.GaugeVsParams

show as:
view Lean formalization →

Bridge.GaugeVsParams supplies definitions for rescaling potentials by a factor alpha and offset b, together with gauge-invariant forms of alpha inverse, log phi, curvature, and gap resolution. Researchers checking parameter independence under gauge changes in Recognition Science would reference these objects. The module consists entirely of definitions with no theorems or proofs.

claimThe rescaling map acts on potential $p$ by $pmapsto alphap + b$. Gauge invariance holds for $alpha^{-1}$, $logphi$, curvature, the gap-3 resolution, and the statement that $alpha$ is not tunable.

background

The module imports Constants, whose fundamental time quantum satisfies $tau_0=1$ tick, and Constants.Alpha. It works inside the Recognition Science setting that uses the J-cost function, the Recognition Composition Law, and the phi-ladder for mass assignments. The supplied module doc-comment states the central operation: rescale potential by factor alpha and offset b, written $p to alphap + b$.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the gauge-invariant objects that appear in sibling declarations such as alpha_not_tunable and gap3_resolved. It therefore supports the broader claim that physical constants remain fixed under gauge transformations, consistent with the J-uniqueness step and the alpha band inside (137.030,137.039).

scope and limits

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (11)