Encyclopedia Cost Cost Gauge Orbit Classification

ARTICLE 4 claims 4 theorems

Cost Gauge Orbit Classification

A machine-checked proof shows that every well-behaved cost function in the framework is either a simple sign check or a signed power, with no other options.

Verify this page

Classifying the ledger's costs

Cost gauge orbit classification is a result inside the Recognition Science framework. The framework models reality as maintaining a ledger, a discrete record of recognition events, where each event has a cost. The classification theorem says that the cost function, which assigns a number to each possible ratio of recognized values, can only take one of two forms. Either it is a sign gauge, which only records whether the ratio is positive or negative, or it is a signed power, which raises the ratio to a fixed exponent and then applies a sign. The theorem proves that no other cost function is possible under the framework's axioms.

The result is proved in a machine-checked library of formal theorems. The proof splits into two cases. The first case is when the cost at the ratio 2 is zero. The theorem degenerate_is_signGauge shows that in this case, the cost function is exactly the sign gauge. The second case is when the cost at 2 is not zero. Here, the proof uses a condition called the six exponentials trace input, a number-theoretic assumption. Under this assumption, the theorem GaugeOrbitIsSignedPowerFamily_of_sixExponentials shows that the cost must be a signed power. The exponent is a natural number, so the cost is one of a countable family of functions, not a continuous range.

The classification is a structural result, not a numerical one. It does not say which exponent appears; that is a separate question. The theorem charges_positively_at_two shows that when the cost at 2 is not zero, it is positive, so the sign gauge is the only way to get a zero cost at 2. The theorem signGauge_sees_orientation_only makes the sign gauge explicit: it assigns 0 to positive ratios and -2 to negative ones. The signed power family is a natural generalization, and the classification shows the framework's axioms force the cost to be one of these two simple types.

In Recognition Science, this classification is a step toward understanding what the ledger can and cannot do. The framework's axioms are meant to be minimal, and this theorem shows they are also restrictive. The result is a target for further work: the six exponentials assumption is not proved within the framework, so the full classification without it remains open. The theorem is a conditional statement, and the condition is a genuine mathematical hypothesis.

THEOREM GaugeOrbitIsSignedPowerFamily_of_sixExponentials · IndisputableMonolith/Cost/GaugeOrbitClassification.lean
GaugeOrbitIsSignedPowerFamily_of_sixExponentials · IndisputableMonolith/Cost/GaugeOrbitClassification.lean:365 
/-- **The anchor-free gauge classification, on one named import.** Every inhabitant of the
anchor-free structural cost ledger is the sign cost or the sign-extended power cost of a
nonnegative integer exponent. The only hypothesis is the six exponentials input; the Erdős
step is now the theorem `Cost.MonotonePower.exists_exponent`.

Two things this does NOT say. It does not say the exponent is odd: both parities are
inhabited, by construction in `GaugeOrbitFromRealCharacter`. And it does not select `J`:
selection is leastness, which lives in `Cost.UnitFromMinimality`. -/
theorem GaugeOrbitIsSignedPowerFamily_of_sixExponentials
    (hsix : SixExponentialsTraceInput) : GaugeOrbitIsSignedPowerFamily := by
  intro G hG
  have hS := realCharacterFactorizationHypotheses_of_structural hG
  by_cases htwo : rationalTrace G 2 = 2
  · exact Or.inl (degenerate_is_signGauge hS htwo)
  · obtain ⟨k, hk1, hk⟩ := exists_nat_exponent hsix hS htwo
    exact Or.inr ⟨k - 1, nontrivial_is_signedPower hS htwo hk1 hk⟩
THEOREM degenerate_is_signGauge · IndisputableMonolith/Cost/GaugeOrbitClassification.lean
degenerate_is_signGauge · IndisputableMonolith/Cost/GaugeOrbitClassification.lean:106 
/-- **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
THEOREM charges_positively_at_two · IndisputableMonolith/Cost/GaugeOrbitClassification.lean
charges_positively_at_two · IndisputableMonolith/Cost/GaugeOrbitClassification.lean:301 
/-- A nondegenerate inhabitant charges a strictly positive amount at orbit two, so the
condition may be read as an inequality rather than a disequality. -/
theorem charges_positively_at_two (hS : SansAnchorHypotheses F)
    (hne : (F two).toRat ≠ 0) : 0 < (F two).toRat := by
  have hge : (2 : ℝ) ≤ rationalTrace F 2 := by
    have h := IndisputableMonolith.Cost.RealCharacterFactorization.rationalTrace_nat_ge_two hS
      (n := 2) (by norm_num)
    simpa using h
  have hgt : (2 : ℝ) < rationalTrace F 2 :=
    lt_of_le_of_ne hge (Ne.symm fun h => hne ((vanishes_at_two_iff_trace_two hS).mpr h))
  have hd := cost_display hS two
  rw [two_toRat] at hd
  have hpos : (0 : ℝ) < ((F two).toRat : ℝ) := by rw [hd]; linarith
  exact_mod_cast hpos
THEOREM signGauge_sees_orientation_only · IndisputableMonolith/Cost/GaugeOrbitClassification.lean
signGauge_sees_orientation_only · IndisputableMonolith/Cost/GaugeOrbitClassification.lean:351 
/-- What the degenerate member actually is. It charges the full reversal penalty at every
negative ratio and nothing at every positive one: a cost that records orientation and never
magnitude. So the nondegeneracy hypothesis is not "assume cost is not free"; it is "assume
cost sees how far apart the two sides are". -/
theorem signGauge_sees_orientation_only (q : RatioOrbit) :
    (0 < q.toRat → (signGaugeNativeCost q).toRat = 0) ∧
      (q.toRat < 0 → (signGaugeNativeCost q).toRat = -2) := by
  refine ⟨fun hq => ?_, fun hq => ?_⟩
  · rw [signGaugeNativeCost_toRat, signGaugeCostDisplay, if_pos hq]
  · rw [signGaugeNativeCost_toRat, signGaugeCostDisplay, if_neg (not_lt.mpr hq.le),
      if_neg (ne_of_lt hq)]

What this page does not claim

The classification does not determine which signed power exponent appears. The six exponentials trace input is not proved within the framework; it is an assumption. The result does not apply to cost functions that violate the framework's 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/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:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND