IndisputableMonolith.Cost.GaugeOrbitClassification
Classifies real multiplicative characters on the positive reals by their gauge orbits under the cost functional. Degenerate characters are pure sign gauges; nontrivial ones are signed powers. The bridge is that the map v ↦ v + v⁻¹ is strictly increasing on [1, ∞), so trace inequalities become value inequalities and ledger monotonicity lifts to character monotonicity. Cited by cost-unit axiom audits that pin the admissible cost shapes.
claimOn the positive reals, a real multiplicative character $\chi$ is either a pure sign gauge (degenerate case) or a signed power $\chi(x) = \mathrm{sign}(x)^s\,|x|^t$ (nontrivial case). The comparison uses the strictly increasing map $v\mapsto v+v^{-1}$ on $[1,\infty)$: inequalities of traces of principal values are inequalities of the values themselves, so cost monotonicity implies character monotonicity.
background
Recognition Science costs are built from the J-cost $J(x)=(x+x^{-1})/2-1$ (equivalently $\cosh(\log x)-1$), forced unique by the Recognition Composition Law. Gauge freedom acts by real characters on the positive multiplicative group; two displays of cost are equivalent when they differ by such a gauge orbit.
This module sits in the Cost layer and imports the construction of gauge orbits from real characters together with the monotone-multiplicative-power toolkit. The key elementary fact is that $v\mapsto v+v^{-1}$ is strictly increasing on $[1,\infty)$. Consequently an inequality between traces of principal values is already an inequality between the values. That converts the ledger's monotonicity constraint on costs into monotonicity of the underlying character.
Sibling results treat the zero and negative loci of cost, the display of cost at a character, existence of a natural exponent for monotone multiplicative maps, and the characterization that vanishing at two is equivalent to a flat (trace-two) character.
proof idea
The module is a classification package, not a single theorem. It first records that $v\mapsto v+v^{-1}$ is strictly increasing on $[1,\infty)$, so trace comparison yields value comparison (le_of_trace_le). Cost is then evaluated at zero, at negatives, and at positives, and the display map from character to cost is defined.
Degenerate characters are identified with pure sign gauges. Nontrivial characters are shown to be signed powers by combining the monotone-multiplicative-power lemmas with existence of a natural exponent. Vanishing-at-two criteria close the classification: the character vanishes at two if and only if its trace is two if and only if it is flat. The argument is algebraic and order-theoretic; no analytic continuation is required.
why it matters in Recognition Science
Admissible cost shapes in Recognition Science must be compatible with gauge orbits of real characters. This module supplies the exhaustive classification: only sign gauges and signed powers survive. Downstream it is imported by the cost-unit axiom audit script, which checks that the unit and normalization axioms of the cost layer are consistent with exactly these orbits.
In the broader forcing chain the J-cost is unique (T5) and $\phi$ is the self-similar fixed point (T6). Gauge classification ensures that no exotic multiplicative character can produce a second inequivalent cost that still obeys the ledger monotonicity and composition laws. Without it, the passage from abstract cost axioms to the concrete $\phi$-ladder mass formula would leave an open orbit of counter-models.
scope and limits
- Does not construct the J-cost or prove its uniqueness (T5 lives upstream).
- Does not treat complex or non-multiplicative characters.
- Does not derive the eight-tick octave or spatial dimension D=3.
- Does not fix the numerical value of the fine-structure constant band.
- Does not discharge cost-unit axioms; only supplies the orbit classification they audit.
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