Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

HeadleyCubeOddProduct

Abstract

An ordinary R-cycle on an arbitrary finite odd group supplies the exceptional product.

Remark 1.1 (Shared actual row and difference equivalences).

Lean statement: D5/S3/FiniteGroups/HeadleyCubeOddProduct.shiftedSuccessor

Formalization. D5/S3/FiniteGroups/HeadleyCubeOddProduct.shiftedSuccessor (✓ std3).

Source. Repository-derived.

Commentary.

Sigma and delta are the supplied RCycle successor and actual difference permutations. Both fix zero. The nonzero sigma orbit and delta injectivity give sigma(h) nonzero and sigma(h) unequal to h for h nonzero. No RStar, additive ranking or cyclic generator is assumed.

The original odd_box additive equivalence e:H→Box(ds) conjugates the original doubling permutation to B2(h)=h+h. DeltaT is negative doubling. Set f_a=sigma at a=0 and at the last column, and f_a=negation at the other six columns; set Delta_a=delta or DeltaT correspondingly.

A(a,h)=(a,h-s_a), F(a,x)=(a,f_a(x)), C_P(a,x)=(P(a),x), B(a,x)=(a,s_a+x). S0=A.trans F.trans C_P.trans B. With E(a,x)=(a,Delta_a(x)), R(a,y)=(a,y+s_(P(a))-s_a) and C_Q(a,y)=(Q(a),y), D0=A.trans E.trans R.trans C_Q. Each stage is an actual equivalence. Assume Q(a)=P(a)-a for every a. Then D0(a,h)=(Q(a),Delta_a(h-s_a)+s_(P(a))-s_a)=S0(a,h)-(a,h), including every closing edge.

The inverse of S0 at (b,t) has a=P.symm(b) and value (a,s_a+f_a.symm(t-s_b)). The inverse of D0 has a=Q.symm(b) and value (a,s_a+Delta_a.symm(t-s_(P(a))+s_a)). These are reverse compositions of the actual constituent inverses.

For the listed seven columns a_i, V(inl h)=(0,h) and V(inr(i,x))=(a_i,s_(a_i)+(-1)^i x). For a nonzero first coordinate its inverse looks up i and gives inr(i,(-1)^i(h-s_a)); at a=0 it gives inl h. V is a set equivalence. It is not used to transport differences. Assume P(0)=0, s(0)=0 and P(a_i)=a_(i+1 mod 7) for every i in Fin(7). Under these premises V conjugates sum(sigma,cylinder(sigma,4)) to S0: the six ordinary rows negate and the last row applies sigma after the even parity gauge.

The original cylinder_partial, cylinder_round and cylinder_rounds give intermediate columns j<7, return (0,h) after seven steps to (0,sigma(h)), and repeated seven-step returns. Distinct column indices exclude an earlier anchor visit. The input IsCycleOn bounded orbit has length m=card(H)-1 on nonzero h, so the nonzero return period is m. Its implemented equivalence uses exists_pow_eq and injOn_pow_apply, and pow_card_apply supplies the closing return used in connectivity. The original cylinder_connect and sum_sameCycle lifts give exactly three nonzero components: C_H={(0,h):h nonzero}, C_Z={(a,s_a):a nonzero}, and C_N={(a,h):a nonzero and h unequal to s_a}. Their sizes are m,7,7m; the remaining vertex is the fixed origin.

The source successor is Sprime=S0*swap(X,Y)*swap(Z,W). First X in C_H and Y in C_Z join different cycles, separated by the zero-column invariant. The nonzero-offset predicate is invariant under S0 and the first swap. Thus Z in the joined class and W in C_N still lie on different cycles, and the second original swap_joins merges them. The preservation clauses and the chart coverage connect every nonzero vertex; bijOn_complement at the untouched origin completes IsCycleOn.

The successor pairing is tau=swap(X,Y)*swap(Z,W) in both products. The label-source pairing is separately Lambda=swap(X,Z)*swap(Y,W) for HeadleyCubeOddProduct and Lambda=swap(X,W)*swap(Y,Z) for HeadleyC2C4OddProduct. Dprime=Lambda.trans D0. The four source calculations and identity away from those sources prove Dprime(x)=Sprime(x)-x universally. The successor inverse is S0.symm.trans(tau.symm), with tau=swap(X,Y)*swap(Z,W); the difference inverse is D0.symm.trans(Lambda.symm).

All formulas keep arbitrary finite odd noncyclic H. For nontrivial H, n=card(H) is odd and at least three, and m=n-1 is at least two. Allowed coincidences between shifts and between parameters are retained. For trivial H, the definition constructs Subsingleton H and Unique H with default zero and transports the same fixed coefficient RCycle through AddEquiv.prodUnique.symm.

The construction formalizes the supplied native R-only four-source proof. Original HeadleyExtension cylinder, invariant, sum-lift and swap-join proofs are reused at their source; odd_box and doubling reuse the original Gordon normalization. The existing RStar product has a stronger premise and is not applied here. This is repo-derived formal composition, with no mathematical novelty claim. The four-slot audit remains unfinished under https://github.com/the-omega-institute/trureturing/issues/21215 for successor_ne_self, row_zero, shiftedSuccessor_apply, shifted_difference_spec, gauge_zero, chart_inr and joined_nonzero_cycle. Their current source owner and namespace are D5/S3/FiniteGroups/HeadleyCubeOddProduct and D5.S3.FiniteGroups.HeadleyCubeOddProduct, respectively; the issue uses their former HeadleyExceptionalRows owner, and each final declaration name is unchanged. No declared_validated registration is supplied. The arbitrary-subset, same-M, original-coordinate, coefficient-one parent and unrestricted AM remain open.

Definition 1.2 (The complete original-coordinate constructor).

Lean statement: D5/S3/FiniteGroups/HeadleyCubeOddProduct.cube_odd_product

Formalization. D5/S3/FiniteGroups/HeadleyCubeOddProduct.cube_odd_product (✓ std3).

Source. Repository-derived.

Commentary.

Sigma and delta are the supplied RCycle successor and actual difference permutations. Both fix zero. The nonzero sigma orbit and delta injectivity give sigma(h) nonzero and sigma(h) unequal to h for h nonzero. No RStar, additive ranking or cyclic generator is assumed.

The original odd_box additive equivalence e:H→Box(ds) conjugates the original doubling permutation to B2(h)=h+h. DeltaT is negative doubling. Set f_a=sigma at a=0 and at the last column, and f_a=negation at the other six columns; set Delta_a=delta or DeltaT correspondingly.

A(a,h)=(a,h-s_a), F(a,x)=(a,f_a(x)), C_P(a,x)=(P(a),x), B(a,x)=(a,s_a+x). S0=A.trans F.trans C_P.trans B. With E(a,x)=(a,Delta_a(x)), R(a,y)=(a,y+s_(P(a))-s_a) and C_Q(a,y)=(Q(a),y), D0=A.trans E.trans R.trans C_Q. Each stage is an actual equivalence. Assume Q(a)=P(a)-a for every a. Then D0(a,h)=(Q(a),Delta_a(h-s_a)+s_(P(a))-s_a)=S0(a,h)-(a,h), including every closing edge.

The inverse of S0 at (b,t) has a=P.symm(b) and value (a,s_a+f_a.symm(t-s_b)). The inverse of D0 has a=Q.symm(b) and value (a,s_a+Delta_a.symm(t-s_(P(a))+s_a)). These are reverse compositions of the actual constituent inverses.

