Legal chain integral and polar coordinates
Abstract
Integral incidence inversion and polar forms on actual legal-chain states.
Notation: Nat, Int and Real denote the natural numbers, integers and real numbers. All named operators below use the corresponding Lean definitions in LegalChainMomentCoordinates, LegalChainMomentQuotient, LegalChainMomentTopology and LegalChainMomentGeometry. Application is written with parentheses; x.1 and x.2 are product projections and p.val is the underlying subtype value. Every displayed sum is over the indicated finite type. toReal is the integer-to-real inclusion, and toAngle is the ordinary projection Real to Real/(2 pi Int). A binder g in AddCommGroup(G) supplies the additive commutative group structure used in all subsequent expressions on G.
Pattern(n) is exactly the finite subsets I of Fin n with no i,j in I whose natural values satisfy i.val+1=j.val. Low(n,q) and High(n,q) are the subtypes with |I|<=q and q<|I|. V(n)=Pattern(n) to Real. incidence(n)(T,I)=1 when T is contained in I and is zero otherwise; signedIncidence(n)(I,T)=(-1)^(|T|-|I|) when I is contained in T and is zero otherwise. Matrix 1 is the identity. moments(p)(T)=sum over I containing T of p(I); probabilities(mu)(I)=sum over T containing I of (-1)^(|T|-|I|) mu(T); phases(theta)(T)=sum over I contained in T of (-1)^(|T|-|I|) theta(I); originalPhases(Phi)(I)=sum over T contained in I of Phi(T). Integer coefficients act by integer multiples in G.
PositiveProbability(n) consists of p in V(n) with every p(I)>0 and sum p(I)=1. ProbabilityFibre(q,p0) consists of all such p with moments(p)(T)=moments(p0)(T) for every T in Low(n,q). fillMoments(q,p0,x) fills the low slots from moments(p0) and the high slots from x. positiveDomain(q,p0)={x:High(n,q) to Real | every probabilities(fillMoments(q,p0,x))(I)>0}; using a set as a type means its subtype. Nonempty, IsOpen and Convex(Real,…) refer to this actual subset of the full high real function space.
occupationAction(n,q,G,t)(I) is the sum of t(T) over low T contained in I. actionHom(n,q,G,t)=originalPhases(lowEmbedding(t)), where lowEmbedding extends t by zero. PhaseOrbit(n,q,G,theta,eta) means there exists t with eta=theta+occupationAction(n,q,G,t). highPhases(q,theta)(T)=phases(theta)(T.val), with the source’s implicit q shown explicitly. Representative(q,p0)=ProbabilityFibre(q,p0) times all Pattern(n) phase circles. reductionSetoid keeps the probability equal and relates phases by PhaseOrbit. quotientCover(q,p0)(x,theta) is the inverse actual reductionHomeomorph applied to (x,angleCover(n,q)(theta)); angleCover projects each high real phase to its circle of period 2 pi.
polarMap(n,x)(I)=sqrt(x.1(I)) exp(-i x.2(I)); polarTorusMap(n,p,theta)(I)=sqrt(p(I)) times the unit-circle image of -theta(I). polarDerivative(n,x)(d)(I)=exp(-i x.2(I)) times (d.1(I)/(2 sqrt(x.1(I)))-i sqrt(x.1(I)) d.2(I)). amplitudeOneForm(n,x,d) is minus the imaginary part of sum conjugate(polarMap(n,x)(I)) polarDerivative(n,x)(d)(I). sourceTwoForm(n,d,e)=sum over I of d.2(I)e.1(I)-e.2(I)d.1(I). Writing psi(I)=polarMap(n,x)(I) and D(d)(I)=polarDerivative(n,x)(d)(I), projectiveTwoForm(n,x,d,e)=2 Im(sum conjugate(D(d)(I)) D(e)(I) - conjugate(sum conjugate(psi(I)) D(d)(I)) times (sum conjugate(psi(I)) D(e)(I))). Every sum here is over Pattern(n). HasFDerivAt asserts the actual real Frechet derivative, and IsLocalHomeomorph asserts local homeomorphism for the ordinary period projection.
Theorem 1.1 (Integral and polar coordinate laws).
Proof. Machine-checked in Lean as D5/S3/Quantum/Fibers/LegalChainMomentCoordinates.legal_chain_coordinate_laws (✓ std3). ∎
Source. Repository-derived.
Commentary.
For every finite path and every natural order q, the actual legal patterns are its independent subsets. Their downward closure identifies each inclusion interval with the powerset of the difference. Powerset signed cancellation proves both integral incidence inverse identities.
The signed upper moment inverse and unsigned lower phase inverse act by integer multiples on every additive commutative group, including the actual circle of period 2 pi. The literal occupation generators are exactly the inverse images of the low phase slots. Their orbits are classified by all high phases, with no residual finite ambiguity.
For every positive normalized reference law, the actual inverse-moment positivity inequalities define a nonempty open convex high-moment domain. The orbit quotient has its quotient topology and is homeomorphic to this domain times the ordinary high torus. Real lifts have exactly the independent 2 pi integer periods.
The amplitude on the actual phase circles has real-lift expression sqrt(p) exp(-i theta). Its Frechet derivative follows from the square-root and exponential rules. Minus the imaginary amplitude pairing gives sum p dtheta, equal to sum mu dPhi by integral duality. The source two-form becomes sum dPhi wedge dmu. On normalized probability tangents the rank-one projective correction has zero imaginary part, giving the specified projective form with the source sign.
These coordinate laws are used by the smooth fixed-moment reduction. All positivity assumptions, exact period relations and actual polar derivatives are retained.