IndisputableMonolith.Cost.GaugeOrbitClassification
Classification of real characters on the positive multiplicative group by their gauge orbits under the cost functional. Costs are recovered from the trace map v ↦ v + v⁻¹, which is strictly increasing on [1, ∞), so monotonicity of ledger costs becomes monotonicity of the character. Anyone working the RS cost-unit or J-uniqueness chain cites this module. The argument assembles orbit representatives into signed powers and degenerate sign gauges.
claimReal multiplicative characters $\chi$ on $\mathbb{R}_{>0}$ are classified up to gauge by the cost $J$: either $\chi$ is a signed power $x \mapsto \pm x^{k}$ for some $k \in \mathbb{N}$, or it is a degenerate pure sign gauge. The map $v \mapsto v + v^{-1}$ is strictly increasing on $[1,\infty)$, so trace inequalities on principal values are inequalities on the values themselves, converting ledger cost monotonicity into character monotonicity.
background
Recognition Science builds the unique cost $J(x) = (x + x^{-1})/2 - 1$ from the Recognition Composition Law and the forcing chain (T5 J-uniqueness). On the positive reals the same algebraic skeleton appears as a real character $\chi$ whose associated cost is read off the orbit under the involution $v \mapsto v^{-1}$.
The module sits in the Cost domain. It imports the construction of gauge orbits from a real character and the monotone-multiplicative-power lemmas that control $x \mapsto x^{k}$ on $\mathbb{R}_{>0}$. The key analytic fact is that the trace $v \mapsto v + v^{-1}$ is strictly increasing on $[1,\infty)$: an inequality between traces of principal values is therefore an inequality between the values. That turns the ledger's monotonicity condition on costs into monotonicity of the character itself.
Sibling material treats evaluation at zero and negative arguments, the vanishing criterion at two (flat versus nontrivial), and the existence of a natural exponent once monotonicity is secured.
proof idea
The module is a classification package, not a single theorem. It first records that the trace map is strictly monotone on principal values, so cost inequalities descend to character inequalities. Degenerate characters (vanishing cost off the units) are identified with pure sign gauges. Nontrivial characters that remain monotone and multiplicative are shown to be signed natural powers by extracting an exponent from the monotone-multiplicative-power import and checking the cost display formula at positive, zero, and negative points. Vanishing of the cost at two is equivalent to the character being flat (trace identically two).
why it matters in Recognition Science
This module supplies the orbit classification that the cost-unit axiom audit script imports when it checks that the RS cost is the unique gauge-invariant functional compatible with the ledger. Downstream, that uniqueness feeds the T5 step of the forcing chain (J-uniqueness) and the identification of $\phi$ as the self-similar fixed point. Without a clean split between signed-power characters and degenerate sign gauges, the passage from abstract RCL solutions to the concrete $J(x) = \cosh(\log x) - 1$ would remain formal. The module therefore closes a necessary bookkeeping gap between character theory and the physical cost used for the mass ladder and the eight-tick octave.
scope and limits
- Does not prove J-uniqueness from scratch; assumes the Cost-domain imports.
- Does not treat complex or non-multiplicative characters.
- Does not derive the numerical value of $\phi$ or the eight-tick period.
- Does not address dimensional forcing (T8) or the fine-structure band.
- Does not supply a computational decision procedure for arbitrary Lean terms.
used by (1)
depends on (2)
declarations in this module (17)
-
theorem
le_of_trace_le -
theorem
cost_display -
theorem
cost_at_zero -
theorem
cost_at_neg -
theorem
degenerate_is_signGauge -
theorem
natChar_monotoneMultiplicative -
theorem
exists_nat_exponent -
theorem
char_at_pos -
theorem
cost_at_pos -
theorem
nontrivial_is_signedPower -
theorem
vanishes_at_two_iff_trace_two -
theorem
vanishes_at_two_iff_flat -
theorem
charges_positively_at_two -
theorem
strict_somewhere_iff_charges_at_two -
theorem
charges_at_two_iff_not_signGauge -
theorem
signGauge_sees_orientation_only -
theorem
GaugeOrbitIsSignedPowerFamily_of_sixExponentials