For the listed seven columns a_i, V(inl h)=(0,h) and V(inr(i,x))=(a_i,s_(a_i)+(-1)^i x). For a nonzero first coordinate its inverse looks up i and gives inr(i,(-1)^i(h-s_a)); at a=0 it gives inl h. V is a set equivalence. It is not used to transport differences. Assume P(0)=0, s(0)=0 and P(a_i)=a_(i+1 mod 7) for every i in Fin(7). Under these premises V conjugates sum(sigma,cylinder(sigma,4)) to S0: the six ordinary rows negate and the last row applies sigma after the even parity gauge.

The original cylinder_partial, cylinder_round and cylinder_rounds give intermediate columns j<7, return (0,h) after seven steps to (0,sigma(h)), and repeated seven-step returns. Distinct column indices exclude an earlier anchor visit. The input IsCycleOn bounded orbit has length m=card(H)-1 on nonzero h, so the nonzero return period is m. Its implemented equivalence uses exists_pow_eq and injOn_pow_apply, and pow_card_apply supplies the closing return used in connectivity. The original cylinder_connect and sum_sameCycle lifts give exactly three nonzero components: C_H={(0,h):h nonzero}, C_Z={(a,s_a):a nonzero}, and C_N={(a,h):a nonzero and h unequal to s_a}. Their sizes are m,7,7m; the remaining vertex is the fixed origin.

The source successor is Sprime=S0*swap(X,Y)*swap(Z,W). First X in C_H and Y in C_Z join different cycles, separated by the zero-column invariant. The nonzero-offset predicate is invariant under S0 and the first swap. Thus Z in the joined class and W in C_N still lie on different cycles, and the second original swap_joins merges them. The preservation clauses and the chart coverage connect every nonzero vertex; bijOn_complement at the untouched origin completes IsCycleOn.

The successor pairing is tau=swap(X,Y)*swap(Z,W) in both products. The label-source pairing is separately Lambda=swap(X,Z)*swap(Y,W) for HeadleyCubeOddProduct and Lambda=swap(X,W)*swap(Y,Z) for HeadleyC2C4OddProduct. Dprime=Lambda.trans D0. The four source calculations and identity away from those sources prove Dprime(x)=Sprime(x)-x universally. The successor inverse is S0.symm.trans(tau.symm), with tau=swap(X,Y)*swap(Z,W); the difference inverse is D0.symm.trans(Lambda.symm).

All formulas keep arbitrary finite odd noncyclic H. For nontrivial H, n=card(H) is odd and at least three, and m=n-1 is at least two. Allowed coincidences between shifts and between parameters are retained. For trivial H, the definition constructs Subsingleton H and Unique H with default zero and transports the same fixed coefficient RCycle through AddEquiv.prodUnique.symm.

The construction formalizes the supplied native R-only four-source proof. Original HeadleyExtension cylinder, invariant, sum-lift and swap-join proofs are reused at their source; odd_box and doubling reuse the original Gordon normalization. The existing RStar product has a stronger premise and is not applied here. This is repo-derived formal composition, with no mathematical novelty claim. The four-slot audit remains unfinished under https://github.com/the-omega-institute/trureturing/issues/21215 for successor_ne_self, row_zero, shiftedSuccessor_apply, shifted_difference_spec, gauge_zero, chart_inr and joined_nonzero_cycle. Their current source owner and namespace are D5/S3/FiniteGroups/HeadleyCubeOddProduct and D5.S3.FiniteGroups.HeadleyCubeOddProduct, respectively; the issue uses their former HeadleyExceptionalRows owner, and each final declaration name is unchanged. No declared_validated registration is supplied. The arbitrary-subset, same-M, original-coordinate, coefficient-one parent and unrestricted AM remain open.

Original binary coordinates are right associated. e=100, b=010, c=001, t=110, p=011, k=111, l=101. The complete source row is 0,e,b,c,t,p,k,l. P has image row 0,b,c,t,p,k,l,e and agrees with (x0,x1,x2)↦(x2,x0+x2,x1). Q=P-id has image row 0,t,p,k,l,e,b,c. The reverse rows are the explicit inverses. P closes l→e and the closing Q-label is c.

Choose v nonzero, w=sigma(v), d=w-v=delta(v), q=sigma.symm(d). Then w,d,q are nonzero, w is unequal to v, sigma(q)=d and q is unequal to d. Shifts in source-row order are 0,v,w,v,w,0,0,v-q. No nonzero or distinct-shift hypothesis is imposed.

Let r_j=sigma^j(d), 0≤j<m. The bounded input orbit enumerates H minus zero exactly once, r_0=d and r_(m-1)=q. Define the original-coordinate block B(r)=((e,v+r),(b,w-r),(c,v+r),(t,w-r),(p,r),(k,-r),(l,v-q+r)).

The complete cyclic word is ((0,v),(t,w),(p,0),(k,0),(l,v-q),(e,v),B(r_0),…,B(r_(m-1)),(b,w),(c,v),(0,sigma(v)),(0,sigma^2(v)),…,(0,sigma^(m-1)(v))). Its last vertex is followed by its first. The seven nonzero K fibers omit exactly their shifts inside the blocks and the seven exterior vertices restore them. The zero K fiber is the given nonzero sigma orbit. The length is 1+5+7m+2+(m-1)=8n-1.

The six internal block labels, in order, are (t,d-2r),(p,-d+2r),(k,d-2r),(l,2r-w),(e,-2r),(b,v-q+2r). For j<m-1 the interblock label is (c,q+delta(r_j)).

Seam 1: (0,v)→(t,w), label (t,d).

Seam 2: (t,w)→(p,0), label (l,-w).

Seam 3: (p,0)→(k,0), label (e,0).

Seam 4: (k,0)→(l,v-q), label (b,v-q).

Seam 5: (l,v-q)→(e,v), label (c,q).

Seam 6: (e,v)→first B(d)=(e,w), label (0,d).

Seam 7: last B(q)=(l,v)→(b,w), label (k,d).

Seam 8: (b,w)→(c,v), label (p,-d).

Seam 9: (c,v)→(0,w), label (c,d).

The tail edges are (0,sigma^i(v))→(0,sigma^(i+1)(v)) for 1≤i<m, with sigma^m(v)=v. Their labels are (0,delta(sigma^i(v))). In particular i=m-1 is the real last-to-first edge (0,sigma^(m-1)(v))→(0,v), label (0,v-sigma^(m-1)(v)).

Bulk inventory by K label: 0 has delta(sigma^i(v)), 1≤i<m, omitting d among H minus zero, restored by seam 6. t has d-2r, r nonzero, omitting d, restored by seam 1. p has -d+2r, omitting -d, restored by seam 8. k has d-2r, omitting d, restored by seam 7. l has 2r-w, omitting -w, restored by seam 2. e has -2r, omitting zero, restored by seam 3. b has v-q+2r, omitting v-q, restored by seam 4. c has q+delta(r) for r outside {0,q}, omitting q,d, restored by seams 5,9. The last two are distinct because q is unequal to d; delta(q)=d-q. The affine rows use the actual doubling equivalence. These inventories are consequences of the consumed universal edge formula, not a second Lean counting construction.

Cuts, in X,Y,Z,W order: X=(0,v) has old image (0,w), old label (0,d), component C_H and new label (t,d). Y=(c,v) has old image (t,w), old label (k,d), component C_Z and new label (c,d). Z=(e,v) has old image (b,w), old label (t,d), component C_Z and new label (0,d). W=(l,v) has old image (e,w), old label (c,d), component C_N with offset q and new label (k,d). Lambda=swap(X,Z)*swap(Y,W). The W computation is v+sigma(q)=v+d=w.

For trivial H the cyclic vertices (e,0),(b,0),(c,0),(t,0),(p,0),(k,0),(l,0) have directed labels (t,0),(p,0),(k,0),(l,0),(e,0),(b,0),(c,0), closing included. For n=3, w=-v,d=v,q=-v,m=2. There are two blocks, one interblock edge and one tail closing edge. The uniform construction allows these coincidences.

References