Cost Gauge Orbit Classification Vanishes At Two Iff Trace Two

The vanishing test

In the Recognition Science framework, a ledger is a discrete record of recognition events, and each event carries a cost, a real number that measures how expensive that recognition is. The framework's central question is which cost functions are possible at all. The theorem vanishes_at_two_iff_trace_two answers a sharp version of that question for one specific input: the ratio 2.

The theorem states a biconditional. On one side, the cost function F assigns the value 0 to the ratio 2: F(2) = 0. On the other side, a quantity called the rational trace of F at 2 equals 2. The trace here is not the matrix trace of linear algebra; it is a framework-internal function that packages the cost values into a single scalar, defined so that the cost display formula holds: F(q) = (trace(q) / 2) - 1. The theorem proves that these two conditions are equivalent, for any cost function F satisfying the framework's structural hypotheses.

The content of the equivalence is a classification. If the trace at 2 is exactly 2, then the cost function is what the framework calls a sign gauge: it sees only the sign of its input, returning 0 for positive ratios and -2 for negative ones. Such a function carries no information beyond orientation. If the trace at 2 is not 2, then the cost function is nontrivial: it charges a nonzero cost at 2, and the framework proves it must belong to a signed power family, with the cost at a positive ratio q given by j(q^k) for some integer k ≥ 1. The theorem vanishes_at_two_iff_trace_two is the pivot that splits these two cases.

This matters because the split is exhaustive and exclusive. The framework proves that a cost function either vanishes at 2, in which case it is the trivial sign gauge, or it does not, in which case it is a genuine power law. The trace at 2 is the single diagnostic that decides which. The theorem is proved in the machine-checked library of formal theorems, with no unverified assumptions beyond the framework's own structural hypotheses.

The theorem does not claim that the sign gauge is the only possible cost function, nor that the signed power family is complete without the six-exponentials hypothesis. It does not assert that any particular physical system realizes either branch. It establishes a logical equivalence within the framework, and the framework's library separately proves the classification consequences that follow from each branch.

/-- Cost vanishes at orbit two exactly when the trace there takes the degenerate value. -/
theorem vanishes_at_two_iff_trace_two (hS : SansAnchorHypotheses F) :
    (F two).toRat = 0 ↔ rationalTrace F 2 = 2 := by
  have hd := cost_display hS two
  rw [two_toRat] at hd
  constructor
  · intro h
    rw [h] at hd
    push_cast at hd
    linarith
  · intro h
    rw [h] at hd
    have hz : ((F two).toRat : ℝ) = 0 := by rw [hd]; norm_num
    exact_mod_cast hz

/-- **The degenerate anchor is exactly the sign cost.** If the trace at two is two then the
trace is two at every positive display, the cost vanishes there, and orientation reversal
fills in the rest. -/
theorem degenerate_is_signGauge (hS : SansAnchorHypotheses F)
    (htwo : rationalTrace F 2 = 2) (q : RatioOrbit) :
    RatioOrbit.crossEq (F q) (signGaugeNativeCost q) := by
  refine dispCross ?_
  rw [signGaugeNativeCost_toRat]
  rcases lt_trichotomy q.toRat 0 with hneg | hzero | hpos
  · have hpospart : (0 : ℚ) < -q.toRat := by linarith
    have hp : (F (ratioOrbitOfRat (-q.toRat))).toRat = 0 := by
      have h := cost_display hS (ratioOrbitOfRat (-q.toRat))
      rw [ratioOrbitOfRat_toRat,
        rationalTrace_pos_eq_two_of_two_eq_two hS htwo hpospart] at h
      norm_num at h
      exact_mod_cast h
    rw [cost_at_neg hS q, hp, signGaugeCostDisplay, if_neg (not_lt.mpr hneg.le),
      if_neg (ne_of_lt hneg)]
    norm_num
  · rw [cost_at_zero hS hzero, signGaugeCostDisplay,
      if_neg (by rw [hzero]; exact lt_irrefl 0), if_pos hzero]
  · have h := cost_display hS q
    rw [rationalTrace_pos_eq_two_of_two_eq_two hS htwo hpos] at h
    norm_num at h
    rw [signGaugeCostDisplay, if_pos hpos]
    exact_mod_cast h

/-- **The nondegenerate branch is a sign-extended power cost.** -/
theorem nontrivial_is_signedPower (hS : SansAnchorHypotheses F)
    (hnt : rationalTrace F 2 ≠ 2) {k : ℕ} (hk1 : 1 ≤ k)
    (hk : ∀ n : ℕ, 1 ≤ n → nontrivialCharacterValue F (n : ℚ) = ((n : ℝ)) ^ k) :
    ∀ q : RatioOrbit, RatioOrbit.crossEq (F q) (signedPowerNativeCost (k - 1) q) := by
  obtain ⟨m, rfl⟩ : ∃ m : ℕ, k = m + 1 := ⟨k - 1, by omega⟩
  intro q
  refine dispCross ?_
  rw [signedPowerNativeCost_toRat]
  simp only [Nat.add_sub_cancel]
  rcases lt_trichotomy q.toRat 0 with hneg | hzero | hpos
  · have hpospart : (0 : ℚ) < -q.toRat := by linarith
    have hp : (F (ratioOrbitOfRat (-q.toRat))).toRat = jq ((-q.toRat) ^ (m + 1)) := by
      have h := cost_at_pos hS hnt hk (q := ratioOrbitOfRat (-q.toRat))
        (by rw [ratioOrbitOfRat_toRat]; exact hpospart)
      rwa [ratioOrbitOfRat_toRat] at h
    rw [cost_at_neg hS q, hp, signedPow, abs_of_neg hneg,
      show q.toRat * (-q.toRat) ^ m = -((-q.toRat) ^ (m + 1)) by ring, jq_neg]
  · rw [cost_at_zero hS hzero, hzero, signedPow_zero_arg]
    norm_num [jq]
  · rw [cost_at_pos hS hnt hk hpos, signedPow, abs_of_pos hpos]
    congr 1
    ring

/-- The cost display is the trace display, halved and shifted. -/
private theorem cost_display (hS : SansAnchorHypotheses F) (q : RatioOrbit) :
    ((F q).toRat : ℝ) = rationalTrace F q.toRat / 2 - 1 := by
  rw [rationalTrace_eq_traceDisplay hS q]
  simp only [traceDisplay, nativeCostDoubledTrace, doubledTraceValue,
    RatioOrbit.mul_toRat, RatioOrbit.add_toRat, two_toRat, RatioOrbit.one_toRat]
  push_cast
  ring

What this page does not claim

The theorem does not claim that the sign gauge is the only possible cost function. It does not claim that the signed power family is complete without the six-exponentials hypothesis. It does not claim that any particular physical system realizes either branch.

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/GaugeOrbitClassification.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: