Cost Gauge Orbit From Real Character Sign Gauge Native Cost Not Odd Power Genera

A cost that refuses the odd-power family

A cost function in Recognition Science assigns a number to each ratio, and the framework's ledger, a discrete record of recognition events, demands that this assignment obey strict structural rules. One candidate is the sign gauge cost: it sends every positive ratio to 0, the ratio 0 to -1, and every negative ratio to -2. This is a deliberately coarse, sign-sensitive rule, and it satisfies the framework's basic structural hypotheses, including sign reversal and monotonicity.

The framework also studies a family of smoother candidates, the odd-power generated costs, which send a ratio x to a value proportional to x raised to an odd exponent. These costs are natural because they preserve sign and vanish at zero, and they form a plausible classification family for all structurally valid costs. The question is whether the sign gauge cost, despite its coarse jumps, might secretly be one of these smooth odd-power rules in disguise.

The machine-checked theorem signGaugeNativeCost_not_oddPowerGeneratedNativeCost answers no. For every odd exponent k, there exists at least one ratio where the sign gauge cost and the odd-power cost disagree. The proof is constructive: it exhibits the specific ratio 2, where the sign gauge cost returns 0 while any odd-power cost returns a nonzero value. This single counterexample, checked by the framework's library of formal theorems, rules out the entire infinite family at once.

What this does not claim is broader. It does not say the sign gauge cost is the only valid cost, nor that the odd-power family is entirely invalid. Other costs, such as the signed-power costs with even exponents, do coincide with odd-power rules on all ratios, as a separate theorem shows. The result is a precise negative: one specific coarse cost escapes one specific smooth family, and the classification of all structural costs therefore needs a wider net than odd powers alone.

/-- Display of the zero-exponent sign cost. -/
def signGaugeCostDisplay (x : ℚ) : ℚ :=
  if 0 < x then 0 else if x = 0 then -1 else -2

/-- The sign member cannot equal any positive odd-power cost. -/
theorem signGaugeNativeCost_not_oddPowerGeneratedNativeCost (k : ℕ) :
    ¬ ∀ q : RatioOrbit,
      RatioOrbit.crossEq (signGaugeNativeCost q)
        (oddPowerGeneratedNativeCost k q) := by
  intro h
  have htwo := crossDisp (h two)
  rw [signGaugeNativeCost_toRat, oddPowerGeneratedNativeCost_toRat,
    two_toRat] at htwo
  have hexp : 2 * k + 1 ≠ 0 := by omega
  have hp : (1 : ℚ) < 2 ^ (2 * k + 1) :=
    one_lt_pow₀ (by norm_num) hexp
  have hzero : jq ((2 : ℚ) ^ (2 * k + 1)) = 0 := by
    norm_num [signGaugeCostDisplay] at htwo
    exact htwo.symm
  have hone := jq_eq_zero (ne_of_gt (lt_trans zero_lt_one hp)) hzero
  exact (ne_of_gt hp) hone

/-- The extracted sign character is not any positive odd-integer power,
already at the anchor. -/
theorem signGaugeNativeCost_character_not_oddPower (k : ℕ) :
    IndisputableMonolith.Cost.RealCharacterFactorization.realCharacterCandidate
        signGaugeNativeCost
        (IndisputableMonolith.Cost.RealCharacterFactorization.natOrbit 2) ≠
      (2 : ℝ) ^ (2 * k + 1) := by
  rw [signGaugeNativeCost_realCharacterCandidate,
    IndisputableMonolith.Cost.RealCharacterFactorization.natOrbit_toRat]
  have hsign :
      IndisputableMonolith.Cost.RealCharacterFactorization.rationalSignCharacter
        (((2 : ℕ) : ℚ)) = 1 := by
    norm_num
      [IndisputableMonolith.Cost.RealCharacterFactorization.rationalSignCharacter]
  rw [hsign]
  exact ne_of_lt (one_lt_pow₀ (by norm_num) (by omega))

/-- The sign member takes the degenerate trace value two at the anchor. -/
theorem signGaugeNativeCost_rationalTrace_two :
    IndisputableMonolith.Cost.RealCharacterFactorization.rationalTrace
      signGaugeNativeCost 2 = 2 := by
  rw [IndisputableMonolith.Cost.RealCharacterFactorization.rationalTrace,
    IndisputableMonolith.Cost.RealCharacterFactorization.traceDisplay,
    nativeCostDoubledTrace, doubledTraceValue]
  simp only [RatioOrbit.mul_toRat, RatioOrbit.add_toRat, two_toRat,
    RatioOrbit.one_toRat, signGaugeNativeCost_toRat, ratioOrbitOfRat_toRat]
  norm_num [signGaugeCostDisplay]

/-- The even indices recover the known odd-power family, so the new family contains it. -/
theorem signedPowerNativeCost_even_eq_oddPower (k : ℕ) (q : RatioOrbit) :
    (signedPowerNativeCost (2 * k) q).toRat =
      (oddPowerGeneratedNativeCost k q).toRat := by
  rw [signedPowerNativeCost_toRat, oddPowerGeneratedNativeCost_toRat, signedPow_even]

What this page does not claim

The sign gauge cost is the only valid cost in the framework. The odd-power family is entirely invalid or useless for classification. The theorem shows anything about costs that do not satisfy the structural hypotheses. The sign gauge cost is derived from the framework's fundamental cost J rather than merely satisfying the same structural axioms.

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: