Foundation Primitive Recognition Calculus Grow Ratio Orbit Zero Lt One

The first rung of the ratio orbit

The ratio orbit is a sequence of ratios that the Recognition Science framework uses to model how a discrete record of events, its ledger, grows. The orbit starts at a zero ratio and moves through a one ratio, then onward. The module RatioOrbitZeroLtOne establishes the very first ordering fact about that orbit: the zero ratio is strictly less than the one ratio. In plain terms, the starting point of the orbit is genuinely smaller than its first nontrivial step; the orbit does not begin by standing still or jumping backward.

The proof is a formal proof, checked by a machine. It unpacks the definition of the ordering relation on ratios, compares the two ratios by their natural-number representations, and shows that they are not equal. The equality case is ruled out by a direct computation. Nothing about the framework's physical interpretation is needed for this step; the ordering is a purely combinatorial fact about the orbit's construction.

In Recognition Science, this ordering is the first rung of a ladder. The framework proves that the ratio orbit's growth follows a forced pattern, and that pattern eventually leads to the golden ratio as the unique self-similar scaling. The zero-below-one fact is the anchor that makes the orbit's direction unambiguous: growth starts at zero, moves to one, and never collapses those two positions into a single point. Without this ordering, the orbit could not serve as a model of increasing recognition cost.

The consequence for a reader is simple. The framework's growth dynamics have a definite starting point, and that starting point is strictly before the first step. This is not a numerical accident; it is a theorem about the orbit's definition. The rest of the framework's claims about growth, scaling, and the golden ratio build on this foundation.

theorem zero_ltQ_one : ltQ RatioOrbit.zero RatioOrbit.one := by
  unfold ltQ
  refine ⟨?_, ?_⟩
  · unfold leQ
    rw [le_iff_toNat_cf]
    decide
  · intro h
    have hf : ¬ RatioOrbit.crossEq RatioOrbit.zero RatioOrbit.one := by decide
    exact hf h

What this page does not claim

The ratio orbit's full sequence or its limit is not derived here. The physical interpretation of the ledger is not established by this module. The golden ratio result is not proved in this module; it is a later step in the framework.

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/PrimitiveRecognitionCalculus/Grow/RatioOrbitZeroLtOne.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: