The fibre carries both record coordinates: hyperbolicity needs the second coordinate sheared

Category: 7-SigmaLayer. BACKLOG #153 (out of #19 and #148); the structural reading of Posit 10 in its I3 form.

#148 put the corpus's two fibre maps on the two sides of one line: the hyperbolic witness catStroke stretches at 2 log φ, the constructed de-isolation witness shearEvolve stretches nothing (fibre_witnesses_lyapunov). This file says why, in terms of what each map does to the two coordinates of the fibre T² = KTorus.

• The constructed de-isolation moves one fibre coordinate by an amount read off the base: (shearEvolve idx s t x).2 = pshift (amount of the selector) x.2 (shearEvolve_snd), and the second fibre coordinate is untouched (★ shearEvolve_snd_snd). It is a pshift-type map.
• The hyperbolic stroke is two transverse pshift-type maps, each reading the other fibre coordinate: ★★ catStroke_eq_two_shears, catStroke = (shift the first coordinate by the second) ∘ (shift the second coordinate by the first) — shearX_eq_pshift, shearY_eq_qshift, where qshift is the transverse partner of pshift (measurePreserving_qshift).
• No single pshift-type map is the hyperbolic stroke (★ catStroke_ne_pshift_type): the stroke moves the second coordinate (catStroke_snd_ne), and a pshift-type map never does.
• Neither shear stretches on its own. Each factor's lift has Lyapunov exponent 0 in every direction (shearXR_fderiv_hasLyapunovExponent, shearYR_fderiv_hasLyapunovExponent) while the composition has exponent 2 log φ (catR_fderiv_hasLyapunovExponent). The stretching is produced by the transversality of the two shears, not by either of them. Both factors preserve the torus area form (areaForm_shearXR, areaForm_shearYR): the factoring is symplectic.

★★★ fibre_two_shears states the package. Read against #19's criterion (the de-isolation flow has a positive Lyapunov exponent on the fibre): a de-isolation that shears the fibre along q alone, by any base-read amount, has exponent 0 — so a de-isolation that could discharge R-019's map identification must act on the second fibre coordinate too, reading the first. That second coordinate is the one Posit 10 (I3, author's decision of 2026-10-10) says carries record content.

Honest scope

• ⚠️ Structure, not derivation. This says what a hyperbolic de-isolation would have to do to the fibre; it does not say that nature's does it, and nothing here decides #19 or R-019.
• The row that priced this file said each shear factor "carries the same flux obstruction as the corpus's shear". That wording does not apply and is corrected here: the shear factors are linear toral automorphisms, not time-one maps of vector fields on T² (the plane flow (x, y) ↦ (x, y + t x) descends only at integer t), so the flux obstruction for translation fields (not_isHamiltonianVectorField_torusStrokeField, LF4/ArenaStrokeFlux.lean) is about a different kind of map. What is true and proved of the factors is that they are symplectic (area-preserving) and Haar-preserving.
• The exponents are those of the lifts' derivatives, constant for every map here, as in FibreLyapunov.lean; no tangent bundle on T² is used.
• pshift-type is read literally: a map x ↦ pshift (g x) x for some real-valued g. The shearEvolve fibre action is of that type with g reading the base; shearX is of that type with g = rep ∘ Prod.snd.

References: specs/BACKLOG.md #153, #19, #148; specs/POSITS.md Posit 10; Mathlib/Dynamics/CatMapShears.lean (shearX, shearY, cat_eq_shearX_comp_shearY, hasLyapunovExponent_shearXR, cat_two_shears); SigmaLayer/FibreLyapunov.lean (fibre_witnesses_lyapunov, shearEvolve_snd); RecordLayer/ShearWitness.lean (pshift, shearEvolve); RecordLayer/CircleFibre.lean (rep, coe_rep); Mathlib/Geometry/Manifold/TranslationAtlasForm.lean (TorusForm.areaForm).

The transverse partner of pshift

noncomputable def CSD.SigmaLayer.qshift (a : ℝ) (x : LF4.KTorus) : LF4.KTorus

Translate the second fibre coordinate by a: the transverse partner of pshift.

Equations

• CSD.SigmaLayer.qshift a x = (x.1, x.2 + ↑a)

@[simp]

theorem CSD.SigmaLayer.qshift_fst (a : ℝ) (x : LF4.KTorus) : (qshift a x).1 = x.1

@[simp]

theorem CSD.SigmaLayer.pshift_snd (a : ℝ) (x : LF4.KTorus) : (RecordLayer.pshift a x).2 = x.2

A pshift-type map never moves the second coordinate.

theorem CSD.SigmaLayer.measurePreserving_qshift (a : ℝ) : MeasureTheory.MeasurePreserving (qshift a) MeasureTheory.volume MeasureTheory.volume

Translating the second coordinate preserves Haar measure on the fibre.

The two shears are coordinate-reading shifts

theorem CSD.SigmaLayer.shearX_eq_pshift (x : LF4.KTorus) : MeasureTheory.shearX x = RecordLayer.pshift (RecordLayer.rep x.2) x

The horizontal shear shifts the first coordinate by the second.

theorem CSD.SigmaLayer.shearY_eq_qshift (x : LF4.KTorus) : MeasureTheory.shearY x = qshift (RecordLayer.rep x.1) x

The vertical shear shifts the second coordinate by the first.

theorem CSD.SigmaLayer.catStroke_eq_two_shears : catStroke = (fun (x : LF4.KTorus) => RecordLayer.pshift (RecordLayer.rep x.2) x) ∘ fun (x : LF4.KTorus) => qshift (RecordLayer.rep x.1) x

★★ The hyperbolic stroke is two transverse coordinate-reading shifts: the second coordinate shifted by the first, then the first shifted by the (new) second.

One shear against two

theorem CSD.SigmaLayer.shearEvolve_snd_snd {Xsel : Type u_1} {K : ℕ} (idx : Xsel → Fin K) (s t : OnticTime) (x : Xsel × LF4.KTorus) : (RecordLayer.shearEvolve idx s t x).2.2 = x.2.2

★ The constructed de-isolation leaves the second fibre coordinate untouched. Together with shearEvolve_snd (the first coordinate is shifted by a base-read amount) this says the witness is a single pshift-type map of the fibre.

theorem CSD.SigmaLayer.catStroke_snd_ne : ∃ (x : LF4.KTorus), (catStroke x).2 ≠ x.2

The hyperbolic stroke moves the second coordinate of (1/2, 0).

theorem CSD.SigmaLayer.catStroke_ne_pshift_type (g : LF4.KTorus → ℝ) : catStroke ≠ fun (x : LF4.KTorus) => RecordLayer.pshift (g x) x

★ No single pshift-type map is the hyperbolic stroke, whatever its amount reads.

Neither shear stretches; the composition does

theorem CSD.SigmaLayer.shearXR_fderiv_hasLyapunovExponent (v w : ℝ × ℝ) : HasLyapunovExponent (fderiv ℝ (⇑MeasureTheory.shearXR) v) w 0

The lift of the horizontal shear has exponent 0 in every direction.

theorem CSD.SigmaLayer.shearYR_fderiv_hasLyapunovExponent (v w : ℝ × ℝ) : HasLyapunovExponent (fderiv ℝ (⇑MeasureTheory.shearYR) v) w 0

The lift of the vertical shear has exponent 0 in every direction.

theorem CSD.SigmaLayer.areaForm_shearXR (u v : ℝ × ℝ) : TorusForm.areaForm ![MeasureTheory.shearXR u, MeasureTheory.shearXR v] = TorusForm.areaForm ![u, v]

The horizontal shear's lift preserves the torus area form.

theorem CSD.SigmaLayer.areaForm_shearYR (u v : ℝ × ℝ) : TorusForm.areaForm ![MeasureTheory.shearYR u, MeasureTheory.shearYR v] = TorusForm.areaForm ![u, v]

The vertical shear's lift preserves the torus area form.

★★★ The package

theorem CSD.SigmaLayer.fibre_two_shears {Xsel : Type u_1} {K : ℕ} (idx : Xsel → Fin K) (s t : OnticTime) : (catStroke = (fun (x : LF4.KTorus) => RecordLayer.pshift (RecordLayer.rep x.2) x) ∘ fun (x : LF4.KTorus) => qshift (RecordLayer.rep x.1) x) ∧ (∀ (g : LF4.KTorus → ℝ), catStroke ≠ fun (x : LF4.KTorus) => RecordLayer.pshift (g x) x) ∧ (∀ (x : Xsel × LF4.KTorus), (RecordLayer.shearEvolve idx s t x).2 = RecordLayer.pshift ((RecordLayer.elapsed t - RecordLayer.elapsed s) * RecordLayer.shearAmt K (idx x.1)) x.2 ∧ (RecordLayer.shearEvolve idx s t x).2.2 = x.2.2) ∧ (∀ (v w : ℝ × ℝ), HasLyapunovExponent (fderiv ℝ (⇑MeasureTheory.shearXR) v) w 0) ∧ (∀ (v w : ℝ × ℝ), HasLyapunovExponent (fderiv ℝ (⇑MeasureTheory.shearYR) v) w 0) ∧ ∀ (v w : ℝ × ℝ), MeasureTheory.ellUR w ≠ 0 → HasLyapunovExponent (fderiv ℝ (⇑MeasureTheory.catR) v) w (2 * Real.log Real.goldenRatio)

★★★ The fibre carries both record coordinates: hyperbolicity needs the second coordinate sheared. The hyperbolic stroke is two transverse coordinate-reading shifts of the fibre and is not any single pshift-type map; the constructed de-isolation is a single pshift-type map whose amount reads the base and whose second fibre coordinate is untouched; each shear's lift has Lyapunov exponent 0 in every direction while their composition has exponent 2 log φ off the stable line. A de-isolation that shears along q alone cannot meet #19's criterion.