Foundation Arithmetic From Logic Pow Lt Pow Iff Of One Lt

The comparison rule

The statement pow_lt_pow_iff_of_one_lt is a theorem about ordered multiplication: if a base number is greater than 1, then raising it to a smaller power gives a smaller result, and conversely. In symbols, for a base b > 1, the inequality b^m < b^n holds exactly when m < n. This is the familiar monotonicity of exponentiation, the reason 2³ < 2⁵ follows from 3 < 5 without computing either power. It is a basic fact of ordered arithmetic, used constantly in number theory and analysis.

The theorem appears in the Recognition Science framework's ledger, a discrete record of events, as part of a construction that derives arithmetic from logic. The framework begins with a comparison operator satisfying five plain conditions, and from those conditions proves that a cost function J(x) = (x + 1/x)/2 − 1 is forced. From that cost function, the framework derives a generator γ ≠ 1 with strictly positive cost, and the orbit {1, γ, γ², γ³, ...} under repeated multiplication. That orbit, together with the identity element 1, has exactly two constructors: "be at the identity" and "take one more step." This two-constructor structure is the natural-number structure, formalized as an inductive type called LogicNat.

Within this construction, the theorem pow_lt_pow_iff_of_one_lt establishes that the ordering on these constructed numbers agrees with the ordering on their exponents. The framework defines comparison on LogicNat by existence of a difference: n ≤ m means there exists k such that n + k = m. The theorem then shows that this order behaves correctly under exponentiation, so that a < b in the constructed numbers is equivalent to γ^a < γ^b in the real numbers. This is a coherence result: the abstract arithmetic built from logic matches the familiar arithmetic of real numbers.

What the theorem does not claim is broader. It does not assert that the framework's construction is the only way to build arithmetic, nor that it is simpler than the standard Peano axioms. It does not claim that the particular generator γ is the golden ratio; that identification is a separate result. The theorem is a local fact about ordered exponentiation, proved within a specific formal system. It shows that one piece of the framework's arithmetic is internally consistent, not that the framework's overall derivation of physics from logic is complete or correct.

theorem lt_iff_succ_le {n m : LogicNat} : n < m ↔ succ n ≤ m := by
  constructor
  · rintro ⟨k, hk⟩
    refine ⟨k, ?_⟩
    show succ n + k = m
    rw [succ_add]
    show succ (n + k) = m
    rw [← add_succ]
    -- need n + succ k = m, but we have n + succ k = m via hk; succ_add transforms
    -- Wait: hk : n + succ k = m, and succ (n + k) = n + succ k by add_succ. So succ (n + k) = m.
    exact hk
  · rintro ⟨k, hk⟩
    refine ⟨k, ?_⟩
    show n + succ k = m
    rw [add_succ]
    show succ (n + k) = m
    rw [← succ_add]
    exact hk

/-- **Chain closure**: a comparison operator satisfying the Law of Logic
yields an explicit non-trivial generator. The construction extracts the
witness from `non_trivial` and uses `identity` to rule out `value = 1`.

This is the structural completion of the chain. Before this lemma,
`Generator` was a free structure; now it is *literally* derived from
`SatisfiesLawsOfLogic`. -/
noncomputable def generatorOfLawsOfLogic
    {C : ComparisonOperator} (hLaws : SatisfiesLawsOfLogic C) : Generator :=
  let x := Classical.choose hLaws.non_trivial
  have hx : 0 < x ∧ derivedCost C x ≠ 0 := Classical.choose_spec hLaws.non_trivial
  { value      := x
    pos        := hx.1
    nontrivial := by
      intro hx_eq_one
      apply hx.2
      show derivedCost C x = 0
      rw [hx_eq_one]
      show C 1 1 = 0
      exact hLaws.identity 1 one_pos }

/-- The natural numbers as forced by the Law of Logic.

`identity` represents the zero-cost element (the multiplicative
identity in the orbit). `step` represents one more iteration of the
generator. The two-constructor structure mirrors the orbit
{1, γ, γ², γ³, ...} as the smallest subset of ℝ₊ closed under
multiplication by γ and containing 1. -/
inductive LogicNat : Type
  | identity : LogicNat
  | step     : LogicNat → LogicNat
  deriving DecidableEq, Repr

What this page does not claim

The theorem does not claim that the framework's construction of arithmetic is the only possible one. The theorem does not identify the generator γ with the golden ratio; that is a separate result. The theorem does not assert that the framework's overall derivation of physics from logic is complete.

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/Foundation/ArithmeticFromLogic.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: