Cost Gauge Orbit Classification Charges At Two Iff Not Sign Gauge

The charge test

In the Recognition Science framework, a ledger, a discrete record of recognition events, assigns a cost to every positive ratio between two quantities. One particular ratio, two, acts as a test point. The theorem charges_at_two_iff_not_signGauge states a clean dichotomy: the cost at ratio two is nonzero if and only if the ledger is not the sign gauge, the special cost function that reads only whether a ratio is positive or negative and ignores its magnitude.

The sign gauge is the simplest possible cost rule: it charges zero for every positive ratio and a fixed penalty for every negative one. The theorem proves that any ledger that differs from this rule, even at a single ratio, must show a nonzero cost at ratio two. Conversely, if the cost at two vanishes, the ledger is exactly the sign gauge on all ratios. The proof runs through the trace, a derived quantity equal to twice the cost plus two, and uses the fact that the map from a value to its trace is strictly increasing above one.

The result belongs to a classification of all possible ledgers under the framework's structural axioms. A companion theorem, conditional on the six exponentials conjecture, splits every ledger into two families: the sign gauge or a signed power cost, where the cost at a ratio is a power of that ratio. The charge test at two decides which family a ledger falls into, without needing to inspect the whole function.

The theorem does not say that a nonzero cost at two is positive; that requires a separate argument. It does not identify which power governs a non-sign ledger, only that such a ledger is not the sign gauge. And it does not assert that the six exponentials conjecture holds, only that the full classification depends on it.

/-- **Nondegeneracy is exactly the exclusion of the sign cost**, with no reference to
exponents and no appeal to the classification. -/
theorem charges_at_two_iff_not_signGauge (hS : SansAnchorHypotheses F) :
    (F two).toRat ≠ 0 ↔
      ¬ ∀ q : RatioOrbit, RatioOrbit.crossEq (F q) (signGaugeNativeCost q) := by
  constructor
  · intro hne hall
    have h := crossDisp (hall two)
    rw [signGaugeNativeCost_toRat, two_toRat, signGaugeCostDisplay,
      if_pos (by norm_num : (0 : ℚ) < 2)] at h
    exact hne h
  · intro hnot hzero
    exact hnot (degenerate_is_signGauge hS ((vanishes_at_two_iff_trace_two hS).mp hzero))

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

/-- **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⟩

What this page does not claim

The theorem does not prove that a nonzero cost at two is positive; that requires a separate argument. It does not identify which power governs a non-sign ledger, only that such a ledger is not the sign gauge. It does not assert that the six exponentials conjecture holds, only that the full classification depends on it.

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: