SigmaLayer/NoRecordGeometry: the no-record set is inside the closure of its interior

Category: dynamical measurement — specs/BACKLOG.md B5-geom, the single remaining hypothesis of B5, the trilemma's third leg.

The gap this closes

posMeasure_noRecord_of_correlates (SharpenedNoGo.lean) proved the third leg with every dynamical hypothesis discharged and exactly one geometric assumption left: hreg, that the no-record set is contained in the closure of its interior. This module constructs the perturbation that proves it, and instantiates the leg for the pointer's own record regions — so B5 closes outright.

The construction: feed weight into the ready component

For q = [v] with the relevant record moments m_{j+1}(q) ≤ 1/2, perturb v by replacing its ready component v 0 with a slightly larger one (feedReady):

• every record numerator ‖v (j+1)‖² is untouched (feedReady_succ),
• the norm strictly grows (norm_sq_feedReady_gt),
• hence every relevant record moment strictly drops below 1/2 — the perturbed ray has all of them < 1/2 (a moment with zero numerator stays 0 < 1/2).

The replacement family is phase-preserving where it matters: if v 0 ≠ 0 we scale it by 1 + 1/(n+1) (same phase, so convergence to v is immediate — no chart argument); if v 0 = 0 we insert the real weight 1/(n+1) (converging to 0 = v 0). Either way feedReady v (c n) → v, so the perturbed rays converge to q through the continuous quotient map Projectivization.mk', and q lies in the closure of the strict set (mem_closure_of_tendsto).

★ mk_mem_closure_strictNoRecord / noRecord_subset_closure_strict — the core, for an arbitrary index set S (so one proof serves both consumers below). ★ noRecord_subset_closure_interior — the B5-geom statement: the full no-record set (⋃ j, recordRegion j)ᶜ is contained in the closure of its interior. ★★ posMeasure_noRecord_pointer — B5 closed: on the pointer manifold, a continuous open-map propagator that correlates two outcomes on an open preconnected ready set gives the no-record set positive Fubini–Study measure. Every hypothesis is now either the witness's own dynamics or a theorem; nothing geometric is assumed.

Honest scope

This is the local trilemma leg (the pointer's moment-region geometry), exactly as scoped when the row was parked: general exhaustiveness — no witness on any arena combines continuity, positive-width ready, a.e.-exact records and exact Born — quantifies over all arenas and stays research (specs/BACKLOG.md §E, the two research frontiers).

References

specs/BACKLOG.md B5, B5-geom (and §E for general trilemma exhaustiveness, which stays research); specs/future-work.md (the completed-work ledger this lands in); SigmaLayer/SharpenedNoGo.lean (posMeasure_noRecord_of_correlates, whose hreg this discharges); SigmaLayer/PointerArena.lean (recordRegion, the moment-region geometry); SigmaLayer/NullSeamWitness.lean (the third horn whose Dirac price this makes a theorem); docs/TOUR.md §"Which horn is the right one?".

The perturbation: feed weight into the ready component

noncomputable def CSD.RecordLayer.feedReady {K : ℕ} (v : EuclideanSpace ℂ (Fin (K + 1))) (c : ℂ) : EuclideanSpace ℂ (Fin (K + 1))

Replace the ready component of v by c, leaving every record component untouched. The module is the observation that this map carries a boundary no-record state into the strict no-record set while converging back to v.

Equations

• CSD.RecordLayer.feedReady v c = WithLp.toLp 2 (Function.update v.ofLp 0 c)

theorem CSD.RecordLayer.feedReady_of_ne {K : ℕ} (v : EuclideanSpace ℂ (Fin (K + 1))) (c : ℂ) {i : Fin (K + 1)} (hi : i ≠ 0) : (feedReady v c).ofLp i = v.ofLp i

Components away from the ready index are untouched.

theorem CSD.RecordLayer.feedReady_succ {K : ℕ} (v : EuclideanSpace ℂ (Fin (K + 1))) (c : ℂ) (j : Fin K) : (feedReady v c).ofLp j.succ = v.ofLp j.succ

Record components are untouched: the record numerators are fixed.

theorem CSD.RecordLayer.feedReady_zero {K : ℕ} (v : EuclideanSpace ℂ (Fin (K + 1))) (c : ℂ) : (feedReady v c).ofLp 0 = c

The ready component is replaced.

theorem CSD.RecordLayer.feedReady_self {K : ℕ} (v : EuclideanSpace ℂ (Fin (K + 1))) : feedReady v (v.ofLp 0) = v

Feeding the original component back is the identity.

theorem CSD.RecordLayer.norm_sq_feedReady_gt {K : ℕ} (v : EuclideanSpace ℂ (Fin (K + 1))) {c : ℂ} (hc : ‖v.ofLp 0‖ < ‖c‖) : ‖v‖ ^ 2 < ‖feedReady v c‖ ^ 2

The norm strictly grows when the ready component does: split the sum at 0; the erased part is untouched.

theorem CSD.RecordLayer.feedReady_ne_zero {K : ℕ} (v : EuclideanSpace ℂ (Fin (K + 1))) {c : ℂ} (hc : ‖v.ofLp 0‖ < ‖c‖) : feedReady v c ≠ 0

The perturbed vector is nonzero: its norm-square strictly exceeds a nonnegative one.

theorem CSD.RecordLayer.tendsto_feedReady {K : ℕ} (v : EuclideanSpace ℂ (Fin (K + 1))) {c : ℕ → ℂ} (hlim : Filter.Tendsto c Filter.atTop (nhds (v.ofLp 0))) : Filter.Tendsto (fun (n : ℕ) => feedReady v (c n)) Filter.atTop (nhds v)

As the fed component tends to v 0, the perturbed vectors tend to v.

The closure argument on rays

theorem CSD.RecordLayer.mk_mem_closure_strictNoRecord {K : ℕ} (S : Set (Fin K)) (v : EuclideanSpace ℂ (Fin (K + 1))) (hv : v ≠ 0) (hle : ∀ j ∈ S, LF4.momentMap (Projectivization.mk ℂ v hv) j.succ ≤ 1 / 2) (c : ℕ → ℂ) (hgt : ∀ (n : ℕ), ‖v.ofLp 0‖ < ‖c n‖) (hlim : Filter.Tendsto c Filter.atTop (nhds (v.ofLp 0))) : Projectivization.mk ℂ v hv ∈ closure {q : Pointer K | ∀ j ∈ S, LF4.momentMap q j.succ < 1 / 2}

★ The core: a ray whose S-indexed record moments are all ≤ 1/2 lies in the closure of the set where they are all < 1/2, along any feeding family that strictly enlarges the ready component while converging to it. The record numerators are fixed (feedReady_succ) while the norm strictly grows (norm_sq_feedReady_gt), so every relevant moment strictly drops; convergence passes through Projectivization.mk'.

theorem CSD.RecordLayer.noRecord_subset_closure_strict {K : ℕ} (S : Set (Fin K)) : {q : Pointer K | ∀ j ∈ S, LF4.momentMap q j.succ ≤ 1 / 2} ⊆ closure {q : Pointer K | ∀ j ∈ S, LF4.momentMap q j.succ < 1 / 2}

★ The ≤-set is inside the closure of the <-set, for any index set S of record moments. The two feeding branches: if v 0 = 0, insert the real weight 1/(n+1); else scale v 0 by 1 + 1/(n+1) — phase-preserving, so the limit is immediate.

The record-region geometry, discharged

theorem CSD.RecordLayer.noRecord_subset_closure_interior {K : ℕ} : (⋃ (j : Fin K), recordRegion j)ᶜ ⊆ closure (interior (⋃ (j : Fin K), recordRegion j)ᶜ)

★ B5-geom: the full no-record set is contained in the closure of its interior. A state with every record moment ≤ 1/2 is approximated by states with every record moment < 1/2 — obtained by feeding weight toward the ready vertex — and the strict set is open, hence inside the interior.

theorem CSD.RecordLayer.recordRegion_pair_compl_regular {K : ℕ} (j l : Fin K) : (recordRegion j ∪ recordRegion l)ᶜ ⊆ closure (interior (recordRegion j ∪ recordRegion l)ᶜ)

★ The pair form posMeasure_noRecord_of_correlates consumes: the complement of a union of two record regions is regular (contained in the closure of its interior).

theorem CSD.RecordLayer.posMeasure_noRecord_pointer {K : ℕ} (q₀ : Pointer K) {Φ : Pointer K → Pointer K} (hopen : IsOpenMap Φ) (hcont : Continuous Φ) {A : Set (Pointer K)} (hA : IsOpen A) (hconn : IsPreconnected A) {j l : Fin K} (hjl : j ≠ l) (hmeetj : ∃ x ∈ A, Φ x ∈ recordRegion j) (hmeetl : ∃ x ∈ A, Φ x ∈ recordRegion l) : (Matrix.UnitaryGroup.fubiniStudyMeasure q₀) (A ∩ Φ ⁻¹' interior (recordRegion j ∪ recordRegion l)ᶜ) ≠ 0

★★ The trilemma's third leg, closed (BACKLOG B5). On the pointer manifold, a continuous open-map propagator that correlates two outcomes on an open preconnected ready set gives the no-record set positive Fubini–Study measure. Compared with posMeasure_noRecord_of_correlates, no geometric hypothesis remains: regularity of the no-record set is recordRegion_pair_compl_regular, disjointness and openness of the record regions are the arena's own theorems, and FS positivity on opens is fubiniStudyMeasure_pos_of_isOpen. Exact-a.e. records therefore force Dirac calibration — the third horn's price is now a theorem, not a classification.