UOR Chaos Lean

UorChaos.lean

/-!
# Exact Chaotic Systems in UOR — The Driftless Torus

This file formalizes a chaotic dynamical system under the UOR paradigm, in the
same proof style as the UOR matmul file (`UorMatMul.lean`): first pin the exact
semantics, then prove codec-invariance as a congruence over the pinned
semantics, and finally prove the exact closure / bijection / hyperbolicity
facts that make the prose claim mathematical rather than heuristic. It follows
the uor-addr / F1 Lean discipline: core Lean 4 v4.16.0, no Mathlib, no `sorry`,
proofs by `decide` / `omega` / `rfl` / rewriting (`rw`, `rwa`, `calc`) plus
structural induction, case analysis, and quotient soundness; axiom base
`{propext, Quot.sound}`.

## The claim, without classical assumptions

Classical numerical chaos is usually simulated by integrating real-valued
differential equations with floating-point arithmetic. That mixes two different
effects: true sensitivity of the mathematical system, and substrate-dependent
rounding / truncation. UOR grants no field of reals, no hidden floating state,
and no tolerance threshold.

The UOR statement here is:

  * The phase space is the discrete torus of modulus `N`: the quotient of the
    integer plane by the period lattice, `Torus N = ℤ² / (Nℤ)²`. A point *is*
    its address in the equivalence class — the UOR canonical-form-→-κ shape,
    realized as an actual Lean quotient type.
  * A stored initial condition is a **codec**: a decode function
    `d : Code → Point` from any stored code type into exact integer
    coordinates.
  * Evolution is the exact integer cat-map morphism induced by the matrix

        [2 1]
        [1 1]

    with determinant `1`, trace `3`, and hyperbolic discriminant `5`.
  * Canonical representatives are obtained by exact integer remainder (`emod`),
    and the quotient torus is acted on by an exact automorphism with an
    explicit inverse.

**Theorem (topological orbit invariance).** If two codecs decode to the same
exact initial torus address, the chaotic trajectory agrees at every discrete
time `t : Nat`. (The invariance itself is a congruence; its content is the
uniquely pinned evolution it transports — CL-CH02 — and the closure,
realization, and bijection theorems around it.) If the decoded representative
is canonical and `0 < N`, every state stays in the canonical phase box
`[0,N) × [0,N)`. On the quotient torus the cat map is a bijection with
explicit inverse — at every time depth, not just one step — so the driftless
dynamics is an exact topological automorphism, not a floating simulation.

## Conceptual model and scientific method

The four rules of the matmul file, applied to dynamics.

1. **Exactness replaces thresholds.** There is no integrator, no step size,
   and no error tolerance anywhere in this file. The evolution is repeated
   exact integer matrix action followed by exact integer remainder; every
   confinement, reversibility, and sensitivity statement is an identity —
   over `ℤ` or in the quotient `Torus N` — or an integer inequality,
   kernel-checked. Where a float simulation of the cat map drifts by
   substrate, the exact orbit is one integer sequence.

2. **Parametricity: every constant derives from declared parameters.** The
   modulus `N : Int` is a parameter throughout; no theorem before the audit
   section instantiates it. The map `catRaw` is the single declared dynamical
   datum: the matrix entries are *read off its basis action* (`catA`–`catD`
   are projections of `catRaw (1,0)` and `catRaw (0,1)`),
   `catRaw_matrix_action` proves the map is exactly the linear map with those
   entries, and the invariants — determinant `1`, trace `3`, discriminant `5`
   — are `decide`-pinned theorems about those derived entries, not parallel
   declarations. Codecs are parametric over their code type, so every storage
   tier is one theorem.

3. **Kernel authority and a minimal axiom base.** Every theorem is checked by
   the Lean 4 v4.16.0 kernel with no `sorry`, no Mathlib, and no
   `native_decide`; the `#print axioms` audit at the end shows every proof
   closes over at most `{propext, Quot.sound}` — and for the quotient-level
   theorems `Quot.sound` is not incidental bookkeeping but the mathematical
   content: the torus *is* a quotient, and address-level equalities are sound
   exactly because the maps respect the period lattice. (For the pure integer
   lemmas it enters only through core arithmetic; §7 draws the line
   precisely.)

4. **Status discipline: theorems vs. provenance.** Everything asserted about
   the dynamics in this file is a Lean theorem, grouped under `CL-CH01`
   through `CL-CH06` in this header; supporting lemmas are unlabeled. The
   file makes no runtime claims; the analogies to storage tiers and
   substrates in the prose describe the intended UOR reading of the codec
   interface and carry no formal weight.

## What this file proves

1. **CL-CH01 — codec-invariance** (`orbit_invariance`,
   `transcode_orbit_invariance`, `torus_orbit_invariance`,
   `torus_transcode_orbit_invariance`). Equal decoded initial data — as exact
   representatives, or merely as torus addresses — yields identical exact
   trajectories at every discrete time. These are congruences, and they are
   anchored to the real dynamics by the pinning theorems of CL-CH02.
2. **CL-CH02 — pinned semantics** (`orbit_zero`, `orbit_succ`, `orbit_unique`,
   `torusOrbit_zero`, `torusOrbit_succ`, `torusOrbit_unique`, plus the flow
   laws `orbit_add`, `torusOrbit_add`). The two computation rules characterize
   each orbit map uniquely: any function satisfying them *is* the orbit. The
   congruence theorems therefore transport this exact evolution, not an
   unconstrained function of the inputs.
3. **CL-CH03 — exact phase confinement** (`phase_bound`,
   `projectPhase_closed`, `catMap_closed`, `orbit_bounded`,
   `orbit_after_step_bounded`, `decoded_orbit_bounded`). For `0 < N`, the
   canonical orbit never leaves `[0,N) × [0,N)`; from any raw representative
   it enters the box after one step and stays.
4. **CL-CH04 — canonical form is a complete address invariant, and the
   representative dynamics realizes the quotient automorphism**
   (`congruent_iff_emod_eq`, `torusRel_iff_projectPhase_eq`, `torusMk_exact`,
   `torusMk_eq_iff`, `torusMk_eq_iff_canon`, `phase_box_unique`,
   `torusMk_projectPhase`, `catMap_realizes`, `orbit_realizes`,
   `orbit_congruent`, `orbit_canonical_eq`, `catMap_box_injective`,
   `catMap_box_surjective`). Two representatives name the same torus address
   iff their canonical forms are equal (the κ decision, both directions);
   the phase box is a strict fundamental domain (at most one representative
   per address, exactly one when `0 < N`); and the `mod-N` representative
   orbit is *exactly* the quotient orbit read through the quotient
   constructor `torusMk` — the discrete analogue of the matmul file's
   machine-realization theorem. On the phase box, one exact cat-map step is
   itself a bijection.
5. **CL-CH05 — exact automorphism structure** (`catRawInv_catRaw`,
   `catRaw_catRawInv`, `torusCatInv_torusCat`, `torusCat_torusCatInv`,
   `torusCat_injective`, `torusCat_surjective`, `torusRewind_torusOrbit`,
   `torusOrbit_torusRewind`, `torusOrbit_injective`, `torusOrbit_surjective`,
   `torusOrbit_step_reversible`, `torusOrbit_collision_period`). The quotient
   cat map has an explicit two-sided inverse; the `t`-step evolution is a
   bijection for *every* `t`, with an explicit `t`-step rewind; and any
   collision transports to a period at time zero —
   `torusOrbit N z s = torusOrbit N z t` with `s ≤ t` gives
   `torusOrbit N z (t−s) = z` (nontrivial whenever `s < t`). No information
   is ever lost: the dynamics is driftless in the strongest sense
   expressible.
6. **CL-CH06 — exact hyperbolicity and sensitivity** (`catA_eq`–`catD_eq`,
   `catRaw_matrix_action`, `catDet_eq_one`, `catTrace_eq_three`,
   `cat_hyperbolic_signature`, `discriminant_not_square`,
   `cat_no_integer_eigenvalue`, `catRaw_psub`, `rawOrbit_psub`,
   `one_le_two_pow`, `rawOrbit_expansion`, `exact_sensitivity`,
   `catRaw_infinite_order`). The matrix entries are derived from the map's
   basis action and proved to reproduce it on every input; the matrix is
   unimodular
   with trace `3 > 2` and discriminant `5`; `5` is not a perfect square and
   the characteristic polynomial `λ² − 3λ + 1` has no integer root, so the
   expansion is along irrational directions (classically the algebraic
   ingredient behind mixing of the *continuous* cat map — not proved here).
   Sensitivity is proved exactly on the linear lift: the difference of two
   lifted trajectories evolves linearly, and a unit initial difference
   `(1,0)` separates at least exponentially, `2ᵗ ≤ Δx(t)` — with the
   corollary that the lift has infinite order. No float is consulted to
   witness "chaos"; the exponential separation is an integer inequality.

## What it does NOT prove — say this plainly

- **No existence-of-collision (periodicity) claim.** `torusOrbit_collision_period`
  transports a collision to a period; it does not prove a collision exists.
  That would follow from finiteness of the torus by pigeonhole, which needs
  finite-type machinery deliberately out of scope for a core-only file. The
  conditional transport is exact; the existence is left unformalized.
- **No measure-theoretic chaos claims.** Ergodicity, mixing rates, and
  entropy of the cat map are real-analysis theorems about the continuous
  torus; nothing here asserts them. The file proves the exact discrete
  skeleton: hyperbolic signature, irrational eigendirections, exponential
  lift separation, and driftless bijectivity.
- **Sensitivity is stated on the lift.** On the finite torus, coordinates are
  bounded by `N`, so "exponential separation" is only meaningful before
  reduction; the theorem is therefore stated for the exact linear lift
  (`rawOrbit`), where it is unconditionally true. The torus statement that
  survives reduction is exactness itself: addresses never blur, so
  sensitivity is a property of the map, not an artifact of rounding.
- **No runtime claims.** Unlike the matmul file there is no hologram
  provenance here; the codec interface is the UOR shape, and every assertion
  about it in this file is a theorem.

## Check contract

Kernel-checked. This file compiles standalone against core Lean 4 v4.16.0
(the uor-addr / F1 toolchain pin) with no errors, no warnings, no `sorry`,
and no imports beyond the prelude:

```
$ lean +leanprover/lean4:v4.16.0 UorChaos.lean
# expect: exit 0; the only output is the §7 axiom audit (one informational
# line per audited theorem); no errors, no warnings.
# (The +toolchain pin is explicit because this standalone file ships with no
# lean-toolchain file; any elan-managed install resolves it.)
```

The proofs use only core rewriting, structural induction, case analysis,
quotient soundness, `decide`, and `omega`. `set_option autoImplicit false`
and `set_option linter.missingDocs true` are enforced file-wide, so every
declaration carries a docstring and no variable is bound automatically.
-/

set_option autoImplicit false
set_option linter.missingDocs true

namespace UorChaos

/-! ## 0. The discrete manifold, quotient address, and codec model

The modulus `N : Int` is a parameter everywhere; positivity is assumed only
where a theorem genuinely needs it (phase-box confinement and fundamental-
domain uniqueness), never for the algebra of the quotient. -/

/-- A coordinate pair on the integer plane. Canonical representatives of the
finite torus are the points satisfying `InPhaseSpace N`; quotient torus
addresses are represented by `Torus N`. -/
abbrev Point := Int × Int

/-- One-dimensional congruence modulo `N`, written without division. This is
the address-equivalence relation behind the torus quotient: two coordinates
name the same torus address when their difference is an integer multiple of
`N`. -/
def Congruent (N : Int) (x y : Int) : Prop :=
  ∃ k : Int, x - y = k * N

/-- Product congruence on coordinate pairs. -/
def TorusRel (N : Int) (p q : Point) : Prop :=
  Congruent N p.1 q.1 ∧ Congruent N p.2 q.2

/-- Reflexivity of torus-address equivalence. -/
theorem torusRel_refl (N : Int) (p : Point) : TorusRel N p p :=
  ⟨⟨0, by omega⟩, ⟨0, by omega⟩⟩

/-- Symmetry of torus-address equivalence: negate the lattice witnesses. -/
theorem torusRel_symm (N : Int) {p q : Point}
    (h : TorusRel N p q) : TorusRel N q p := by
  rcases h with ⟨⟨kx, hx⟩, ⟨ky, hy⟩⟩
  refine ⟨⟨-kx, ?_⟩, ⟨-ky, ?_⟩⟩
  · have hb := Int.neg_mul kx N
    omega
  · have hb := Int.neg_mul ky N
    omega

/-- Transitivity of torus-address equivalence: add the lattice witnesses. -/
theorem torusRel_trans (N : Int) {p q r : Point}
    (hpq : TorusRel N p q) (hqr : TorusRel N q r) : TorusRel N p r := by
  rcases hpq with ⟨⟨kx, hx⟩, ⟨ky, hy⟩⟩
  rcases hqr with ⟨⟨lx, hlx⟩, ⟨ly, hly⟩⟩
  refine ⟨⟨kx + lx, ?_⟩, ⟨ky + ly, ?_⟩⟩
  · have hb := Int.add_mul kx lx N
    omega
  · have hb := Int.add_mul ky ly N
    omega

/-- The quotient torus: a point is its address modulo the period lattice. This
is the UOR form of the state space: the object is its address in the
equivalence class, not a floating representative. -/
abbrev Torus (N : Int) := Quot (TorusRel N)

/-- The quotient constructor for torus addresses. -/
def torusMk (N : Int) (p : Point) : Torus N :=
  Quot.mk (TorusRel N) p

/-- Formal definition of the canonical phase box. A representative is canonical
when both coordinates lie in `[0,N)`. -/
def InPhaseSpace (N : Int) (p : Point) : Prop :=
  0 ≤ p.1 ∧ p.1 < N ∧ 0 ≤ p.2 ∧ p.2 < N

/-- A **codec** evaluates a stored initial condition, of any type, into an
exact integer coordinate representative. -/
def decodedState {Code : Type} (d : Code → Point) (c : Code) : Point :=
  d c

/-- A quotient-valued decoded state: the decoded representative is immediately
viewed as its torus address. This is the strongest codec interface because
different representatives of the same modulo-`N` address are identified. -/
def decodedTorusState {Code : Type} (N : Int) (d : Code → Point)
    (c : Code) : Torus N :=
  torusMk N (decodedState d c)

/-! ### Canonical form is a complete address invariant (CL-CH04, κ half)

Congruence modulo `N` is *equivalent* to equality of exact remainders, in both
directions and for every `N` (including `N = 0`, where `x % 0 = x` and the
congruence degenerates to equality). This upgrades canonicalization from a
convenience to a decision procedure: two representatives name the same torus
address iff their canonical forms are syntactically equal. -/

/-- Congruent coordinates have equal exact remainders. -/
theorem congruent_emod_eq {N x y : Int} (h : Congruent N x y) :
    x % N = y % N := by
  rcases h with ⟨k, hk⟩
  have hx : x = y + N * k := by
    have hb := Int.mul_comm k N
    omega
  rw [hx, Int.add_mul_emod_self_left]

/-- Equal exact remainders are congruent: the lattice witness is the
difference of the exact quotients. -/
theorem emod_eq_congruent {N x y : Int} (h : x % N = y % N) :
    Congruent N x y := by
  refine ⟨x / N - y / N, ?_⟩
  have hx := Int.emod_add_ediv x N
  have hy := Int.emod_add_ediv y N
  have hb : (x / N - y / N) * N = N * (x / N) - N * (y / N) := by
    have h1 := Int.sub_mul (x / N) (y / N) N
    have h2 := Int.mul_comm (x / N) N
    have h3 := Int.mul_comm (y / N) N
    omega
  omega

/-- **The κ decision, coordinate form.** Congruence modulo `N` reduces to
equality of exact remainders — a propositional reduction to decidable integer
equality (no `Decidable` instance is registered; none is needed for the
theorems here). -/
theorem congruent_iff_emod_eq (N x y : Int) :
    Congruent N x y ↔ x % N = y % N :=
  ⟨congruent_emod_eq, emod_eq_congruent⟩

/-! ## 1. Exact cat-map algebra: the topological automorphism -/

/-- The raw integer cat map induced by the matrix `[[2,1],[1,1]]`. This is the
algebraic morphism before choosing canonical representatives. -/
def catRaw (p : Point) : Point :=
  (2 * p.1 + p.2, p.1 + p.2)

/-- The raw inverse matrix `[[1,-1],[-1,2]]`. -/
def catRawInv (p : Point) : Point :=
  (p.1 - p.2, -p.1 + 2 * p.2)

/-! ### The matrix invariants, derived from the map itself

The entries below are *read off `catRaw`'s action on the basis* — they are
projections of `catRaw (1,0)` and `catRaw (0,1)`, not parallel numeric
declarations — and `catRaw_matrix_action` proves that `catRaw` is exactly the
linear map with those entries on every input. Determinant, trace, and
discriminant are then defined from the entries. Editing `catRaw` therefore
breaks these theorems rather than silently orphaning them: the invariants are
formally traceable to the single declared dynamical datum. -/

/-- Matrix entry `a₁₁`, read off the map: first coordinate of `catRaw (1,0)`. -/
def catA : Int := (catRaw (1, 0)).1

/-- Matrix entry `a₁₂`, read off the map: first coordinate of `catRaw (0,1)`. -/
def catB : Int := (catRaw (0, 1)).1

/-- Matrix entry `a₂₁`, read off the map: second coordinate of `catRaw (1,0)`. -/
def catC : Int := (catRaw (1, 0)).2

/-- Matrix entry `a₂₂`, read off the map: second coordinate of `catRaw (0,1)`. -/
def catD : Int := (catRaw (0, 1)).2

/-- Entry pin `a₁₁ = 2`, kernel-computed from the map. -/
theorem catA_eq : catA = 2 := by decide

/-- Entry pin `a₁₂ = 1`, kernel-computed from the map. -/
theorem catB_eq : catB = 1 := by decide

/-- Entry pin `a₂₁ = 1`, kernel-computed from the map. -/
theorem catC_eq : catC = 1 := by decide

/-- Entry pin `a₂₂ = 1`, kernel-computed from the map. -/
theorem catD_eq : catD = 1 := by decide

/-- **The map is its matrix.** `catRaw` acts on every point as the linear map
with the basis-derived entries: the traceability theorem that ties every
invariant below to the actual dynamics, closing the loop between the declared
map and the numbers cited about it. -/
theorem catRaw_matrix_action (p : Point) :
    catRaw p = (catA * p.1 + catB * p.2, catC * p.1 + catD * p.2) := by
  rw [catA_eq, catB_eq, catC_eq, catD_eq]
  cases p with
  | mk x y =>
    show (2 * x + y, x + y) = (2 * x + 1 * y, 1 * x + 1 * y)
    rw [Prod.mk.injEq]
    constructor <;> omega

/-- The determinant of the cat-map matrix, from the basis-derived entries. -/
def catDet : Int := catA * catD - catB * catC

/-- The trace of the cat-map matrix, from the basis-derived entries. -/
def catTrace : Int := catA + catD

/-- The hyperbolic discriminant `trace² - 4·determinant`. -/
def catDiscriminant : Int := catTrace * catTrace - 4 * catDet

/-- The exact determinant pin: the cat-map matrix is unimodular. -/
theorem catDet_eq_one : catDet = 1 := by decide

/-- The exact trace pin. -/
theorem catTrace_eq_three : catTrace = 3 := by decide

/-- The exact hyperbolic signature of Arnold's cat map: determinant `1`,
trace `3`, discriminant `5`, and `|trace| > 2` (the hyperbolicity criterion
for unimodular matrices). This is the algebraic source of the mathematical
sensitivity; it is not a property of floating arithmetic. -/
theorem cat_hyperbolic_signature :
    catDet = 1 ∧ catTrace = 3 ∧ catDiscriminant = 5 ∧ 2 < catTrace.natAbs := by
  decide

/-- The discriminant `5` is not a perfect square: no integer squares to it.
Case analysis on the magnitude — squares of `{0,1,2}` are at most `4`, squares
of magnitude `≥ 3` are at least `9`. Hence the eigenvalues `(3 ± √5)/2` are
irrational, which is the exact algebraic content of "the expanding direction
is irrational" — classically the ingredient behind mixing of the *continuous*
cat map, which is not proved here. -/
theorem discriminant_not_square (m : Int) : m * m ≠ catDiscriminant := by
  intro h
  have h5 : m.natAbs * m.natAbs = 5 := by
    have hcast := congrArg Int.natAbs h
    rwa [Int.natAbs_mul] at hcast
  rcases Nat.lt_or_ge m.natAbs 3 with hlt | hge
  · have hle : m.natAbs ≤ 2 := by omega
    have hbound : m.natAbs * m.natAbs ≤ 2 * 2 := Nat.mul_le_mul hle hle
    omega
  · have hbound : 3 * 3 ≤ m.natAbs * m.natAbs := Nat.mul_le_mul hge hge
    omega

/-- The characteristic polynomial `λ² − (trace)λ + det = λ² − 3λ + 1` has no
integer root: the cat map has no integer eigenvalue, so no lattice direction
is preserved with an integer scale factor. Together with
`discriminant_not_square` this pins, in exact integer arithmetic, that the
expansion happens along irrational eigendirections. -/
theorem cat_no_integer_eigenvalue (l : Int) :
    l * l - catTrace * l + catDet ≠ 0 := by
  intro h
  rw [catTrace_eq_three, catDet_eq_one] at h
  rcases Int.le_total l 0 with hl | hl
  · have hnn : 0 ≤ (-l) * (-l) := Int.mul_nonneg (by omega) (by omega)
    have hb := Int.neg_mul_neg l l
    omega
  · have hsplit : l ≤ 2 ∨ 3 ≤ l := by omega
    rcases hsplit with hle2 | hge3
    · have hcase : l = 0 ∨ l = 1 ∨ l = 2 := by omega
      rcases hcase with h0 | h1 | h2
      · rw [h0] at h; omega
      · rw [h1] at h; omega
      · rw [h2] at h; omega
    · have hbound : 3 * l ≤ l * l :=
        Int.mul_le_mul_of_nonneg_right hge3 (by omega)
      omega

/-- The raw inverse followed by the raw cat map is exactly the identity on the
integer plane: `[[1,-1],[-1,2]] · [[2,1],[1,1]] = I`, witnessed pointwise. -/
theorem catRawInv_catRaw (p : Point) : catRawInv (catRaw p) = p := by
  cases p with
  | mk x y =>
    show ((2 * x + y) - (x + y), -(2 * x + y) + 2 * (x + y)) = (x, y)
    rw [Prod.mk.injEq]
    constructor <;> omega

