Cost Gauge Orbit From Real Character

The gauge orbit theorem

A cost function, in the Recognition Science framework, assigns a number to each recognition event, and the framework's central theorem forces the specific form J(x) = (x + 1/x)/2 - 1. But before that theorem applies, one must ask: what are the possible cost functions that satisfy the framework's structural conditions at all? The module GaugeOrbitFromRealCharacter answers this question completely.

The answer is a dichotomy. Every structural cost function is either a sign gauge, which sends positive numbers to 0, zero to -1, and negative numbers to -2, or it is a signed power, which sends x to x times |x|^m for some natural number m. The module proves this classification theorem in the machine-checked library of formal theorems, with no gaps in the reasoning.

The proof proceeds by showing that every structural cost function has a real character factorization, a representation as a product of a sign character and a power. The sign gauge corresponds to the case where the exponent is zero, and the signed powers cover all other cases. The module also proves that these two families are genuinely distinct: the sign gauge is not a signed power, and no signed power equals an odd power generated cost, which is a separate family that appears in related work.

This classification is not just a curiosity. It establishes the precise boundary of what the framework's structural conditions can produce, before the central uniqueness theorem narrows the field to a single cost function. It shows that the framework's axioms are not vacuous: they permit a small, well-understood family of costs, and the uniqueness theorem then selects one member of that family. The module thus provides a complete structural census, a necessary step in understanding why the framework's forced cost function is the only one that survives all five conditions.

/-- **PROVED**, on one named import, in `Cost.GaugeOrbitClassification`
(`GaugeOrbitIsSignedPowerFamily_of_sixExponentials`). Corrected a third time before it
closed: every anchor-free structural inhabitant is the sign cost (exponent zero) or a
sign-extended power cost (exponent `m+1`), so the classification allows every nonnegative
integer exponent and no more. The odd powers are the even indices by
`signedPowerNativeCost_even_eq_oddPower`. The single hypothesis of the proof is
`Cost.TraceRationalExponent.SixExponentialsTraceInput`. -/
def GaugeOrbitIsSignedPowerFamily : Prop :=
  ∀ F : RatioOrbit → RatioOrbit, PRCStructuralNativeCostHypothesesSansAnchor F →
    (∀ q : RatioOrbit, RatioOrbit.crossEq (F q) (signGaugeNativeCost q)) ∨
      ∃ m : ℕ, ∀ q : RatioOrbit,
        RatioOrbit.crossEq (F q) (signedPowerNativeCost m q)

/-- The cost generated by the sign character. -/
def signGaugeNativeCost (q : RatioOrbit) : RatioOrbit :=
  if 0 < q.toRat then RatioOrbit.zero
  else if q.toRat = 0 then ratioOrbitOfRat (-1)
  else ratioOrbitOfRat (-2)

/-- The cost generated by the sign-extended power character `χ(x) = sgn(x)·|x|^(m+1)`. -/
def signedPowerNativeCost (m : ℕ) (q : RatioOrbit) : RatioOrbit :=
  if q.toRat = 1 then RatioOrbit.zero
  else onRatioOrbit (ratioOrbitOfRat (signedPow m q.toRat))

theorem signedPowerNativeCost_one_not_signGauge :
    ¬ ∀ q : RatioOrbit,
      RatioOrbit.crossEq (signedPowerNativeCost 1 q) (signGaugeNativeCost q) := by
  intro h
  have htwo := crossDisp (h two)
  rw [signedPowerNativeCost_one_two_toRat, signGaugeNativeCost_toRat,
    two_toRat] at htwo
  norm_num [signGaugeCostDisplay, jq] at htwo

What this page does not claim

This module does not prove the central uniqueness theorem J(x) = (x + 1/x)/2 - 1. This module does not claim that the sign gauge and signed power families are the only costs satisfying the full five conditions, only the structural ones.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Cost/GaugeOrbitFromRealCharacter.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: