SigmaLayer/MovingFibreWitness: an ε > 0 projectable Hamiltonian, and a fibre that moves

Category: 7-SigmaLayer (the projective-sector layer, Paper C — the A5 approximate regime).

EpsProjectable is Σ1's central object, and until now every instance of it had ε = 0 (diagOnticEnergy, RecordLayer/ApproxProjectability.lean; the moment-map signature, RecordLayer/HamiltonianSignature.lean). An interface whose only inhabitants sit at the degenerate parameter is not populated in the sense that matters: the ε = 0 case is exactly "factors through π" (epsProjectable_zero_iff), so those instances say nothing about the approximate regime. This module supplies the missing inhabitant.

What is exhibited

★ movingFibreEnergy h g ε — the shape Paper C's approximate regime asks for, H = h ∘ π + ε·f·g with the fibre profile f = catObs/2 taken from the corpus's own hyperbolic-torus witness:

H (p, θ) = h p + ε · (g p · (catObs θ / 2))

★ movingFibreEnergy_epsProjectable — it is EpsProjectable at ε, for every ε ≥ 0 and every base profile g bounded by one. The bound is the pointwise oscillation |catObs θ − catObs θ'| ≤ 2 against the /2.

★★ movingFibreEnergy_not_projectable — and the fibre genuinely moves. For ε > 0 and g p ≠ 0 the Hamiltonian is not EpsProjectable at 0, so it does not factor through π. This is the non-vacuity that matters: without it the witness could be an ε = 0 instance wearing a parameter, which is precisely the defect the module exists to fix. The proof runs through cat_nontrivial (⟨f²⟩ ≠ ⟨f⟩²): a constant fibre profile has zero variance, and catObs does not.

★ catStroke — the hyperbolic fibre map, cat presented on KTorus with the properties a fibre stroke needs (catStroke_measurePreserving, catStroke_bijective, catStroke_continuous). ⚠️ It is hyperbolic, not a translation, which is the point: a translation cannot decorrelate (not_hasCorrelationDecay_of_compactGroup) while this map has correlations exactly zero at every nonzero lag (cat_hasCorrelationDecay).

⚠️ Scope, and one thing the item asked for that does not typecheck

KTorus is Torus2 — both are AddCircle 1 × AddCircle 1 — so the cat map is literally a map on the corpus's own fibre. No transport is needed and none is hidden.

⚠️ quantum_effective_shadowing cannot be instantiated at this witness, and the plan that asked for it was working from a wrong premise. That theorem is about matrices (H H₀ : Matrix (Fin N) (Fin N) ℂ, ‖H − H₀‖ ≤ ε), whereas EpsProjectable is about ontic Hamiltonians on KSigma N. The two are the same idea at different levels and the corpus has no bridge between them; supplying one is a separate piece of work, not a corollary. Nothing here claims the shadowing bound for this witness.

⚠️ This populates the predicate, not the dynamics: no flow is constructed whose generator this is, and catStroke is offered as an available hyperbolic fibre map rather than wired into a ConstraintDynamics. What is closed is the "no ε > 0 instance" gap (specs/reconstruction-status.md §7); what is not closed is A5's approximate regime as a dynamical statement.

References

RecordLayer/ApproxProjectability.lean (EpsProjectable, epsProjectable_zero_iff, epsProjectable_mono, quantum_effective_shadowing); Mathlib/Dynamics/CatMapWitness.lean (cat, catObs, cat_nontrivial, cat_hasCorrelationDecay, measurePreserving_cat); Mathlib/Dynamics/CompactGroupNoMixing.lean (not_hasCorrelationDecay_of_compactGroup — why a translation would not do); LF4/KahlerInstance.lean (KSigma, KTorus); specs/reconstruction-status.md §7; specs/future-work.md.

The hyperbolic fibre map

noncomputable def CSD.SigmaLayer.catStroke : LF4.KTorus → LF4.KTorus

The hyperbolic fibre stroke: the cat map, presented on the corpus's own fibre KTorus.

⚠️ Hyperbolic, deliberately. A torus translation provably cannot decorrelate (not_hasCorrelationDecay_of_compactGroup); this map has correlations exactly zero at every nonzero lag (cat_hasCorrelationDecay). Offered here as an available fibre map; it is not wired into a ConstraintDynamics.

Equations

• CSD.SigmaLayer.catStroke = MeasureTheory.cat

theorem CSD.SigmaLayer.catStroke_measurePreserving : MeasureTheory.MeasurePreserving catStroke MeasureTheory.volume MeasureTheory.volume

theorem CSD.SigmaLayer.catStroke_bijective : Function.Bijective catStroke

theorem CSD.SigmaLayer.catStroke_continuous : Continuous catStroke

theorem CSD.SigmaLayer.catStroke_hasCorrelationDecay : MeasureTheory.HasCorrelationDecay MeasureTheory.volume catStroke MeasureTheory.catObs MeasureTheory.catEnv

★ The hyperbolic stroke does decorrelate, with a finitely supported envelope: correlations are exactly zero at every nonzero lag.

theorem CSD.SigmaLayer.relaxation_requires_hyperbolic_fibre {N : ℕ} (p₀ : LF4.CPN N) (sh : LF4.KTorus) {ε : ℕ → ℝ} (hsum : Summable ε) : ¬MeasureTheory.HasCorrelationDecay (LF4.kMuL p₀) (LF4.kFlow sh) LF4.fibreObs ε ∧ MeasureTheory.HasCorrelationDecay MeasureTheory.volume catStroke MeasureTheory.catObs MeasureTheory.catEnv

★★ Relaxation requires a hyperbolic fibre — the CR-14 fallback, as a theorem.

On one and the same fibre KTorus, with observables of the same kind:

• the corpus's own fibre flow, the translation kFlow sh, admits no summable decay envelope at all — for every shift and every summable ε; and
• the hyperbolic stroke catStroke has one, indeed a finitely supported one.

⚠️ What this converts, and what it does not. It converts "CSD has no relaxation account" into "relaxation requires a hyperbolic fibre, and here is the proof that translations cannot supply it". That is a structural result about which dynamics could relax, not a relaxation theorem: nothing here shows a coarse-grained distribution approaches Haar, and no H-theorem is claimed. The H-theorem itself stays blocked on first-passage asymptotics for small sets, which is research-grade and is not scheduled (RESIDUE(R-019)).

⚠️ It also does not say Σ cannot mix. The obstruction is the choice of map, not the space: not_hasCorrelationDecay_of_compactGroup rules out flows whose iterates are powers of a compact-group element, and a torus translation is one while a toral automorphism is not (LF4/KahlerFibreMixing.lean).

The ε > 0 witness

noncomputable def CSD.SigmaLayer.movingFibreEnergy {N : ℕ} (h g : LF4.CPN N → ℝ) (ε : ℝ) : LF4.KSigma N → ℝ

The moving-fibre ontic Hamiltonian, in the shape Paper C's approximate regime asks for: H = h ∘ π + ε · f · g with fibre profile f = catObs/2 and base profile g.

Equations

• CSD.SigmaLayer.movingFibreEnergy h g ε x = h x.1 + ε * (g x.1 * (MeasureTheory.catObs x.2 / 2))

theorem CSD.SigmaLayer.movingFibreEnergy_epsProjectable {N : ℕ} (h g : LF4.CPN N → ℝ) {ε : ℝ} (hε : 0 ≤ ε) (hg : ∀ (p : LF4.CPN N), |g p| ≤ 1) : RecordLayer.EpsProjectable (movingFibreEnergy h g ε) ε

★ The witness is EpsProjectable at ε. Fibre oscillation is bounded by ε because catObs is bounded by one and the profile is halved.

theorem CSD.SigmaLayer.movingFibreEnergy_not_projectable {N : ℕ} (h g : LF4.CPN N → ℝ) {ε : ℝ} (hε : 0 < ε) {p : LF4.CPN N} (hgp : g p ≠ 0) : ¬RecordLayer.EpsProjectable (movingFibreEnergy h g ε) 0

★★ And the fibre genuinely moves. For ε > 0 at a base point where the profile does not vanish, the witness is not EpsProjectable at 0 — equivalently, it does not factor through π (epsProjectable_zero_iff).

This is the non-vacuity the module exists for. Without it the witness could be an ε = 0 instance wearing a parameter, which is exactly the defect being fixed. The proof is variance: a constant fibre profile would give ⟨f²⟩ = ⟨f⟩², and cat_nontrivial says catObs does not.