/-- The raw cat map followed by its raw inverse is exactly the identity on the
integer plane. -/
theorem catRaw_catRawInv (p : Point) : catRaw (catRawInv p) = p := by
  cases p with
  | mk x y =>
    show (2 * (x - y) + (-x + 2 * y), (x - y) + (-x + 2 * y)) = (x, y)
    rw [Prod.mk.injEq]
    constructor <;> omega

/-- The raw cat map respects torus-address equivalence: the image lattice
witnesses are the matrix action on the input witnesses. -/
theorem catRaw_respects (N : Int) {p q : Point}
    (h : TorusRel N p q) : TorusRel N (catRaw p) (catRaw q) := by
  rcases h with ⟨⟨kx, hx⟩, ⟨ky, hy⟩⟩
  refine ⟨⟨2 * kx + ky, ?_⟩, ⟨kx + ky, ?_⟩⟩
  · have hb1 := Int.add_mul (2 * kx) ky N
    have hb2 := Int.mul_assoc 2 kx N
    show (2 * p.1 + p.2) - (2 * q.1 + q.2) = (2 * kx + ky) * N
    omega
  · have hb := Int.add_mul kx ky N
    show (p.1 + p.2) - (q.1 + q.2) = (kx + ky) * N
    omega

/-- The raw inverse map respects torus-address equivalence. -/
theorem catRawInv_respects (N : Int) {p q : Point}
    (h : TorusRel N p q) : TorusRel N (catRawInv p) (catRawInv q) := by
  rcases h with ⟨⟨kx, hx⟩, ⟨ky, hy⟩⟩
  refine ⟨⟨kx - ky, ?_⟩, ⟨-kx + 2 * ky, ?_⟩⟩
  · have hb := Int.sub_mul kx ky N
    show (p.1 - p.2) - (q.1 - q.2) = (kx - ky) * N
    omega
  · have hb1 := Int.add_mul (-kx) (2 * ky) N
    have hb2 := Int.neg_mul kx N
    have hb3 := Int.mul_assoc 2 ky N
    show (-p.1 + 2 * p.2) - (-q.1 + 2 * q.2) = (-kx + 2 * ky) * N
    omega

/-- The exact cat-map automorphism on the quotient torus, well defined by
`catRaw_respects` through `Quot.sound`. -/
def torusCat (N : Int) : Torus N → Torus N :=
  Quot.lift (fun p : Point => torusMk N (catRaw p))
    (fun _ _ h => Quot.sound (catRaw_respects N h))

/-- The exact inverse automorphism on the quotient torus. -/
def torusCatInv (N : Int) : Torus N → Torus N :=
  Quot.lift (fun p : Point => torusMk N (catRawInv p))
    (fun _ _ h => Quot.sound (catRawInv_respects N h))

/-- The inverse automorphism cancels the cat-map automorphism on the quotient
torus. -/
theorem torusCatInv_torusCat (N : Int) (z : Torus N) :
    torusCatInv N (torusCat N z) = z := by
  refine Quot.inductionOn z ?_
  intro p
  show torusMk N (catRawInv (catRaw p)) = torusMk N p
  rw [catRawInv_catRaw]

/-- The cat-map automorphism cancels its inverse on the quotient torus. -/
theorem torusCat_torusCatInv (N : Int) (z : Torus N) :
    torusCat N (torusCatInv N z) = z := by
  refine Quot.inductionOn z ?_
  intro p
  show torusMk N (catRaw (catRawInv p)) = torusMk N p
  rw [catRaw_catRawInv]

/-- Injectivity of the exact quotient cat map. -/
theorem torusCat_injective (N : Int) {z₁ z₂ : Torus N}
    (h : torusCat N z₁ = torusCat N z₂) : z₁ = z₂ := by
  rw [← torusCatInv_torusCat N z₁, ← torusCatInv_torusCat N z₂, h]

/-- Surjectivity of the exact quotient cat map: the preimage is the inverse
automorphism applied to the target. -/
theorem torusCat_surjective (N : Int) (z : Torus N) :
    ∃ pre : Torus N, torusCat N pre = z :=
  ⟨torusCatInv N z, torusCat_torusCatInv N z⟩

/-! ### Quotient exactness: address equality decides congruence (CL-CH04)

`Quot.sound` gives congruence → address equality. The converse — address
equality → congruence — is proved by lifting the relation itself along the
quotient, which is only possible because `TorusRel` is an equivalence. With
the κ coordinate decision above, torus-address equality is therefore decided
by comparing canonical forms. -/

/-- Quotient exactness: equal torus addresses are congruent representatives. -/
theorem torusMk_exact (N : Int) {p q : Point}
    (h : torusMk N p = torusMk N q) : TorusRel N p q := by
  have lift_ok : ∀ a b : Point,
      TorusRel N a b → TorusRel N p a = TorusRel N p b := by
    intro a b hab
    exact propext ⟨fun hpa => torusRel_trans N hpa hab,
                   fun hpb => torusRel_trans N hpb (torusRel_symm N hab)⟩
  have hpp : TorusRel N p p = TorusRel N p q :=
    congrArg (Quot.lift (TorusRel N p) lift_ok) h
  exact hpp ▸ torusRel_refl N p

/-- **CL-CH04 — address equality is congruence, both directions.** -/
theorem torusMk_eq_iff (N : Int) (p q : Point) :
    torusMk N p = torusMk N q ↔ TorusRel N p q :=
  ⟨torusMk_exact N, fun h => Quot.sound h⟩

/-! ## 2. Canonical representatives and exact phase confinement -/

/-- Canonicalize one coordinate by exact integer remainder. -/
def canon (N : Int) (x : Int) : Int :=
  x % N

/-- Canonicalize both coordinates. -/
def projectPhase (N : Int) (p : Point) : Point :=
  (canon N p.1, canon N p.2)

/-- The canonical Arnold cat map on representatives:
`(x,y) ↦ (2x+y, x+y) mod N`. -/
def catMap (N : Int) (p : Point) : Point :=
  projectPhase N (catRaw p)

/-- Core bounding utility: exact integer remainder by a positive modulus lands
in `[0,N)`. -/
theorem phase_bound (x N : Int) (hN : 0 < N) :
    0 ≤ canon N x ∧ canon N x < N := by
  unfold canon
  exact ⟨Int.emod_nonneg x (by omega), Int.emod_lt_of_pos x hN⟩

/-- Canonicalization always returns a representative inside the phase box. -/
theorem projectPhase_closed (N : Int) (hN : 0 < N) (p : Point) :
    InPhaseSpace N (projectPhase N p) := by
  have hx := phase_bound p.1 N hN
  have hy := phase_bound p.2 N hN
  exact ⟨hx.1, hx.2, hy.1, hy.2⟩

/-- The chaotic transition map strictly preserves the canonical phase box:
because it canonicalizes by exact integer remainder, its output is in the
phase box for any input representative. -/
theorem catMap_closed (N : Int) (hN : 0 < N) (p : Point) :
    InPhaseSpace N (catMap N p) :=
  projectPhase_closed N hN (catRaw p)

/-- Canonicalization does not move the torus address: a representative and its
canonical form are congruent. -/
theorem projectPhase_torusRel (N : Int) (p : Point) :
    TorusRel N (projectPhase N p) p := by
  constructor
  · exact emod_eq_congruent (by
      show p.1 % N % N = p.1 % N
      exact Int.emod_emod_of_dvd p.1 (Int.dvd_refl N))
  · exact emod_eq_congruent (by
      show p.2 % N % N = p.2 % N
      exact Int.emod_emod_of_dvd p.2 (Int.dvd_refl N))

/-- Canonicalization is invisible at the address level. -/
theorem torusMk_projectPhase (N : Int) (p : Point) :
    torusMk N (projectPhase N p) = torusMk N p :=
  Quot.sound (projectPhase_torusRel N p)

/-- Canonicalization is idempotent: the canonical form of a canonical form is
itself. -/
theorem projectPhase_idempotent (N : Int) (p : Point) :
    projectPhase N (projectPhase N p) = projectPhase N p := by
  show (p.1 % N % N, p.2 % N % N) = (p.1 % N, p.2 % N)
  rw [Prod.mk.injEq]
  exact ⟨Int.emod_emod_of_dvd p.1 (Int.dvd_refl N),
         Int.emod_emod_of_dvd p.2 (Int.dvd_refl N)⟩

/-- **CL-CH04 — the κ decision, point form.** Two representatives name the
same torus address iff their canonical forms are equal, for every modulus. -/
theorem torusRel_iff_projectPhase_eq (N : Int) (p q : Point) :
    TorusRel N p q ↔ projectPhase N p = projectPhase N q := by
  constructor
  · intro ⟨h1, h2⟩
    show (p.1 % N, p.2 % N) = (q.1 % N, q.2 % N)
    rw [Prod.mk.injEq]
    exact ⟨congruent_emod_eq h1, congruent_emod_eq h2⟩
  · intro h
    have h' : (p.1 % N, p.2 % N) = (q.1 % N, q.2 % N) := h
    rw [Prod.mk.injEq] at h'
    exact ⟨emod_eq_congruent h'.1, emod_eq_congruent h'.2⟩

/-- **CL-CH04 — address equality is decided by canonical forms.** The
composite of quotient exactness and the κ decision: `torusMk N p = torusMk N q`
iff `projectPhase N p = projectPhase N q`, an equality of exact integers. -/
theorem torusMk_eq_iff_canon (N : Int) (p q : Point) :
    torusMk N p = torusMk N q ↔ projectPhase N p = projectPhase N q :=
  (torusMk_eq_iff N p q).trans (torusRel_iff_projectPhase_eq N p q)

/-- **CL-CH04 — the phase box is a strict fundamental domain.** Congruent
canonical representatives are equal: each torus address has at most one
representative in `[0,N) × [0,N)`. (Existence of the representative is the
separate theorem `projectPhase_closed` with `torusMk_projectPhase`, and needs
`0 < N`; uniqueness, proved here, needs no positivity hypothesis because the
box is empty otherwise.) -/
theorem phase_box_unique (N : Int) {p q : Point}
    (hp : InPhaseSpace N p) (hq : InPhaseSpace N q)
    (h : TorusRel N p q) : p = q := by
  obtain ⟨h1, h2⟩ := h
  obtain ⟨hp1, hp2, hp3, hp4⟩ := hp
  obtain ⟨hq1, hq2, hq3, hq4⟩ := hq
  have e1 : p.1 % N = q.1 % N := congruent_emod_eq h1
  have e2 : p.2 % N = q.2 % N := congruent_emod_eq h2
  have r1 : p.1 % N = p.1 := Int.emod_eq_of_lt hp1 hp2
  have r2 : q.1 % N = q.1 := Int.emod_eq_of_lt hq1 hq2
  have r3 : p.2 % N = p.2 := Int.emod_eq_of_lt hp3 hp4
  have r4 : q.2 % N = q.2 := Int.emod_eq_of_lt hq3 hq4
  cases p with
  | mk px py =>
    cases q with
    | mk qx qy =>
      rw [Prod.mk.injEq]
      constructor <;> omega

/-! ## 3. Exact representative dynamics and semantic pinning -/

/-- The canonical representative orbit at discrete time `t`. There is no
numerical integration and no floating step: this is repeated exact integer
application of `catMap`. -/
def orbit (N : Int) (start : Point) : Nat → Point
  | 0 => start
  | Nat.succ t => catMap N (orbit N start t)

/-- Computation rule: time zero returns the starting representative. -/
theorem orbit_zero (N : Int) (start : Point) :
    orbit N start 0 = start := rfl

/-- Computation rule: a successor time applies one exact cat-map step. -/
theorem orbit_succ (N : Int) (start : Point) (t : Nat) :
    orbit N start (Nat.succ t) = catMap N (orbit N start t) := rfl

/-- **CL-CH02 — the two computation rules characterize `orbit` uniquely.**
The codec-invariance theorems below therefore transport this pinned exact
evolution, not an unconstrained function of the inputs. -/
theorem orbit_unique (N : Int) (F : Point → Nat → Point)
    (h0 : ∀ start, F start 0 = start)
    (hs : ∀ start t, F start (Nat.succ t) = catMap N (F start t)) :
    ∀ start t, F start t = orbit N start t := by
  intro start t
  induction t with
  | zero => rw [h0, orbit_zero]
  | succ t ih => rw [hs, orbit_succ, ih]

/-- **CL-CH02 — exact flow law.** Evolving for `s + t` steps is the same as
evolving for `s` steps and then for `t` more steps. -/
theorem orbit_add (N : Int) (start : Point) (s t : Nat) :
    orbit N start (s + t) = orbit N (orbit N start s) t := by
  induction t with
  | zero => rfl
  | succ t ih =>
    calc
      orbit N start (s + Nat.succ t)
          = orbit N start (Nat.succ (s + t)) := by rw [Nat.add_succ]
      _ = catMap N (orbit N start (s + t)) := by rw [orbit_succ]
      _ = catMap N (orbit N (orbit N start s) t) := by rw [ih]
      _ = orbit N (orbit N start s) (Nat.succ t) := by rw [orbit_succ]

/-- **CL-CH03 — exact phase confinement.** If the initial representative is
canonical and `0 < N`, every discrete-time state remains canonical. -/
theorem orbit_bounded (N : Int) (hN : 0 < N) (start : Point)
    (hStart : InPhaseSpace N start) (t : Nat) :
    InPhaseSpace N (orbit N start t) := by
  induction t with
  | zero => exact hStart
  | succ t _ =>
    rw [orbit_succ]
    exact catMap_closed N hN (orbit N start t)

/-- Even from a noncanonical raw representative, after one exact cat-map step
the orbit is canonical, and stays so. -/
theorem orbit_after_step_bounded (N : Int) (hN : 0 < N)
    (start : Point) (t : Nat) :
    InPhaseSpace N (orbit N start (Nat.succ t)) := by
  rw [orbit_succ]
  exact catMap_closed N hN (orbit N start t)

/-- A decoded initial condition that is canonical stays canonical under exact
chaotic evolution. -/
theorem decoded_orbit_bounded {Code : Type} (N : Int) (hN : 0 < N)
    (d : Code → Point) (c : Code)
    (hStart : InPhaseSpace N (decodedState d c)) (t : Nat) :
    InPhaseSpace N (orbit N (decodedState d c) t) :=
  orbit_bounded N hN (decodedState d c) hStart t

/-! ## 4. Codec-invariance for exact chaotic flow (CL-CH01)

These are congruences — well-definedness of the exact evolution on decoded
initial data — and a congruence alone would hold for any function of the
inputs. They are anchored to the real dynamics by `orbit_unique` /
`torusOrbit_unique` (CL-CH02): what is transported is the uniquely pinned
exact cat-map evolution. -/

/-- **CL-CH01 — representative orbit codec-invariance.** If two codecs decode
to the same exact representative, their exact chaotic trajectories are
identical at every discrete time `t`. The result depends on the decoded state
and the exact map, not on the storage tier or hardware substrate. -/
theorem orbit_invariance {C₁ C₂ : Type} (N : Int) (t : Nat)
    (d₁ : C₁ → Point) (c₁ : C₁)
    (d₂ : C₂ → Point) (c₂ : C₂)
    (h : decodedState d₁ c₁ = decodedState d₂ c₂) :
    orbit N (decodedState d₁ c₁) t = orbit N (decodedState d₂ c₂) t := by
  rw [h]

/-- **CL-CH01 — exact representative transcoding.** Re-encoding initial sensor
data through a code map `e` is invisible to the exact orbit when decoding is
composed: `d (e c)` and `(d ∘ e) c` are definitionally the same state. -/
theorem transcode_orbit_invariance {C₁ C₂ : Type} (N : Int) (t : Nat)
    (e : C₁ → C₂) (d : C₂ → Point) (c : C₁) :
    orbit N (decodedState d (e c)) t
      = orbit N (decodedState (d ∘ e) c) t :=
  rfl

/-! ## 5. The quotient dynamics: codec-invariance, realization, reversal -/

/-- The quotient-torus orbit at discrete time `t`. This is the same exact
dynamics, but stated directly on modulo-`N` torus addresses rather than on a
chosen canonical representative. -/
def torusOrbit (N : Int) (start : Torus N) : Nat → Torus N
  | 0 => start
  | Nat.succ t => torusCat N (torusOrbit N start t)

/-- Computation rule: quotient orbit at time zero. -/
theorem torusOrbit_zero (N : Int) (start : Torus N) :
    torusOrbit N start 0 = start := rfl

/-- Computation rule: quotient orbit at successor time. -/
theorem torusOrbit_succ (N : Int) (start : Torus N) (t : Nat) :
    torusOrbit N start (Nat.succ t) = torusCat N (torusOrbit N start t) := rfl

/-- **CL-CH02 — the quotient orbit is uniquely characterized** by its zero and
successor rules. -/
theorem torusOrbit_unique (N : Int) (F : Torus N → Nat → Torus N)
    (h0 : ∀ start, F start 0 = start)
    (hs : ∀ start t, F start (Nat.succ t) = torusCat N (F start t)) :
    ∀ start t, F start t = torusOrbit N start t := by
  intro start t
  induction t with
  | zero => rw [h0, torusOrbit_zero]
  | succ t ih => rw [hs, torusOrbit_succ, ih]

/-- **CL-CH02 — exact flow law on the quotient.** -/
theorem torusOrbit_add (N : Int) (start : Torus N) (s t : Nat) :
    torusOrbit N start (s + t) = torusOrbit N (torusOrbit N start s) t := by
  induction t with
  | zero => rfl
  | succ t ih =>
    calc
      torusOrbit N start (s + Nat.succ t)
          = torusOrbit N start (Nat.succ (s + t)) := by rw [Nat.add_succ]
      _ = torusCat N (torusOrbit N start (s + t)) := by rw [torusOrbit_succ]
      _ = torusCat N (torusOrbit N (torusOrbit N start s) t) := by rw [ih]
      _ = torusOrbit N (torusOrbit N start s) (Nat.succ t) := by
            rw [torusOrbit_succ]

/-- **CL-CH01 — quotient orbit codec-invariance.** If two codecs decode to
the same modulo-`N` torus address, their exact quotient trajectories agree at
every discrete time, even if the raw representatives differ by period-lattice
translations. -/
theorem torus_orbit_invariance {C₁ C₂ : Type} (N : Int) (t : Nat)
    (d₁ : C₁ → Point) (c₁ : C₁)
    (d₂ : C₂ → Point) (c₂ : C₂)
    (h : decodedTorusState N d₁ c₁ = decodedTorusState N d₂ c₂) :
    torusOrbit N (decodedTorusState N d₁ c₁) t
      = torusOrbit N (decodedTorusState N d₂ c₂) t := by
  rw [h]

/-- **CL-CH01 — exact quotient transcoding.** Transcoding is invisible at the
torus-address level: `d (e c)` and `(d ∘ e) c` name the same quotient state by
definition. -/
theorem torus_transcode_orbit_invariance {C₁ C₂ : Type} (N : Int) (t : Nat)
    (e : C₁ → C₂) (d : C₂ → Point) (c : C₁) :
    torusOrbit N (decodedTorusState N d (e c)) t
      = torusOrbit N (decodedTorusState N (d ∘ e) c) t :=
  rfl

/-! ### CL-CH04 — the representative dynamics realizes the quotient
automorphism

The discrete analogue of the matmul file's machine-realization theorem: the
`mod-N` canonical-representative orbit, read through `torusMk`, *is* the
quotient orbit. The canonicalization step is exactly invisible — not
approximately, and not by convention. -/

/-- One canonical cat-map step realizes one quotient automorphism step. -/
theorem catMap_realizes (N : Int) (p : Point) :
    torusMk N (catMap N p) = torusCat N (torusMk N p) := by
  show torusMk N (projectPhase N (catRaw p)) = torusCat N (torusMk N p)
  rw [torusMk_projectPhase]
  rfl

/-- **CL-CH04 — realization at every time.** The canonical representative
orbit, viewed as a torus address, is the quotient orbit of the initial
address: `mod-N` iteration on representatives and abstract automorphism
iteration on the quotient are the same exact dynamics. -/
theorem orbit_realizes (N : Int) (start : Point) (t : Nat) :
    torusMk N (orbit N start t) = torusOrbit N (torusMk N start) t := by
  induction t with
  | zero => rfl
  | succ t ih =>
    rw [orbit_succ, catMap_realizes, ih, torusOrbit_succ]

/-- Congruent starting representatives stay congruent at every time: the
representative dynamics descends to the quotient coherently. -/
theorem orbit_congruent (N : Int) {s₁ s₂ : Point}
    (h : TorusRel N s₁ s₂) (t : Nat) :
    TorusRel N (orbit N s₁ t) (orbit N s₂ t) := by
  apply torusMk_exact N
  have hmk : torusMk N s₁ = torusMk N s₂ := Quot.sound h
  rw [orbit_realizes, orbit_realizes, hmk]

/-- **CL-CH04 — canonical determinism.** Congruent *canonical* starting
representatives have literally equal orbits at every time: within the
fundamental domain, the torus address determines the entire exact trajectory
pointwise. -/
theorem orbit_canonical_eq (N : Int) (hN : 0 < N) {s₁ s₂ : Point}
    (h : TorusRel N s₁ s₂)
    (h₁ : InPhaseSpace N s₁) (h₂ : InPhaseSpace N s₂) (t : Nat) :
    orbit N s₁ t = orbit N s₂ t :=
  phase_box_unique N (orbit_bounded N hN s₁ h₁ t)
    (orbit_bounded N hN s₂ h₂ t) (orbit_congruent N h t)

/-- One exact cat-map step is injective on the phase box: canonical
representatives with equal images are equal. No positivity hypothesis is
needed — a canonical representative can only exist when `0 < N`. -/
theorem catMap_box_injective (N : Int) {p q : Point}
    (hp : InPhaseSpace N p) (hq : InPhaseSpace N q)
    (h : catMap N p = catMap N q) : p = q := by
  have haddr : torusMk N p = torusMk N q := by
    apply torusCat_injective N
    show torusCat N (torusMk N p) = torusCat N (torusMk N q)
    rw [← catMap_realizes, ← catMap_realizes, h]
  exact phase_box_unique N hp hq (torusMk_exact N haddr)

/-- One exact cat-map step is surjective onto the phase box: every canonical
representative has a canonical preimage, obtained by canonicalizing the raw
inverse. With `catMap_box_injective`, the exact cat map is a bijection of the
finite phase box — the representative-level driftless automorphism. -/
theorem catMap_box_surjective (N : Int) (hN : 0 < N) {w : Point}
    (hw : InPhaseSpace N w) :
    ∃ p : Point, InPhaseSpace N p ∧ catMap N p = w := by
  refine ⟨projectPhase N (catRawInv w), projectPhase_closed N hN _, ?_⟩
  have haddr : torusMk N (catMap N (projectPhase N (catRawInv w)))
      = torusMk N w := by
    rw [catMap_realizes, torusMk_projectPhase]
    show torusMk N (catRaw (catRawInv w)) = torusMk N w
    rw [catRaw_catRawInv]
  exact phase_box_unique N
    (catMap_closed N hN (projectPhase N (catRawInv w))) hw
    (torusMk_exact N haddr)

