RecordLayer/CellLawFreedom: the moment-map cell law is a posit, and here is why

Category: 7-SigmaLayer (the record layer's own foundations).

globalBasin_born reads the Born weights off the fibre partition at momentContext, and the corpus's prose has read that as the rates are forced by the Kähler structure.

In the standard symplectic reading that is true, and this module does not dispute it. A moment map for the Tⁿ action on connected ℂℙ^{N−1} is unique up to an additive constant; sum-one and non-negativity pin the constant to zero. (At the form's fixed scale — the corpus normalisation ω u (J u) = ‖u‖² of IsFubiniStudyKahler; rescaling ω ↦ λω readmits a family λΦ + c.)

But that argument is unformalised HERE, and what this module verifies does not carry it. When this was written Mathlib had no symplectic API and the corpus did not state the moment-map equation ι_{X_i} ω = dΦᵢ. Since 2026-09-08 it does, on the manifold (Projectivization.torusField_isHamiltonianVectorField, eq_torusHamiltonian_of_nonneg_of_sum — the standard argument above as a theorem, G6/G8); see LF4/MomentMap.lean's header. This module's own claim is unchanged: momentMap is defined by the coordinate formula, and what is machine-checked about it here is that formula plus its symmetries. This module shows those do not pin it down: globalBasin_prob holds for every ContextField, momentContext is one field among many, and bornRate is a definition. Relative to the machine-checked corpus the cell law is a structural posit, and the prose that cites momentMap_mk for "forced" is citing a scale-invariance lemma for a claim it does not make.

This module makes that concrete rather than conceding it in prose, by exhibiting a second, fully functioning cell law.

What is exhibited

★ sqContext — the normalised-squares field x ↦ x²/∑x² composed with the moment map. It is a ContextField in good standing: non-negative, normalised, measurable. It is torus-invariant (★ sqRate_phaseDiag_invariant, inherited from momentMap_phaseDiag_invariant), it vanishes exactly where the moment map does (★ sqRate_eq_zero_iff), and — since globalBasin_prob is generic — it drives the whole basin machinery, producing its own Born-like weights (★ globalBasin_prob_sqContext).

★★ rate_field_not_forced_by_torus_symmetry — and it is not the moment map: at the explicit state ψ = (2, 1, 1) in ℂℙ², whose moment coordinates are (⅔, ⅙, ⅙), the normalised-squares field gives outcome 0 the rate 8/9 where the moment map gives ⅔.

What this settles, and what it does not

Settles: torus invariance, normalisation, measurability and the support condition — the properties the corpus actually verifies — do not characterise the moment map. So the step "the rates are torus-equivariant and normalised, hence they are the moment map" is invalid; equivariance is shared by a continuum of other fields, of which this is one. The symplectic argument above is untouched, because sqRate is not a moment map for the torus action: no ι_{X_i} ω = d(sqRateᵢ) holds. What fails is the weak package, which is the only package in Lean.

Settled since, by a different route: a stronger condition does characterise the moment map, and it is not the one guessed here. RecordLayer/CellLawForced.lean proves torusGenerated_eq_momentMap — a context field whose rates generate the coordinate phase rotations (the moment-map equation, at the linear level) is exactly the moment map, and sqContext_not_torusGenerated shows the rival below fails precisely that. The gap between the two modules is one word: sqRate is invariant under the torus, the moment map generates it.

The frame-function route sketched below was declined, not attempted: it would have bought the cell law with noncontextuality. Kept because the cost analysis is worth preserving. The natural candidate was consistency across bases — a rate field defined for every orthogonal decomposition and additive under merging outcomes is a frame function, and for N ≥ 3 that is Gleason's hypothesis. Whether the corpus's effect_gleason_representation transfers (it fixes a state and varies effects; the cell law fixes a context and varies the state) is open and is stage 2 of specs/cell-law-scoping.md. ⚠️ If noncontextuality is what forces the cell law, then "Gleason-free" is true of the volume theorem and false of the choice of cell law — a distinction worth keeping.

⚠️ Not a claim that nothing in the corpus distinguishes them. Two things do. (i) The Duistermaat–Heckman results: the moment map pushes μ_FS forward to the flat law on [0,1] (LF4/MomentUniform.lean, fs_moment_pushforward_uniform) and to the Dirichlet law on the simplex (LF4/MomentDirichletN.lean, fs_moment_joint_dirichlet_N); sqRate's pushforward is neither. That is a proved asymmetry — though not a characterisation (any μ_FS-preserving precomposition shares a pushforward), and no record-layer selection argument currently invokes it. (ii) bornRate has a flow-carved witness (shearDeIsolationInteraction discharges basin_rate from a constructed propagator); sqRate has none. ⚠️ Superseded in part: when this was written, what selected momentContext was agreement with the Born target. CellLawForced.lean now supplies an in-corpus selection theorem whose premise mentions no probability at all.

Not a defect report. The machinery is correct and globalBasin_born is true. What is corrected is an account of why it is true.

References

RecordLayer/GlobalBasin.lean (ContextField, globalBasin_prob, momentContext, globalBasin_born); RecordLayer/MomentMapRace.lean (bornRate_eq_momentMap — the identification whose docstring this module qualifies); RecordLayer/HamiltonianSignature.lean (momentMap_phaseDiag_invariant, the torus action); LF4/MomentMap.lean (momentMap_nonneg, momentMap_sum_eq_one, momentMap_mk); LF4/MomentUniform.lean, LF4/MomentDirichletN.lean (the Duistermaat–Heckman pushforward laws); specs/POSITS.md (Posit 1); specs/cell-law-scoping.md (stage 2); specs/future-work.md ("Cell-law characterisation (stage 2)").

A second cell law

noncomputable def CSD.RecordLayer.sqRate {N : ℕ} (p : LF4.CPN N) (i : Fin N) : ℝ

The normalised-squares rate: x ↦ xᵢ² / ∑ₖ xₖ² applied to the moment coordinates.

Chosen because it shares every symmetry property the moment map is usually motivated by, and is not the moment map.

Equations

• CSD.RecordLayer.sqRate p i = Projectivization.momentMap p i ^ 2 / ∑ k : Fin N, Projectivization.momentMap p k ^ 2

theorem CSD.RecordLayer.sq_sum_pos {N : ℕ} (p : LF4.CPN N) : 0 < ∑ k : Fin N, Projectivization.momentMap p k ^ 2

The denominator is positive: the moment coordinates are non-negative and sum to one, so they cannot all vanish.

theorem CSD.RecordLayer.sqRate_nonneg {N : ℕ} (p : LF4.CPN N) (i : Fin N) : 0 ≤ sqRate p i

theorem CSD.RecordLayer.sqRate_sum_eq_one {N : ℕ} (p : LF4.CPN N) : ∑ i : Fin N, sqRate p i = 1

theorem CSD.RecordLayer.measurable_sqRate {N : ℕ} (i : Fin N) : Measurable fun (p : LF4.CPN N) => sqRate p i

noncomputable def CSD.RecordLayer.sqContext (N : ℕ) : ContextField N

★ A second cell law. The normalised-squares field is a ContextField in good standing — so every theorem GlobalBasin.lean proves for an arbitrary context field applies to it.

Equations

• CSD.RecordLayer.sqContext N = { rate := CSD.RecordLayer.sqRate, measurable_rate := ⋯, nonneg := ⋯, sum_one := ⋯ }

@[simp]

theorem CSD.RecordLayer.sqContext_rate {N : ℕ} (p : LF4.CPN N) : (sqContext N).rate p = sqRate p

It has the symmetries the moment map is motivated by

theorem CSD.RecordLayer.sqRate_phaseDiag_invariant {N : ℕ} (φ : Fin N → ℝ) (p : LF4.CPN N) (i : Fin N) : sqRate (phaseDiag φ • p) i = sqRate p i

★ Torus-invariant. The diagonal phase action preserves every moment coordinate, hence the normalised-squares field built from them. This is the property usually offered as the reason the moment map is canonical; it does not distinguish the two fields.

theorem CSD.RecordLayer.sqRate_eq_zero_iff {N : ℕ} (p : LF4.CPN N) (i : Fin N) : sqRate p i = 0 ↔ Projectivization.momentMap p i = 0

★ Same support. The rate vanishes exactly where the moment coordinate does, so the "vanishes off the i-th coordinate hyperplane" condition does not distinguish them either.

theorem CSD.RecordLayer.globalBasin_prob_sqContext {N : ℕ} (i : Fin N) (p : LF4.CPN N) : (epistemicMeasure p) (globalBasin (sqContext N) i) = ENNReal.ofReal (sqRate p i)

★ It drives the basin machinery. globalBasin_prob is generic in the context field, so the alternative cell law produces its own weights on its own basins. This makes it a genuine underdetermination witness for the interface — not a rival account of measurement: it is not empirically adequate, giving 8/9 where Born requires ⅔. That is the point. Empirical adequacy, not geometry, is what picks momentContext out.

The separation

noncomputable def CSD.RecordLayer.witState : EuclideanSpace ℂ (Fin 3)

The witness state (2, 1, 1) in ℂℙ², unnormalised. Rational entries deliberately: the moment coordinates come out (⅔, ⅙, ⅙) with no square roots, and the two rate fields separate there.

Equations

• CSD.RecordLayer.witState = !₂[2, 1, 1]

theorem CSD.RecordLayer.witState_ne_zero : witState ≠ 0

theorem CSD.RecordLayer.norm_sq_witState : ‖witState‖ ^ 2 = 6

theorem CSD.RecordLayer.momentMap_witState_zero : (Projectivization.mk ℂ witState witState_ne_zero).momentMap 0 = 2 / 3

theorem CSD.RecordLayer.momentMap_witState (i : Fin 3) : (Projectivization.mk ℂ witState witState_ne_zero).momentMap i = ![2 / 3, 1 / 6, 1 / 6] i

theorem CSD.RecordLayer.sq_sum_witState : ∑ k : Fin 3, (Projectivization.mk ℂ witState witState_ne_zero).momentMap k ^ 2 = 1 / 2

theorem CSD.RecordLayer.rate_field_not_forced_by_torus_symmetry : ∃ (p : LF4.CPN 3) (i : Fin 3), sqRate p i ≠ Projectivization.momentMap p i

★★ The cell law is not forced by the symmetries usually offered for it.

At [(2,1,1)] ∈ ℂℙ² the moment map gives outcome 0 the rate ⅔; the normalised-squares field — torus-invariant, normalised, measurable, with the same support — gives it 8/9. So no argument from equivariance, normalisation and support can single out the moment map: those hypotheses hold of both.

momentContext is therefore not pinned down by these properties. What does pin it is torus generation rather than invariance — torusGenerated_eq_momentMap in RecordLayer/CellLawForced.lean, which this theorem is the exact complement of: invariance leaves a continuum, generation leaves one.