@@ -40,6 +40,7 @@ jobs:
           python3 scripts/audit_interval_capacity.py
           python3 scripts/audit_floor_excursion.py
           python3 scripts/audit_five_band_clock.py
+          python3 scripts/audit_rational_band_obstruction.py
 
       - name: Check exact first-descent intervals
         run: |
 
@@ -2110,3 +2110,4 @@ import Collatz.Exploration.IntervalCapacity
 import Collatz.Exploration.TwoStepCapacity
 import Collatz.Exploration.FloorExcursion
 import Collatz.Exploration.FiveBandClock
+import Collatz.Exploration.RationalBandObstruction
@@ -0,0 +1,177 @@
+import Collatz.Exploration.FloorExcursion
+
+/-! Odd-denominator rational Collatz dynamics encoded by natural numerators.
+With a fixed odd denominator d, the odd update on numerators is 3n+d;
+the even update halves an even numerator. All comparisons below are exact
+cross-multiplied rational comparisons. This map is distinct from step. -/
+namespace Collatz.Exploration.RationalBandObstruction
+
+def denominatorStep (d n : Nat) : Nat :=
+  if n % 2 = 0 then n / 2 else 3*n+d
+
+def denominatorOrbit (d : Nat) : Nat → Nat → Nat
+  | 0, n => n
+  | k+1, n => denominatorStep d (denominatorOrbit d k n)
+
+/-- Denominator one recovers the original integer map, including zero. -/
+theorem denominator_one_step (n : Nat) : denominatorStep 1 n = step n := by
+  by_cases hz : n = 0
+  · subst n; decide
+  · simp [denominatorStep, step, hz]
+
+theorem denominator_one_orbit (k n : Nat) : denominatorOrbit 1 k n = orbit k n := by
+  induction k with
+  | zero => rfl
+  | succ k ih =>
+    simp only [denominatorOrbit, ih, denominator_one_step, orbit_succ_steps]
+    exact (orbit_step_commute k n).symm
+
+/-- The branch word OEOEEOEE has this affine identity for every fixed offset. -/
+theorem word_identity (d x0 x1 x2 x3 x4 x5 x6 x7 x8 : Nat)
+    (h0 : x1 = 3*x0+d) (h1 : 2*x2 = x1)
+    (h2 : x3 = 3*x2+d) (h3 : 2*x4 = x3) (h4 : 2*x5 = x4)
+    (h5 : x6 = 3*x5+d) (h6 : 2*x7 = x6) (h7 : 2*x8 = x7) :
+    32*x8 = 27*x0+23*d := by omega
+
+/-- Closure in this word forces the encoding denominator to be divisible by five. -/
+theorem closure_denominator (d n : Nat) (h : 32*n = 27*n+23*d) : d%5 = 0 := by
+  omega
+
+/-- This word's closed encodings are exactly multiples of the primitive pair (5,23). -/
+theorem closure_classification (d n : Nat) (h : 32*n = 27*n+23*d) :
+    ∃ t, d = 5*t ∧ n = 23*t := by
+  have hd := closure_denominator d n h
+  refine ⟨d/5, ?_, ?_⟩ <;> omega
+
+/-- The rational 23/5 cycle, uniformly encoded at every odd scale. -/
+theorem scaled_transitions (t : Nat) (ht : t%2 = 1) :
+    denominatorStep (5*t) (23*t) = 74*t ∧
+    denominatorStep (5*t) (74*t) = 37*t ∧
+    denominatorStep (5*t) (37*t) = 116*t ∧
+    denominatorStep (5*t) (116*t) = 58*t ∧
+    denominatorStep (5*t) (58*t) = 29*t ∧
+    denominatorStep (5*t) (29*t) = 92*t ∧
+    denominatorStep (5*t) (92*t) = 46*t ∧
+    denominatorStep (5*t) (46*t) = 23*t := by
+  simp [denominatorStep, Nat.mul_mod, ht]
+  omega
+
+/-- These eight numerator values form a closed invariant set. -/
+def Member (t n : Nat) : Prop :=
+  n = 23*t ∨ n = 74*t ∨ n = 37*t ∨ n = 116*t ∨
+  n = 58*t ∨ n = 29*t ∨ n = 92*t ∨ n = 46*t
+
+theorem member_forward {t n : Nat} (ht : t%2 = 1) (h : Member t n) :
+    Member t (denominatorStep (5*t) n) := by
+  obtain ⟨h0,h1,h2,h3,h4,h5,h6,h7⟩ := scaled_transitions t ht
+  rcases h with h | h | h | h | h | h | h | h <;>
+    simp_all [Member]
+
+theorem orbit_member (t : Nat) (ht : t%2 = 1) (k : Nat) :
+    Member t (denominatorOrbit (5*t) k (23*t)) := by
+  induction k with
+  | zero => exact Or.inl rfl
+  | succ k ih => exact member_forward ht ih
+
+theorem cycle_eight (t : Nat) (ht : t%2 = 1) :
+    denominatorOrbit (5*t) 8 (23*t) = 23*t := by
+  obtain ⟨h0,h1,h2,h3,h4,h5,h6,h7⟩ := scaled_transitions t ht
+  simp only [denominatorOrbit, h0,h1,h2,h3,h4,h5,h6,h7]
+
+/-- The primitive normalized cycle has least positive period eight. -/
+theorem primitive_period : denominatorOrbit 5 8 23 = 23 ∧
+    ∀ k : Fin 7, denominatorOrbit 5 (k.val+1) 23 ≠ 23 := by decide
+
+/-- The numerator cycle stays in the interval [23t,116t] for all time. -/
+theorem bounds_all (t : Nat) (ht : t%2 = 1) (k : Nat) :
+    23*t ≤ denominatorOrbit (5*t) k (23*t) ∧
+    denominatorOrbit (5*t) k (23*t) ≤ 116*t := by
+  have h := orbit_member t ht k
+  rcases h with h | h | h | h | h | h | h | h <;> omega
+
+/-- Its rational minimum is greater than one, and the maximum ratio is 116/23. -/
+theorem rational_floor_certificate :
+    5 < 23 ∧ (∀ k, 23 ≤ denominatorOrbit 5 k 23 ∧
+      denominatorOrbit 5 k 23 ≤ 116) ∧ denominatorOrbit 5 3 23 = 116 := by
+  refine ⟨by decide, ?_, by decide⟩
+  intro k
+  simpa using bounds_all 1 (by decide) k
+
+/-- The cycle defeats every rational-interval clock at ratio 51/10. -/
+theorem band_fifty_one_tenths (k : Nat) :
+    23 ≤ denominatorOrbit 5 k 23 ∧ 10*denominatorOrbit 5 k 23 ≤ 51*23 := by
+  have h := bounds_all 1 (by decide) k
+  simp only [Nat.mul_one] at h
+  omega
+
+/-- It still exits the narrower ratio-five band, at its largest point. -/
+theorem exits_five_band : 5*23 < denominatorOrbit 5 3 23 := by decide
+
+/-- Even the multiplicative part 81/16 of the integer-floor bound fails here. -/
+theorem fails_integer_floor_excursion (k : Nat) :
+    16*denominatorOrbit 5 k 23 < 81*23 := by
+  have h := bounds_all 1 (by decide) k
+  simp only [Nat.mul_one] at h
+  omega
+
+/-- A uniform result for arbitrary odd offsets would wrongly exclude this cycle. -/
+theorem no_offset_band_exit :
+    ¬ (∀ d b n : Nat, d%2 = 1 → 1 < b →
+      ∃ k, denominatorOrbit d k n < b ∨
+        116*b < 23*denominatorOrbit d k n) := by
+  intro h
+  obtain ⟨k,hl | hu⟩ := h 5 23 23 (by decide) (by decide)
+  · have hb := bounds_all 1 (by decide) k
+    simp only [Nat.mul_one] at hb
+    omega
+  · have hb := bounds_all 1 (by decide) k
+    simp only [Nat.mul_one] at hb
+    omega
+
+/-- Changing the denominator changes the odd update; this is no integer cycle. -/
+theorem ordinary_map_control : step 23 = 70 ∧ denominatorStep 5 23 = 74 := by decide
+
+/-- The corresponding ordinary integer congruence class has an exact descending trace.
+This class was already closed in Strategy/ExcursionMap; this records the fixed clock. -/
+theorem integer_trace (q : Nat) :
+    step (32*q+11) = 96*q+34 ∧ step (96*q+34) = 48*q+17 ∧
+    step (48*q+17) = 144*q+52 ∧ step (144*q+52) = 72*q+26 ∧
+    step (72*q+26) = 36*q+13 ∧ step (36*q+13) = 108*q+40 ∧
+    step (108*q+40) = 54*q+20 ∧ step (54*q+20) = 27*q+10 := by
+  have h0 : (32*q+11)%2 = 1 := by omega
+  have h1 : (96*q+34)%2 = 0 := by omega
+  have h2 : (48*q+17)%2 = 1 := by omega
+  have h3 : (144*q+52)%2 = 0 := by omega
+  have h4 : (72*q+26)%2 = 0 := by omega
+  have h5 : (36*q+13)%2 = 1 := by omega
+  have h6 : (108*q+40)%2 = 0 := by omega
+  have h7 : (54*q+20)%2 = 0 := by omega
+  simp [step, h0,h1,h2,h3,h4,h5,h6,h7]
+  omega
+
+theorem integer_eighth_value (q : Nat) : orbit 8 (32*q+11) = 27*q+10 := by
+  obtain ⟨h0,h1,h2,h3,h4,h5,h6,h7⟩ := integer_trace q
+  simp only [orbit, h0,h1,h2,h3,h4,h5,h6,h7]
+
+theorem integer_strict_descent (q : Nat) : orbit 8 (32*q+11) < 32*q+11 := by
+  rw [integer_eighth_value]
+  omega
+
+/-- The formal affine return identity, exposing the rational fixed point 23/5. -/
+theorem integer_return_identity (q : Nat) :
+    32*orbit 8 (32*q+11) = 27*(32*q+11)+23 := by
+  rw [integer_eighth_value]
+  omega
+
+/-- The word's affine identity enforces the exact integer source residue. -/
+theorem integer_source_residue (n r : Nat) (h : 32*r = 27*n+23) : n%32 = 11 := by
+  omega
+
+theorem integer_descent_of_residue {n : Nat} (h : n%32 = 11) : orbit 8 n < n := by
+  have hn : n = 32*(n/32)+11 := by omega
+  rw [hn]
+  exact integer_strict_descent (n/32)
+
+theorem no_integer_fixed_point (n : Nat) : ¬ (32*n = 27*n+23) := by omega
+
+end Collatz.Exploration.RationalBandObstruction
@@ -35,6 +35,9 @@ own verification instructions.
   a hypothetical orbit floor to exceed five times its starting value. Every
   arbitrary-start orbit exits `[b,5b]` within twelve steps for `b>1`; the
   clock is sharp and yields conditional high-visit witnesses.
