Two transverse shears with base-read offsets are the cat stroke up to a translation

Category: 7-SigmaLayer. BACKLOG #175 (out of #19 and #153): the narrowing brick for Posit 1's discharge.

#153 said what a hyperbolic de-isolation must do to the fibre: shear both coordinates, each reading the other (catStroke_eq_two_shears), where the constructed witness shearEvolve shears one coordinate by a base-read amount. The natural class that does both is two transverse coordinate-reading shears each carrying a base-read offset g₁, g₂ (whatever the base says at that base point):

shearXOff g₁ ∘ shearYOff g₂ = affineCat (g₁ + g₂, g₂),

an affine cat map x ↦ A x + c. CatMapAffine.lean shows every affine cat map is conjugate to the cat map by a translation of the fibre, so it is strongly mixing and its lift stretches at 2 log φ — the base-read offsets are invisible to #19's criterion (the de-isolation flow has a positive Lyapunov exponent on the fibre). What decides the criterion is the transverse pair, not what the base says; the choice #19 is about is between conjugacy classes of fibre maps.

• shearXOff, shearYOff — the two coordinate-reading shears with an offset; at offset 0 they are MeasureTheory.shearX, shearY (shearXOff_zero, shearYOff_zero);
• ★★ shearXOff_comp_shearYOff — two offset shears are the affine cat map affineCat (g₁+g₂, g₂);
• ★★★ mixing_shearXOff_comp_shearYOff, ergodic_shearXOff_comp_shearYOff, measurePreserving_shearXOff_comp_shearYOff — strongly mixing, for every pair of offsets;
• shearXOff_comp_shearYOff_coe, ★ lift_fderiv_hasLyapunovExponent — the lift's derivative is catR, exponent 2 log φ off the stable line, offsets or not;
• ★★★ fibre_affine_shears — the package, read against #19.

Honest scope

• ⚠️ Narrows, does not decide. One whole conjugacy class of candidate fibre maps — the affine cat maps, i.e. two transverse coordinate-reading shears with any base-read offsets — is shown to be dynamically the cat stroke. Which class nature uses stays #19; nothing here says the de-isolation is of this class.
• The offsets g₁, g₂ are real numbers, read as "what the base says at this base point"; the statement is pointwise in the base, as fibre_two_shears is. No base dependence is modelled.
• The cat matrix only, as in the whole line.

References: specs/BACKLOG.md #175, #19, #153, #147, #148; specs/POSITS.md Posit 1, Posit 10; SigmaLayer/FibreTwoShears.lean (qshift, catStroke_eq_two_shears, fibre_two_shears); Mathlib/Dynamics/CatMapAffine.lean (affineCat, affineCat_mixing, affineCatR_fderiv_hasLyapunovExponent); RecordLayer/ShearWitness.lean (pshift); RecordLayer/CircleFibre.lean (rep, coe_rep).

The two shears with offsets

noncomputable def CSD.SigmaLayer.shearXOff (g : ℝ) (x : LF4.KTorus) : LF4.KTorus

Shift the first fibre coordinate by the second plus an offset g.

Equations

• CSD.SigmaLayer.shearXOff g x = CSD.RecordLayer.pshift (CSD.RecordLayer.rep x.2 + g) x

noncomputable def CSD.SigmaLayer.shearYOff (g : ℝ) (x : LF4.KTorus) : LF4.KTorus

Shift the second fibre coordinate by the first plus an offset g.

Equations

• CSD.SigmaLayer.shearYOff g x = CSD.SigmaLayer.qshift (CSD.RecordLayer.rep x.1 + g) x

theorem CSD.SigmaLayer.shearXOff_apply (g : ℝ) (x : LF4.KTorus) : shearXOff g x = (x.1 + x.2 + ↑g, x.2)

theorem CSD.SigmaLayer.shearYOff_apply (g : ℝ) (x : LF4.KTorus) : shearYOff g x = (x.1, x.2 + x.1 + ↑g)

theorem CSD.SigmaLayer.shearXOff_zero : shearXOff 0 = MeasureTheory.shearX

theorem CSD.SigmaLayer.shearYOff_zero : shearYOff 0 = MeasureTheory.shearY

theorem CSD.SigmaLayer.shearXOff_comp_shearYOff (g₁ g₂ : ℝ) : shearXOff g₁ ∘ shearYOff g₂ = MeasureTheory.affineCat (↑(g₁ + g₂), ↑g₂)

★★ Two transverse coordinate-reading shears with offsets are the affine cat map x ↦ A x + (g₁ + g₂, g₂).

Mixing and the exponent, for every pair of offsets

theorem CSD.SigmaLayer.mixing_shearXOff_comp_shearYOff (g₁ g₂ : ℝ) : Mixing (shearXOff g₁ ∘ shearYOff g₂) MeasureTheory.volume

★★★ Two offset shears are strongly mixing, whatever the offsets.

theorem CSD.SigmaLayer.ergodic_shearXOff_comp_shearYOff (g₁ g₂ : ℝ) : Ergodic (shearXOff g₁ ∘ shearYOff g₂) MeasureTheory.volume

theorem CSD.SigmaLayer.measurePreserving_shearXOff_comp_shearYOff (g₁ g₂ : ℝ) : MeasureTheory.MeasurePreserving (shearXOff g₁ ∘ shearYOff g₂) MeasureTheory.volume MeasureTheory.volume

theorem CSD.SigmaLayer.shearXOff_comp_shearYOff_coe (g₁ g₂ x y : ℝ) : (shearXOff g₁ ∘ shearYOff g₂) (↑x, ↑y) = (↑(MeasureTheory.affineCatR (g₁ + g₂, g₂) (x, y)).1, ↑(MeasureTheory.affineCatR (g₁ + g₂, g₂) (x, y)).2)

The offset shears descend from the lift affineCatR (g₁ + g₂, g₂).

theorem CSD.SigmaLayer.lift_fderiv_hasLyapunovExponent (g₁ g₂ : ℝ) (v : ℝ × ℝ) {w : ℝ × ℝ} (hw : MeasureTheory.ellUR w ≠ 0) : HasLyapunovExponent (fderiv ℝ (MeasureTheory.affineCatR (g₁ + g₂, g₂)) v) w (2 * Real.log Real.goldenRatio)

★ The lift's derivative has exponent 2 log φ off the stable line: the offsets do not enter.

The package

theorem CSD.SigmaLayer.fibre_affine_shears (g₁ g₂ : ℝ) : shearXOff g₁ ∘ shearYOff g₂ = MeasureTheory.affineCat (↑(g₁ + g₂), ↑g₂) ∧ Mixing (shearXOff g₁ ∘ shearYOff g₂) MeasureTheory.volume ∧ ∀ (v w : ℝ × ℝ), MeasureTheory.ellUR w ≠ 0 → HasLyapunovExponent (fderiv ℝ (MeasureTheory.affineCatR (g₁ + g₂, g₂)) v) w (2 * Real.log Real.goldenRatio)

★★★ Two transverse coordinate-reading shears with base-read offsets are the cat stroke up to a translation of the fibre: they compose to the affine cat map A x + (g₁ + g₂, g₂), which is strongly mixing and whose lift stretches at 2 log φ off the stable line, for every pair of offsets. Read against #19's criterion: the base-read offsets are invisible to it; what decides it is the transverse pair. Which conjugacy class nature uses is BACKLOG #19.