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

IndisputableMonolith.Bridge.GaugeVsParams

show as:
view Lean formalization →

Bridge.GaugeVsParams supplies the rescaling map that sends a potential p to alpha p plus offset b, together with the GaugeInvariant predicate applied to alpha inverse, log phi, and curvature. Researchers working on dimensionless constants in Recognition Science cite these constructions when demonstrating that the observed alpha band survives gauge transformations. The module is assembled from direct definitions of rescale_potential, rescale_cost, and the listed invariance statements, each obtained by substitution into the Recognition rules.

claimThe rescaling operation is $pmapsto alphap+b$. Gauge invariance is asserted by the predicate GaugeInvariant for the quantities $alpha^{-1}$, $logphi$, curvature, and the gap-3 term, all of which remain unchanged under the map.

background

The module imports the RS time quantum tau_0=1 tick from Constants and the alpha definitions from Constants.Alpha. It introduces the linear rescaling of potentials together with the GaugeInvariant predicate that encodes invariance under this transformation. The setting is the bridge between dimensional constants on the phi-ladder and the dimensionless observables required for the alpha band (137.030,137.039).

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

The module feeds the sibling results alpha_not_tunable and gap3_resolved by supplying the gauge-invariant formulations of alpha inverse and curvature. It realizes the step from the phi-ladder constants to dimensionless observables that are independent of gauge choice, consistent with T5 J-uniqueness and the eight-tick octave.

scope and limits

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (11)