+- [Rational band obstruction](Research/RationalBandObstruction.md) — a
+  denominator-aware cycle certificate, exact closure classification, and
+  why the integer floor bound does not extend to rational floors.
 
 - [First passage through 2,592 steps](Research/PassageAtlas/README.md) —
   a stronger conditional descent theorem, an exact residual condition
 
@@ -0,0 +1,89 @@
+# Rational band obstruction and integer return clock
+
+The investigation of wider bands exposed a limit of the real affine
+relaxation used to guide the ratio-five certificate. It is not sufficient
+to strengthen an integer theorem by treating its orbit values and anchor
+as unconstrained rational numbers. This note records a counterexample to
+that transfer, not a counterexample to the integer Collatz conjecture.
+
+## Exact denominator encoding
+
+For an odd fixed denominator `d`, a rational state `n/d` has an even or
+odd numerator. Its numerator update is
+
+`denominatorStep(d,n) = n/2` if `n` is even, and `3n+d` otherwise.
+
+An even numerator is halved exactly; the odd denominator remains fixed.
+Reducing such a fraction cancels an odd common factor and preserves the
+numerator parity. At denominator one, Lean proves both the step and the
+whole orbit equal the original integer definitions, including zero.
+The Lean file works with natural numerators and exact cross-multiplied
+comparisons; it does not silently identify the offset map with `3n+1`.
+
+At denominator five the numerator cycle is
+
+`23→74→37→116→58→29→92→46→23`.
+
+Lean proves its least positive period is eight and every future value lies
+in `[23,116]`. Every odd scale `t` gives the encoding with denominator `5t`
+and numerators multiplied by `t`; the normalized rational cycle is the
+same. Even scales are deliberately excluded from the numerator parity
+statement and rejected by a test control.
+
+The underlying affine cycle method is standard. [Halbeisen and
+Hungerbühler, *Optimal Bounds for the Length of Rational Collatz Cycles*](https://people.math.ethz.ch/~halorenz/publications/pdf/collatz.pdf)
+define the odd-denominator rational parity rule and present the affine
+parity-word fixed-point formula (Lemma 2, attributed there to Lagarias).
+Their accelerated map includes an odd update followed immediately by a
+halving. The ordinary eight-step word here corresponds to the five-step
+accelerated word `11010`. No priority claim is made for this rational cycle
+or the standard affine identity.
+
+## Why integrality matters
+
+The rational minimum is `23/5>1`. The maximum/minimum ratio is
+`116/23≈5.04348`, so every state remains in the ratio-`51/10` band anchored
+at that minimum. Yet every value is strictly less than `(81/16)*(23/5)`.
+The exact gap between that threshold and the maximum is `7/80`.
+Consequently, even the multiplicative part of the repository's integer
+floor excursion theorem fails for this rational floor. The cycle does
+exceed five times its minimum, by `1/5`, and therefore does not refute the
+ratio-five excursion result.
+
+Lean proves the generalized return equation for the branch word `OEOEEOEE`:
+
+`32*x8 = 27*x0 + 23*d`.
+
+Closure forces `5*x0=23*d`, and the full natural-number classification is
+`d=5t`, `x0=23t`. In particular, denominator one has no closed encoding in
+this word. The actual integer class `n=32q+11` instead satisfies
+
+`C^8(n)=27q+10<n`.
+
+The code gives its exact eight-step trace, return identity, and the converse
+source-residue constraint. This integer class was already closed in
+`Strategy/ExcursionMap.lean`; the new file records the fixed clock and its
+relationship to the rational closure obstruction. It is not a newly
+resolved residue class or an established frontier discovery.
+
+The exploratory real-affine guide exhausted ratio five at depth twelve,
+but retained feasible prefixes at depth 48 for several larger ratios.
+Those surviving prefixes are evidence about a relaxation, not integer
+orbits. In particular, the rational anchor `23/5` is not an allowed natural
+anchor in the current band-clock theorem. No wider-band integer exit
+clock is refuted or proved by this exploration. A subsequent search can
+use the anchor's integrality and state congruences before declaring a
+prefix viable.
+
+## Verification
+
+Run `python3 scripts/audit_rational_band_obstruction.py`. It builds the
+module, checks all 24 named theorem axiom footprints, scans the source for
+proof escapes, and requires Lean to reject four false transfers. Independent
+Fraction tests check 10,000 rational states, 4,100 odd scales including large
+integers, 56 exact affine branch words (16 parity-valid), 10,004 integer
+traces, and denominator-one/even-scale controls. These finite tests
+corroborate the universal Lean proofs; no computation is imported as an
+axiom. The library export and CI include the new audit.
+
+The conjecture and the requested frontier-novel proportion remain open.
@@ -0,0 +1,29 @@
+#!/usr/bin/env python3
+"""Build, independently test, audit axioms, and reject false denominator transfers."""
+import subprocess
+from audit_barrier_kernel import ROOT, check_axioms, check_false_certificates
+from check_proof_escapes import violations
+
+MODULE = 'Collatz.Exploration.RationalBandObstruction'
+SOURCE = ROOT / 'Collatz/Exploration/RationalBandObstruction.lean'
+
+
+def main():
+    assert not violations(SOURCE.read_text())
+    subprocess.run(['lake', 'build', MODULE], cwd=ROOT, check=True)
+    subprocess.run(['python3', str(ROOT / 'scripts/test_rational_band_obstruction.py')],
+                   cwd=ROOT, check=True)
+    count = check_axioms(SOURCE, MODULE)
+    prefix = 'Collatz.Exploration.RationalBandObstruction.'
+    claims = [
+        f'example : {prefix}denominatorOrbit 5 8 23 = 24 := by decide\n',
+        f'example : {prefix}denominatorStep 1 23 = 74 := by decide\n',
+        f'example : {prefix}denominatorOrbit 10 8 46 = 46 := by decide\n',
+        'example : Collatz.orbit 8 11 = 11 := by decide\n',
+    ]
+    rejected = check_false_certificates(MODULE, claims)
+    print(f'{count} theorem axiom footprints checked; {rejected} false transfers rejected')
+
+
+if __name__ == '__main__':
+    main()
@@ -0,0 +1,76 @@
+#!/usr/bin/env python3
+"""Exact Fraction dynamics, odd-scale encodings, and integer comparison controls."""
+from fractions import Fraction as F
+from itertools import combinations
+from test_barrier_kernel import trajectory
+
+
+def rational_step(x):
+    assert x.denominator % 2 == 1
+    return x/2 if x.numerator % 2 == 0 else 3*x+1
+
+
+def numerator_step(d, n):
+    return n//2 if n % 2 == 0 else 3*n+d
+
+
+def main():
+    expected = [23, 74, 37, 116, 58, 29, 92, 46]
+    x = F(23, 5)
+    for k in range(10000):
+        assert x == F(expected[k % 8], 5)
+        assert F(23, 5) <= x <= F(116, 5)
+        assert x < F(81, 16)*F(23, 5)
+        x = rational_step(x)
+    assert x == F(23, 5)
+    assert F(81, 16)*F(23, 5)-F(116, 5) == F(7, 80)
+    assert F(116, 23) < F(51, 10)
+    scales = list(range(1, 8192, 2)) + [2**p-1 for p in (90, 180, 512, 1024)]
+    for t in scales:
+        n = 23*t
+        for k in range(64):
+            assert n == expected[k % 8]*t
+            assert F(n, 5*t) == F(expected[k % 8], 5)
+            n = numerator_step(5*t, n)
+        assert n == 23*t
+    # Systematic enumeration of the 56 branch words with three odd updates.
+    words = genuine = 0
+    ratios = []
+    for positions in combinations(range(8), 3):
+        word = ''.join('1' if i in positions else '0' for i in range(8))
+        a, c = F(1), F(0)
+        for bit in word:
+            a, c = (a/2, c/2) if bit == '0' else (3*a, 3*c+1)
+        assert a == F(27, 32)
+        start = c/(1-a)
+        states = []
+        x = start
+        valid = True
+        for bit in word:
+            states.append(x)
+            valid &= (x.numerator % 2 == int(bit)) and x.denominator % 2 == 1
+            x = x/2 if bit == '0' else 3*x+1
+        assert x == start
+        words += 1
+        if valid:
+            genuine += 1
+            ratios.append(max(states)/min(states))
+    assert words == 56 and genuine == 16 and min(ratios) == F(116, 23)
+    qs = list(range(10000)) + [2**p-1 for p in (90, 180, 512, 1024)]
+    for q in qs:
+        values = trajectory(32*q+11, 8)
+        assert values == [32*q+11, 96*q+34, 48*q+17, 144*q+52,
+                          72*q+26, 36*q+13, 108*q+40, 54*q+20, 27*q+10]
+        assert values[-1] < values[0]
+        assert 32*values[-1] == 27*values[0]+23
+    # Actual integer dynamics and a changed/even denominator must not be conflated.
+    assert numerator_step(5, 23) == 74 and trajectory(23, 1)[1] == 70
+    assert numerator_step(10, 46) != 74*2
+    for n in range(10000):
+        assert numerator_step(1, n) == trajectory(n, 1)[1]
+    print(f'10000 rational states; {len(scales)} odd scales; {words} exact affine words '
+          f'({genuine} parity-valid); {len(qs)} integer traces; bridge and denominator controls passed')
+
+
+if __name__ == '__main__':
+    main()