Foundation Universal Forcing Strict Positive Ratio Positive Ratio Arith Equiv Lo

The arithmetic equivalence

In mathematics, when two different constructions produce the same arithmetic, they are said to be equivalent. The declaration positiveRatio_arith_equiv_logicNat is a machine-checked statement that one such equivalence holds. It takes a comparison operator C that satisfies the five laws of logic, builds a strict positive-ratio realization from it, and then shows that the arithmetic forced by that realization is isomorphic to the standard arithmetic object called LogicNat. In plain terms, the arithmetic that comes out of the strict positive-ratio structure is the same arithmetic that comes out of the existing lightweight wrapper; the two are interchangeable for any further formal work.

The proof rests on two earlier constructions. The first is strictPositiveRatioRealization, which takes a comparison operator satisfying the laws and produces a strict logic realization. The second is a bridge called orbitEquivLogicNat, which connects the strict realization's arithmetic to LogicNat. The declaration then composes these two steps into a single equivalence. A companion declaration, positiveRatio_strict_equiv_existing, shows the same arithmetic is also equivalent to the arithmetic from the existing positive-ratio lightweight wrapper, so all three structures agree on their forced arithmetic.

What the declaration does not claim is just as important. It does not assert that the strict positive-ratio realization is the only realization, nor that it is the most natural one. It does not claim that the arithmetic itself is new, only that it is the same arithmetic already known from LogicNat. It also does not claim anything about the physical content of the framework, such as the golden ratio or the eight-tick cycle; those are separate theorems built elsewhere. The declaration is a structural bridge, not a new discovery about arithmetic itself.

The practical consequence is that any theorem proved about LogicNat's arithmetic applies unchanged to the strict positive-ratio realization. A formal library that has developed results for one can reuse them for the other without re-proving them. This is the kind of bookkeeping that keeps a large machine-checked collection coherent: when two roads lead to the same arithmetic, the library records that fact once, and every later proof can cross the bridge freely.

/-- Strict positive-ratio forced arithmetic is canonically `LogicNat`. -/
noncomputable def positiveRatio_arith_equiv_logicNat
    (C : ComparisonOperator) (h : SatisfiesLawsOfLogic C) :
    (StrictLogicRealization.arith (strictPositiveRatioRealization C h)).peano.carrier
      ≃ ArithmeticFromLogic.LogicNat :=
  (StrictLogicRealization.toLightweight (strictPositiveRatioRealization C h)).orbitEquivLogicNat

/-- The strict-derived lightweight realization has the same forced arithmetic
as the existing positive-ratio lightweight wrapper. -/
noncomputable def positiveRatio_strict_equiv_existing
    (C : ComparisonOperator) (h : SatisfiesLawsOfLogic C) :
    (StrictLogicRealization.arith (strictPositiveRatioRealization C h)).peano.carrier
      ≃ (UniversalForcing.arithmeticOf (LogicRealization.ofPositiveRatioComparison C h)).peano.carrier :=
  ArithmeticOf.equivOfInitial
    (StrictLogicRealization.arith (strictPositiveRatioRealization C h))
    (UniversalForcing.arithmeticOf (LogicRealization.ofPositiveRatioComparison C h))

What this page does not claim

The strict positive-ratio realization is the only realization of the laws of logic. The arithmetic forced here is new or different from LogicNat. The declaration says anything about the physical constants or the eight-tick cycle.

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/UniversalForcing/Strict/PositiveRatio.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: