Projectability

In plain terms

If the world is a large deterministic space and quantum mechanics is written on a much smaller curved one, something must connect them, as you can't get the small picture out of the big one for free. The connection is structure, and structure has to be paid for.

Projectability is the payment, made openly. It says the arena admits a many-to-one projection onto the quantum state space, a map that sends every point of the large space to a point of the small one, with many points sharing each target, much as a solid object casts a flat shadow. The projection must be compatible with the dynamics, so motion on the arena maps to the expected motion of quantum states, and with the symmetry. It's one postulate, stated once, and carried as an explicit hypothesis everywhere it's used.

The discipline lies in what isn't postulated. The measure isn't, as symmetry forces it. The Born rule, the quantum rule for outcome probabilities, isn't, as it's computed as a volume. The dynamics on the projected space aren't, as they're derived from record statistics. The programme keeps its postulate count where you can audit it.

In CSD

This is Paper C's sector postulate, the assumption that the constraint surface projects onto a projective sector, the curved space of quantum states regarded as a view of the arena, on which the reconstruction runs. It's projectability, and never "the origin of the constraint surface", as the projection points the wrong way for that reading, so the surface is the floor and the sector is a view of it and not its source.

In the formal corpus the postulate is never assumed globally. Every theorem that needs it takes it as an explicit hypothesis, so the corpus's record of assumptions stays clean and the cost is visible at every point of use.

Mathematically

In Lean the postulate is a structure field and not an axiom, so the kernel's axiom report is unaffected by it. SectorData packages the postulate as a measurable projection from the ontic space to an abstract projective target, a group acting on both sides, invariance of the Liouville measure, and equivariance of the projection.

A guard script enforces that the descent equation is genuinely consumed downstream, as the corpus was once burned by a substrate that was carried but unused, and the linkage is checked mechanically.

Related entries

• Constraint surfaceThere's one arena, it's deterministic, and it doesn't grow, and everything else in the programme is bookkeeping about how much of it a measurement context lets you see.
• Projective sectorQuantum mechanics is written on a curved projective space, and in CSD that space isn't fundamental, as it's the sector the arena projects onto, with its geometry forced by symmetry.
• Many-to-one projectionBehind every quantum state stands a crowd of world-states, and the projection that maps the crowd to one state loses information on purpose, and that loss is where quantum probability comes from.
• Wigner rigidityPreserve the overlaps between quantum states and you have no freedom left, as the rearrangement must be a unitary or an anti-unitary transformation whether or not you intended it to be.
• Schrodinger from recordsCSD doesn't postulate the Schrodinger equation, as preserving the statistics of records forces the dynamics to be unitary, unitarity together with continuity forces a Hamiltonian, and the exponential form of the equation is a theorem at the end of that chain.