AreaPushforwardMatchOpen
plain-language theorem explainer
Names the (1,1)-orbit area pushforward identity: for every hinge slot of type t11, the covering-permutation pushforward of the orbit seed area covector equals the native slot area covector. Gravity analysts cite it when wiring transported multi-orbit Bloch folds to the classical slot convention. The body is a pure Prop; inhabitance is discharged separately by a one-line reduction to the t11 slot-orbit lemma.
Claim. For every hinge slot $(s,t)\in\mathrm{Fin}\,24\times\mathrm{Fin}\,10$ of orbit type $(1,1)$, the area covector obtained by pushing the $(1,1)$ orbit seed forward along the first $S_4$ covering permutation of that slot equals the native slot area covector (value $1/4$ on the two difference masks of the slot, else $0$).
background
This module builds a continuum-facing multi-orbit 4D Bloch fold: each hinge slot transports its orbit's seed area covector and star deficit kernel by the first $S_4$ covering permutation relative to a fixed orbit representative. The covering map orbitCoveringPerm picks that $S_4$ index for a given orbit type and slot; transport of the seed is then ordinary class pushforward.
The native slot area covector puts weight $1/4$ on the two difference masks of the slot and zero elsewhere. The predicate isT11 simply asserts that the hinge orbit type of $(s,t)$ is $(1,1)$. The transported area for type $(1,1)$ is the pushforward of the $(1,1)$ orbit seed area along a covering permutation.
Module status records that $(1,1)$ recovery of the classical slot area and deficit data is already theorem-level via uniform covering pushforward; non-$(1,1)$ orbits must not use the older factorized transport (measured all-orbit $m^2$ along the symbol direction on the TT-plus axis is $-5/2$ raw, not the factorized $0$).
proof idea
Definitional Prop only: the body is the universal statement over slots of type $(1,1)$ equating transported orbit area under the covering permutation with the native slot area covector. No tactics run here. Inhabitation is the sibling theorem that introduces $s,t$ and the type hypothesis, then simpa reduces through the slot-orbit area abbreviation to the already-proved $(1,1)$ covering identity.
why it matters
Closes the formerly open $(1,1)$ area-covector convention match inside the transported all-orbit fold. Downstream, the algebraic closer re-exports this Prop as its area-match obligation, now marked theorem rather than open. The sibling inhabitance theorem discharges it by reduction to the uniform covering pushforward for type $(1,1)$.
In the broader Regge–Bloch 4D stack this pins the area side of the transported fold against the classical slot convention, so $m^2$ on the $(1,1)$ slice can equal the existing symbol formula and the all-orbit fold can be assembled without a second area dictionary. It does not touch gap-action recovery. Remaining opens in the module are all-orbit $m^2$ Tendsto and continuum Einstein–Hilbert isotropy (still needing the residual 3D-style $2/N^4$ cell-sum dictionary).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.