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

Category: 7-SigmaLayer (regularity of pointer record-region complements).

The gap this closes

posMeasure_noRecord_of_correlates (SharpenedNoGo.lean) assumes that the complement of two disjoint open sets is contained in the closure of its interior (hreg). This module proves regularity of the full no-record set, then groups one record region against all the others to obtain a positive-measure set of inputs whose outputs avoid every record. Continuity, openness, an open preconnected ready set and attainment of two distinct outcomes remain hypotheses of the resulting theorem.

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 positive relevant record moment strictly decreases, and all relevant moments are < 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 — ready inputs whose outputs lie in the interior of the complement of all record regions have positive Fubini–Study measure, under the stated dynamical and ready-set hypotheses. The geometric regularity input is proved.

• not_ae_record_pointer — exact records cannot hold almost everywhere for Fubini–Study measure restricted to that ready set, under the same hypotheses.

Honest scope

The closure lemmas cover both the full no-record set and a selected pair's complement. The final positive-measure theorem uses the full complement for arbitrary K; the two selected indices witness attainment of distinct outcomes, not exhaustion of them.

The obstruction is conditional on the propagator and ready-set hypotheses. It does not classify alternative calibrations or prove that Dirac calibration is necessary. General trilemma exhaustiveness over other arenas is not proved here.

References

specs/BACKLOG.md B5, B5-geom (historical motivation) and Q13 (general trilemma exhaustiveness); specs/future-work.md; RecordLayer/SharpenedNoGo.lean (posMeasure_noRecord_of_correlates, whose hreg this discharges); RecordLayer/PointerArena.lean (recordRegion, the moment-region geometry); RecordLayer/NullSeamWitness.lean (the Dirac-calibrated witness); 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 later lemmas choose replacements of strictly larger norm converging to v 0, so boundary no-record rays are approximated by rays in the strict no-record set.

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, (Projectivization.mk ℂ v hv).momentMap 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, Projectivization.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 positive relevant moments decrease and zero moments remain below 1/2; convergence passes through Projectivization.mk'.

theorem CSD.RecordLayer.noRecord_subset_closure_strict {K : ℕ} (S : Set (Fin K)) : {q : Pointer K | ∀ j ∈ S, Projectivization.momentMap q j.succ ≤ 1 / 2} ⊆ closure {q : Pointer K | ∀ j ∈ S, Projectivization.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.fsMeasure q₀) (A ∩ Φ ⁻¹' interior (⋃ (i : Fin K), recordRegion i)ᶜ) ≠ 0

Positive measure of ready inputs whose outputs avoid every record region. Assume a continuous open map reaches two distinct outcomes from an open preconnected ready set A. Group one record region against the union of all the others, then apply posMeasure_noRecord_of_correlates using noRecord_subset_closure_interior. The resulting exceptional set avoids all K records, including when K > 2.

theorem CSD.RecordLayer.not_ae_record_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) : ¬∀ᵐ (q : Pointer K) ∂(Matrix.UnitaryGroup.fsMeasure q₀).restrict A, Φ q ∈ ⋃ (i : Fin K), recordRegion i

Under the same hypotheses, exact records cannot hold almost everywhere on the ready set with respect to restricted Fubini–Study measure. This applies to all K outcomes; it does not classify alternative ready sets, measures or propagators.