Cost Gauge Orbit From Real Character Signed Power Native Cost One Not Sign Gauge

The two gauge families

A recognition cost is a rule that assigns a number to each possible state of a system, a kind of bookkeeping entry that records how expensive it is for the system to recognize that state. In the Recognition Science framework, these costs are not arbitrary: they must satisfy a small set of structural conditions, and the framework's machine-checked library of formal theorems has proved that any cost meeting those conditions must take a specific form. But before that uniqueness result can be stated, the library must first rule out a family of plausible alternatives.

One such alternative is the signed power cost. For a natural number m, it sends a rational number x to x times the absolute value of x raised to the m-th power, written as x·|x|^m. For m = 1 this becomes x·|x|, which is x² for positive x and −x² for negative x. The other alternative is the sign gauge cost, a much cruder rule that ignores the size of x almost entirely: it returns 0 for positive x, −1 for x = 0, and −2 for negative x. Both rules satisfy the structural conditions that the framework requires of a recognition cost, as separate theorems in the library confirm.

The theorem named signedPowerNativeCost_one_not_signGauge establishes that these two rules are not the same. It proves the negation of the statement that for every rational number q, the signed power cost with m = 1 and the sign gauge cost produce the same output. The proof is concrete: it evaluates both rules at the number 2. The signed power cost sends 2 to 4, while the sign gauge cost sends 2 to 0, so the two outputs differ. This single counterexample is enough to refute the claim of universal equality.

The theorem does not claim that the signed power cost is the only cost that differs from the sign gauge cost, nor does it say anything about which cost is correct. It is a negative result, a boundary marker. It shows that the family of costs satisfying the structural conditions is wider than a naive guess might suggest, and it clears the way for the framework's later, positive results about the structure of recognition costs. The theorem is a precise, machine-checked statement about two specific functions, and it should be read as exactly that.

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

/-- The exponent-two member charges `J(4)` at the anchor. -/
theorem signedPowerNativeCost_one_two_toRat :
    (signedPowerNativeCost 1 two).toRat = jq 4 := by
  rw [signedPowerNativeCost_toRat, two_toRat]
  norm_num [signedPow]

/-- 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)

/-- **Every nonnegative integer exponent inhabits the anchor-free ledger.** The
sign-extended power character satisfies every structural field, including orientation
reversal, at every index and so at both parities of exponent. -/
theorem signedPowerNativeCost_sansAnchor (m : ℕ) :
    PRCStructuralNativeCostHypothesesSansAnchor (signedPowerNativeCost m) where
  base_sans_two := signedPowerNativeCost_base m
  sign_reversing := signedPowerNativeCost_signReversing m
  monotone := signedPowerNativeCost_monotone m
  zero_calibrated := signedPowerNativeCost_zero_calibrated m

/-- The zero-exponent sign member satisfies every field of the anchor-free
structural ledger. -/
theorem signGaugeNativeCost_sansAnchor :
    PRCStructuralNativeCostHypothesesSansAnchor signGaugeNativeCost where
  base_sans_two := signGaugeNativeCost_base_sans_two
  sign_reversing := signGaugeNativeCost_signReversing
  monotone := signGaugeNativeCost_monotone
  zero_calibrated := signGaugeNativeCost_zero_calibrated

What this page does not claim

The signed power cost is the only cost that differs from the sign gauge cost. The sign gauge cost is a valid recognition cost in the full sense, without the 'sans anchor' qualification. The theorem says anything about which cost is the correct one for a physical system.

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: