Foundation Primitive Recognition Calculus Grow Ratio Orbit Zero Lt One Zero Lt Q

Ordering the ratio orbit

The declaration zero_ltQ_one is a formal theorem in the Recognition Science framework's machine-checked library of formal theorems. It establishes a precise ordering fact about the first two entries of a discrete sequence called the ratio orbit, a record of successive growth ratios that the framework uses to model scaling behavior. The theorem proves that the entry named zero is strictly less than the entry named one under the framework's own ordering relation ltQ. In plain terms, the first step of this growth sequence is strictly smaller than the second step, and the two steps are not equal.

The proof is fully checked by machine and rests on two direct computations. One part unfolds the ordering relation and decides the comparison between the two entries by calculation. The other part shows that the two entries are not equal by a separate computation, so the ordering is strict rather than merely non-strict. The theorem is axiom-clean, meaning it uses only the standard logical axioms of the underlying type theory and no framework-specific assumptions. This makes the ordering fact a proved theorem in the framework, not a definitional choice or an unverified hypothesis.

What the theorem does not claim is just as important as what it proves. It does not say that the ratio orbit is strictly increasing everywhere, only that the first two entries obey this ordering. It does not assign numerical values to these entries, does not say what growth process the orbit describes, and does not claim that this ordering extends to any later pair of entries. The theorem is a single local fact about the first two steps of a sequence, not a statement about the sequence as a whole.

In Recognition Science, this ordering fact sits at the base of a larger forcing chain that derives constants and dimensional structure from the cost function J(x) = (x + 1/x)/2 - 1. The chain is proved in the framework's library, and this theorem is one of its early rungs. But the theorem itself is deliberately narrow: it pins down the first comparison in a discrete growth record, and nothing more. A reader should take it as a verified local fact, not as evidence about the global behavior of the orbit or about any physical system the orbit might later describe.

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

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 is strictly increasing everywhere. The theorem assigns numerical values to the zero and one entries. The ordering extends to any pair of entries beyond the first two.

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: