Encyclopedia Cost Cost Gauge Orbit Classification Gauge Orbit Is Signed Power Family Of Six Expone

ARTICLE 4 claims 4 theorems

Cost Gauge Orbit Classification Gauge Orbit Is Signed Power Family Of Six Expone

A machine-checked proof shows that under one extra assumption, every cost function in the framework belongs to one of two simple families.

Verify this page

The classification theorem

The declaration GaugeOrbitIsSignedPowerFamily_of_sixExponentials is a theorem in the framework's machine-checked library of formal theorems. It classifies all cost functions that satisfy the framework's structural hypotheses. A cost function, in this framework, assigns a real number to each ratio of two positive magnitudes; it measures the price of recognizing one magnitude in terms of another. The theorem says that, under a certain additional input called the six exponentials trace input, every such cost function is either a sign gauge or a signed power family member.

The two families are simple. The sign gauge cost function depends only on the sign of the ratio: it returns 0 for positive ratios and -2 for negative ratios. The signed power family is indexed by a natural number k, and for a positive ratio x it returns the value j(x^k), where j is the framework's fundamental cost function j(y) = (y + 1/y)/2 - 1. For negative ratios, the value is determined by the sign-reversing symmetry. The theorem does not pick out which family or which exponent occurs; it only proves that every eligible cost function falls into one of the two.

The proof splits into two cases. If the cost at ratio 2 is zero, the function is a sign gauge. If the cost at ratio 2 is nonzero, the function is a signed power. The key intermediate step, exists_nat_exponent, shows that on positive integers the character value is a pure power n^k. This step uses the six exponentials trace input, a number-theoretic assumption about the traces of the cost function. The final theorem then extends this integer behavior to all rational ratios.

What the theorem does not claim is as important as what it proves. It does not assert that the six exponentials trace input holds; that remains an assumption. It does not determine which exponent k occurs, nor does it say that the sign gauge and signed power families exhaust all possibilities without the extra input. The theorem is a conditional classification: if the input holds, the classification is complete.

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 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 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)]
THEOREM nontrivial_is_signedPower · IndisputableMonolith/Cost/GaugeOrbitClassification.lean
nontrivial_is_signedPower · IndisputableMonolith/Cost/GaugeOrbitClassification.lean:224 
/-- **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

What this page does not claim

The theorem does not prove that the six exponentials trace input holds. The theorem does not determine which exponent k occurs for a given cost function. The theorem does not classify cost functions without the six exponentials trace input.

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