/-! ### CL-CH05 — full reversal: the `t`-step evolution is a bijection -/

/-- The exact rewind: iterate the inverse automorphism `t` times. Defined
tail-first so that one rewind step cancels the outermost forward step. -/
def torusRewind (N : Int) (w : Torus N) : Nat → Torus N
  | 0 => w
  | Nat.succ t => torusRewind N (torusCatInv N w) t

/-- **CL-CH05 — full left reversal.** Rewinding `t` steps after evolving `t`
steps returns the initial address exactly, for every `t`. No information is
lost at any time depth: the dynamics is driftless in the strongest sense. -/
theorem torusRewind_torusOrbit (N : Int) (t : Nat) :
    ∀ z : Torus N, torusRewind N (torusOrbit N z t) t = z := by
  induction t with
  | zero => intro z; rfl
  | succ t ih =>
    intro z
    show torusRewind N (torusCatInv N (torusOrbit N z (Nat.succ t))) t = z
    rw [torusOrbit_succ, torusCatInv_torusCat]
    exact ih z

/-- **CL-CH05 — full right reversal.** Evolving `t` steps from a rewound
address returns the original address: rewind is a two-sided inverse of the
`t`-step evolution. -/
theorem torusOrbit_torusRewind (N : Int) (t : Nat) :
    ∀ w : Torus N, torusOrbit N (torusRewind N w t) t = w := by
  induction t with
  | zero => intro w; rfl
  | succ t ih =>
    intro w
    show torusCat N (torusOrbit N (torusRewind N (torusCatInv N w) t) t) = w
    rw [ih (torusCatInv N w), torusCat_torusCatInv]

/-- **CL-CH05 — the `t`-step evolution is injective for every `t`.** -/
theorem torusOrbit_injective (N : Int) (t : Nat) {z₁ z₂ : Torus N}
    (h : torusOrbit N z₁ t = torusOrbit N z₂ t) : z₁ = z₂ := by
  rw [← torusRewind_torusOrbit N t z₁, ← torusRewind_torusOrbit N t z₂, h]

/-- **CL-CH05 — the `t`-step evolution is surjective for every `t`.** -/
theorem torusOrbit_surjective (N : Int) (t : Nat) (w : Torus N) :
    ∃ z : Torus N, torusOrbit N z t = w :=
  ⟨torusRewind N w t, torusOrbit_torusRewind N t w⟩

/-- The quotient cat-map dynamics is reversible at every time by applying the
inverse automorphism to a successor state: the one-step instance of the full
reversal. -/
theorem torusOrbit_step_reversible (N : Int) (start : Torus N) (t : Nat) :
    torusCatInv N (torusOrbit N start (Nat.succ t))
      = torusOrbit N start t := by
  rw [torusOrbit_succ, torusCatInv_torusCat]

/-- **CL-CH05 — collision transports to a period.** If the exact quotient
orbit ever revisits a state (`torusOrbit N z s = torusOrbit N z t`, `s ≤ t`),
the initial address itself is periodic with period `t − s` (nontrivial
whenever `s < t`). Combined with finiteness of the torus for `N ≠ 0` — not
formalized here — this would give periodicity of every address by pigeonhole;
the transport step proved here is the part that fails for lossy floating
simulation, where collisions of rounded states carry no information about the
true orbit. -/
theorem torusOrbit_collision_period (N : Int) (z : Torus N) {s t : Nat}
    (hle : s ≤ t) (h : torusOrbit N z s = torusOrbit N z t) :
    torusOrbit N z (t - s) = z := by
  have hsum : s + (t - s) = t := by omega
  have hsum' : (t - s) + s = t := by omega
  have h1 : torusOrbit N z t = torusOrbit N (torusOrbit N z s) (t - s) := by
    calc torusOrbit N z t
        = torusOrbit N z (s + (t - s)) := by rw [hsum]
      _ = torusOrbit N (torusOrbit N z s) (t - s) := torusOrbit_add N z s (t - s)
  have h2 : torusOrbit N (torusOrbit N z (t - s)) s
      = torusOrbit N (torusOrbit N z s) (t - s) := by
    calc torusOrbit N (torusOrbit N z (t - s)) s
        = torusOrbit N z ((t - s) + s) := (torusOrbit_add N z (t - s) s).symm
      _ = torusOrbit N z t := by rw [hsum']
      _ = torusOrbit N z (s + (t - s)) := by rw [hsum]
      _ = torusOrbit N (torusOrbit N z s) (t - s) := torusOrbit_add N z s (t - s)
  have h3 : torusOrbit N (torusOrbit N z (t - s)) s = torusOrbit N z s := by
    rw [h2, ← h1, ← h]
  exact torusOrbit_injective N s h3

/-! ## 6. Exact hyperbolic sensitivity on the linear lift (CL-CH06)

The raw map is linear, so the difference of two lifted trajectories is itself
a trajectory of the difference. A unit initial difference `(1,0)` then grows
at least exponentially: `2ᵗ ≤ Δx(t)`, an exact integer inequality with no
float and no limit. This is the sensitive-dependence half of chaos, stated
where it is unconditionally true — on the lift; on the finite torus the same
map acts by the driftless automorphism proved above. -/

/-- Coordinatewise difference of two states. -/
def psub (p q : Point) : Point :=
  (p.1 - q.1, p.2 - q.2)

/-- The raw cat map is linear: it commutes with state differences exactly. -/
theorem catRaw_psub (p q : Point) :
    catRaw (psub p q) = psub (catRaw p) (catRaw q) := by
  cases p with
  | mk px py =>
    cases q with
    | mk qx qy =>
      show (2 * (px - qx) + (py - qy), (px - qx) + (py - qy))
          = ((2 * px + py) - (2 * qx + qy), (px + py) - (qx + qy))
      rw [Prod.mk.injEq]
      constructor <;> omega

/-- The raw (unreduced) orbit on the integer plane: repeated exact matrix
action, no canonicalization. This is the linear lift of the torus dynamics. -/
def rawOrbit (start : Point) : Nat → Point
  | 0 => start
  | Nat.succ t => catRaw (rawOrbit start t)

/-- The lift of a difference evolves as the difference of the lifts: exact
linearity of the raw dynamics at every time. -/
theorem rawOrbit_psub (p q : Point) (t : Nat) :
    rawOrbit (psub p q) t = psub (rawOrbit p t) (rawOrbit q t) := by
  induction t with
  | zero => rfl
  | succ t ih =>
    show catRaw (rawOrbit (psub p q) t)
        = psub (catRaw (rawOrbit p t)) (catRaw (rawOrbit q t))
    rw [ih, catRaw_psub]

/-- Positivity of the doubling scale: `1 ≤ 2ᵗ` over `ℤ`, by induction. -/
theorem one_le_two_pow (t : Nat) : (1 : Int) ≤ 2 ^ t := by
  induction t with
  | zero => decide
  | succ t ih =>
    have hpow := Int.pow_succ 2 t
    omega

/-- **CL-CH06 — exact exponential expansion.** From the unit difference
`(1,0)`, the first coordinate of the raw orbit is at least `2ᵗ` (and the
second stays nonnegative) at every time: the expanding cone of the hyperbolic
matrix, witnessed by exact integer inequalities. -/
theorem rawOrbit_expansion (t : Nat) :
    (2 : Int) ^ t ≤ (rawOrbit (1, 0) t).1 ∧ 0 ≤ (rawOrbit (1, 0) t).2 := by
  induction t with
  | zero => exact ⟨by decide, by decide⟩
  | succ t ih =>
    obtain ⟨hx, hy⟩ := ih
    have hpow := Int.pow_succ 2 t
    have hone := one_le_two_pow t
    show (2 : Int) ^ (t + 1) ≤ 2 * (rawOrbit (1, 0) t).1 + (rawOrbit (1, 0) t).2
        ∧ 0 ≤ (rawOrbit (1, 0) t).1 + (rawOrbit (1, 0) t).2
    constructor <;> omega

/-- **CL-CH06 — exact sensitivity to initial conditions.** Two lifted
trajectories whose initial states differ by the unit vector `(1,0)` separate
at least exponentially: `2ᵗ ≤ Δx(t)` exactly, for every `t`. Sensitivity is a
theorem of the integer dynamics, not an artifact of floating rounding. -/
theorem exact_sensitivity (p q : Point) (h : psub p q = (1, 0)) (t : Nat) :
    (2 : Int) ^ t ≤ (psub (rawOrbit p t) (rawOrbit q t)).1 := by
  rw [← rawOrbit_psub, h]
  exact (rawOrbit_expansion t).1

/-- **CL-CH06 — the lift has infinite order.** The raw orbit of `(1,0)` never
returns: exponential expansion excludes recurrence upstairs for this orbit.
Any recurrence of it can therefore only occur on the quotient; existence
there (for `N ≠ 0`, by finiteness) is deliberately left unformalized — see
the module header. -/
theorem catRaw_infinite_order (t : Nat)
    (h : rawOrbit (1, 0) t = (1, 0)) : t = 0 := by
  cases t with
  | zero => rfl
  | succ s =>
    exfalso
    have hexp := (rawOrbit_expansion (Nat.succ s)).1
    rw [h] at hexp
    have hexp' : (2 : Int) ^ (s + 1) ≤ 1 := hexp
    have hone := one_le_two_pow s
    have hpow := Int.pow_succ 2 s
    omega

end UorChaos

/-! ## 7. Audit — the F1 honesty contract, embedded

`#guard` re-evaluates concrete dynamics at elaboration time: one exact
cat-map step, a three-step orbit, the raw inverse cancelling the raw map on
a sample point, the κ decision on a congruent pair, and the Fibonacci growth
of the raw lift (`rawOrbit (1,0) 5 = (89, 55)`, the fifth power of the
matrix).
`#print axioms` displays the
exact axiom footprint of every theorem in the build log. Expected: every
theorem reports axioms ⊆ `{propext, Quot.sound}`. Thirteen report none — the
seven `decide`-proved matrix pins (`catA_eq`, `catB_eq`, `catC_eq`,
`catD_eq`, `catDet_eq_one`, `catTrace_eq_three`, `cat_hyperbolic_signature`)
and the six representative-level theorems whose rewrites are definitional
(`orbit_zero`, `orbit_succ`, `orbit_unique`, `orbit_add`, `orbit_invariance`,
`transcode_orbit_invariance`); `projectPhase_idempotent` reports `propext`
alone; the remaining fifty-four report `{propext, Quot.sound}`, by two
distinct routes that this audit distinguishes. For the quotient-level
theorems, `Quot.sound` is the mathematical content: everything mentioning
`torusMk` / `torusCat` / `Torus` inherits the well-definedness witness in the
lifted map's definition. For the pure integer lemmas among the fifty-four
(the `Congruent`/`TorusRel` algebra, the raw-map identities and sensitivity
chain, `phase_bound`, `discriminant_not_square`, `cat_no_integer_eigenvalue`,
`catRaw_matrix_action`, `one_le_two_pow`), no quotient appears anywhere:
there `Quot.sound` enters incidentally, through the core arithmetic lemmas
`omega` and the `Int` library elaborate with. Anything else — in particular
`sorryAx` or `Classical.choice` — is a build failure of the discipline, even
if Lean accepts the file. -/

#guard UorChaos.catMap 5 (3, 2) = (3, 0)
#guard UorChaos.orbit 5 (1, 0) 3 = (3, 3)
#guard UorChaos.catRawInv (UorChaos.catRaw (7, -4)) = (7, -4)
#guard UorChaos.projectPhase 5 (12, -3) = UorChaos.projectPhase 5 (2, 7)
#guard UorChaos.rawOrbit (1, 0) 5 = (89, 55)

#print axioms UorChaos.torusRel_refl
#print axioms UorChaos.torusRel_symm
#print axioms UorChaos.torusRel_trans
#print axioms UorChaos.congruent_emod_eq
#print axioms UorChaos.emod_eq_congruent
#print axioms UorChaos.congruent_iff_emod_eq
#print axioms UorChaos.catA_eq
#print axioms UorChaos.catB_eq
#print axioms UorChaos.catC_eq
#print axioms UorChaos.catD_eq
#print axioms UorChaos.catRaw_matrix_action
#print axioms UorChaos.catDet_eq_one
#print axioms UorChaos.catTrace_eq_three
#print axioms UorChaos.cat_hyperbolic_signature
#print axioms UorChaos.discriminant_not_square
#print axioms UorChaos.cat_no_integer_eigenvalue
#print axioms UorChaos.catRawInv_catRaw
#print axioms UorChaos.catRaw_catRawInv
#print axioms UorChaos.catRaw_respects
#print axioms UorChaos.catRawInv_respects
#print axioms UorChaos.torusCatInv_torusCat
#print axioms UorChaos.torusCat_torusCatInv
#print axioms UorChaos.torusCat_injective
#print axioms UorChaos.torusCat_surjective
#print axioms UorChaos.torusMk_exact
#print axioms UorChaos.torusMk_eq_iff
#print axioms UorChaos.phase_bound
#print axioms UorChaos.projectPhase_closed
#print axioms UorChaos.catMap_closed
#print axioms UorChaos.projectPhase_torusRel
#print axioms UorChaos.torusMk_projectPhase
#print axioms UorChaos.projectPhase_idempotent
#print axioms UorChaos.torusRel_iff_projectPhase_eq
#print axioms UorChaos.torusMk_eq_iff_canon
#print axioms UorChaos.phase_box_unique
#print axioms UorChaos.orbit_zero
#print axioms UorChaos.orbit_succ
#print axioms UorChaos.orbit_unique
#print axioms UorChaos.orbit_add
#print axioms UorChaos.orbit_bounded
#print axioms UorChaos.orbit_after_step_bounded
#print axioms UorChaos.decoded_orbit_bounded
#print axioms UorChaos.orbit_invariance
#print axioms UorChaos.transcode_orbit_invariance
#print axioms UorChaos.torusOrbit_zero
#print axioms UorChaos.torusOrbit_succ
#print axioms UorChaos.torusOrbit_unique
#print axioms UorChaos.torusOrbit_add
#print axioms UorChaos.torus_orbit_invariance
#print axioms UorChaos.torus_transcode_orbit_invariance
#print axioms UorChaos.catMap_realizes
#print axioms UorChaos.orbit_realizes
#print axioms UorChaos.orbit_congruent
#print axioms UorChaos.orbit_canonical_eq
#print axioms UorChaos.catMap_box_injective
#print axioms UorChaos.catMap_box_surjective
#print axioms UorChaos.torusRewind_torusOrbit
#print axioms UorChaos.torusOrbit_torusRewind
#print axioms UorChaos.torusOrbit_injective
#print axioms UorChaos.torusOrbit_surjective
#print axioms UorChaos.torusOrbit_step_reversible
#print axioms UorChaos.torusOrbit_collision_period
#print axioms UorChaos.catRaw_psub
#print axioms UorChaos.rawOrbit_psub
#print axioms UorChaos.one_le_two_pow
#print axioms UorChaos.rawOrbit_expansion
#print axioms UorChaos.exact_sensitivity
#print axioms UorChaos.catRaw_infinite_order