Composition of Original Controls
Abstract
Arbitrary finite original controls admit exact chronological concatenation.
Theorem 1.1 (Absolute continuity of both original control coordinates).
Proof. Machine-checked in Lean as D5/S3/Quantum/Fibers/OriginalControlComposition.original_ac (✓ std3). ∎
Source. Repository-derived.
Commentary.
For every base b, real duration T and real functions k and chi, OriginalControl(b,T,k,chi) implies absolute continuity of both coordinates on the complete interval from zero to T. No ValidBase hypothesis or strict positivity of T is added. The original control predicate itself requires T>=0, continuity of both coordinates, strict membership of k in the open probability fiber, finite variation of chi, and either absolute continuity of both coordinates or a finite piecewise C1 partition with continuous rates on every closed piece.
The absolute-continuity alternative supplies the conclusion directly. In the finite piecewise C1 alternative, each continuous rate is integrable on its closed piece and agrees with the coordinate derivative in the interior. Truncate the partition at an arbitrary x in [0,T], apply the interval fundamental theorem on each truncated nonempty piece, and telescope the increments. Repeated partition times contribute zero. This gives f(x)=f(0)+integral from zero to x of f prime for each of k and chi. The derivative is interval integrable on the complete interval, so its integral primitive is absolutely continuous. Equality on the closed interval transfers this property to the original coordinate. The argument includes T=0.
Theorem 1.2 (Exact control and integral composition).
Proof. Machine-checked in Lean as D5/S3/Quantum/Fibers/OriginalControlComposition.concatenate_original (✓ std3). ∎
Source. Repository-derived.
Commentary.
The base b and its positive probability fiber J(b) are those of FiniteRectangleTransport. OriginalControl(b,T,k,chi) requires a finite nonnegative duration, continuity of both real controls on [0,T], k(t) in J(b), finite variation of chi, and either absolute continuity of both controls or continuous finite piecewise C1 controls. A finite piecewise C1 partition may contain repeated times; on every open piece both derivatives agree with continuous rates on the corresponding closed piece.
Write J(T,f,g)(x)=f(x) for x<=T and J(T,f,g)(x)=f(T)+g(x-T)-g(0) for x>T. The same relative second path is therefore applied after the first, with its real phase lift translated to the terminal phase. The probability coordinates agree at the join. Neither path is replaced or reparameterized.
In the formula below OC abbreviates OriginalControl. Prefix equality is equality on [0,T]. The scalar readout I(F,k,chi,L) denotes the integral from zero to L of F(k(t))*chi prime(t). All functions F continuous on the original open probability fiber are included. The theorem asserts the original control condition, both prefix equalities, both exact tail equations, the exact real phase increment, and additive scalar readouts.
A finite piecewise C1 coordinate is absolutely continuous on its complete finite interval. To see this, its derivative is integrable on each piece. Truncating the partition at any intermediate time, applying the interval fundamental theorem on each nonempty truncated piece, and telescoping reconstructs the coordinate as its initial value plus the integral of its derivative. Empty pieces contribute zero. The integral primitive is absolutely continuous. This covers both original alternatives and pairs using different alternatives.
For two absolutely continuous coordinates, paste the derivatives at T and integrate. The resulting primitive equals the first coordinate on [0,T] and the translated second coordinate on [T,T+S]. It gives continuity at the join and finite variation. Strict probability support follows separately from the original first and second paths. The additive readout follows by splitting the interval integral at T, using local derivative equality on each open piece, and translating the second integration interval. Junction values do not affect the integral.
Every given original control prefix on [0,T] extends to a base/phase loop of any prescribed signed integer winding m. First concatenate the unit affine probability leg from k(T) to k(0), keeping chi equal to chi(T). Then concatenate a unit leg at k(0) whose relative phase increment is 2pim-(chi(T)-chi(0)). Both probability endpoints lie in the open fiber, and its convexity keeps the new legs inside it. Affine controls are absolutely continuous with finite variation. Two applications of concatenate_original give an original control on [0,T+2], exactly equal to both original controls at every point of [0,T]. Its final height is k(0) and its real phase increment is 2pim. This statement retains the actual control prefix, including either original regularity alternative. It also preserves every prepared integral state lift: for every initial five-vector theta, every s in [0,T] and every mode i, theta(i)+integral from zero to s of w(K(t))(i)*C prime(t) equals theta(i)+integral from zero to s of w(k(t))(i)*chi prime(t). Indeed K=k and C=chi on the entire closed prefix. At every interior time the control phases agree in a neighborhood, so EventuallyEq.deriv_eq identifies their derivatives. The intervalIntegral.integral_congr_uIoo identity then gives equality of the transported integrals, including s=0 and s=T. Thus the construction preserves the actual integral lift throughout the given prefix, with arbitrary preparation phases.
Endpoint constraints alone do not certify a proposed intervening state path. On [0,1], keep k at any allowed initial height and keep chi constant, but propose the increment h(t)=sin(pit)^2(1,1,0,1,1). Its two endpoint increments vanish. At every time it has zero middle coordinate, both wall increment equalities, and zero direction charge. Nevertheless its first phase coordinate has strictly positive derivative at t=1/4, as follows from the chain rule and the positive sine and cosine of pi/4. The original law with constant chi requires that derivative to vanish. Thus this proposed path violates the original ODE and is excluded from the lawful histories, despite matching their endpoint and wall constraints.
Both zero durations are included. For a pair of loops at one fixed base height, the probability coordinate still begins and ends at that height. If the two exact real phase increments are 2pim and 2pin, the resulting winding is m+n. Taking F to be each original phase-weight component gives additive five-coordinate residuals; taking F(k)=k gives additive signed area. A compatible initial five-phase lift stays compatible under the original transported integral lift. These consequences retain the actual arbitrary controls and their real winding, rather than only their endpoint circle classes.
For the original current-ray query, let h be the actual integral increment of any OriginalControl. The integrated charge identity gives charge(h)=chi(T)-chi(0). Therefore k(T)=k0 and exp(icharge(h))=1 hold exactly when the original periodic base closes with an integer winding. Equal middle-positive projective rays force equal heights and equal component circle phases; additivity of the exponential makes exp(icharge(h)) the same for both. This predicate is consequently a function of the current ray and fixed preparation, conditional on the original law. It does not establish that a proposed intervening path obeyed that law.
The literal period lattice also determines exactly which integer windings can return the initial ray. For an increment h in U(b) whose coordinates are 2pi times integers, the charge is an integer multiple of 2pi. On the double wall, h0=h13 and h1=h3 give charge(h)=2*(h0-h1), so the winding is even. Conversely winding 2n is realized by h=(2pin,0,0,0,2pin). Off Eminus, h=(2pim,0,0,0,0) realizes every integer m and respects any Eplus equation. On Eminus alone, h=(0,-2pim,0,0,0) does so instead. The exact prepared finite-prefix construction at terminal height k0 realizes each of these increments by an actual Admissible polygon and OriginalControl, for every fixed preparation theta and initial real phase c0. Its terminal control increment is exactly 2pim, its actual prepared transport integrals are theta+h, and the middle-positive projective ray is the initial one. Thus the ray-returning winding subgroup is Z off the double wall and 2Z on it. Taking m=1 off it or m=2 on it gives the same current ray as a constant history and a different real winding record. At k=k0, every h in U(b) with exp(icharge(h))=1 has charge(h)=2pim for an integer m, by exact exponential periodicity. The prepared finite-prefix construction at k0 supplies an actual original loop with that same h and real winding m. Thus restricting the current source by this predicate recovers the original loop phase domain. On the double wall charge(u,v,0,v,u)=2*(u-v). Its exponential is one exactly when exp(i*(u-v)) is one or minus one, giving precisely alpha=0 or pi as circle classes. This restriction concerns loop endpoints; restricting actual histories further to zero winding is a separate operation. A separate ambiguity fixes even the full terminal lifts. Choose any second legal height k1 distinct from k0, retain every arbitrary initial phase and the real control phase c0, and use the polygon (k0,c0,theta),(k1,c0,theta),(k0,c0,theta). Its two probability legs are lawful; its terminal height, real control phase and every phase integral agree with the constant history, while its height at time one differs. Thus the terminal ray, and even all real terminal increments, omit the intervening path.
Applications on the original open-prefix source
The applications below concern the original five-mode model of AURIC_FIB_ATOM_PROBABILITY_PHASE_TRANSPORT_AND_HOLONOMY, chapter 8, with one fixed positive normalized base, one fixed legal initial height, arbitrary fixed preparation phases and the original absolutely continuous or finite piecewise C1 control class. They reuse FiniteRectangleTransport.finite_rectangles_realize, FiniteRectangleTransport.polygon_admissible, FiniteRectangleTransport.weight_compatible, OriginalControlComposition.concatenate_original and the pinned Mathlib results identified in each derivation. They are application exposition, with no separate mathematical declaration or new-content admission claim. The composition theorem above does not by itself certify the complete application.
Full P1–P12 source/object fidelity and chapter 8 completeness remain outstanding. The obligations are not replaced by the narrower affine-update obstruction: they include the prepared finite-prefix realization, preservation of the actual prefix and lift, winding and ray-return distinctions, current-ray observation and inverse, literal lattice and projective topology, native smooth charts and output embedding, full-family affine capacities, original double-wall fields and commutator, sphere correspondence, descended contact form and its pullback, lawful continuation, and the observer/harmonic interface boundary. The derivations below retain their complete assumptions and parameter correspondence. Missing independently bound exact applications for the projective/manifold and contact bridges, and the all-family capacity claims, remain verification obligations; a source-level derivation is not a compiled Lean proof of those bridges or completion of chapter 8.
Common lawful probability command and affine-response obstruction
In full quantified form, for every real Z,s,a,b with 0<Z<1, s nonzero, a<b and Legal(Z,s,a,b) as expanded below, the base B(Z) is ValidBase, Commands(Z,s,a,b) holds and Affine(Z,s,a,b) fails. Every starting height in (a,b), every initial real control phase and every five-component initial phase vector is retained. The polygon equality is on [0,1]; both derivative equalities quantify every real time. The excluded update allows every real linear map from R4 to R4 and every offset, fixed across the whole interval and both independent real phase parameters.
Fix 0<Z<1, put r=1-Z, and use the original double-wall base B(Z)=(r/2,r/2,Z). The mode order is (0,1,2,3,13), with mode 13 at index 4 and the positive middle mode at index 2. Its probabilities are (k,r/2-k,Z,r/2-k,k). For any real representatives alpha and beta of two independent phase circles, response(r,Z,k,alpha,beta) is the four-vector (2sqrt(k(r/2-k))cos(alpha),2sqrt(k*(r/2-k))sin(alpha),2sqrt(kZ)cos(beta),2sqrt(kZ)*sin(beta)). These are the two original doubled pairs, with alpha=u-v and beta=u. Real representatives here only parameterize the circles; no global angle chart is asserted.
Let s be any nonzero real displacement and let (a,b) be any nonempty open interval such that 0<k<r/2 and 0<k+s<r/2 for every k in it. Legal(Z,s,a,b) abbreviates exactly these four inequalities with that universal quantifier. Commands(Z,s,a,b) abbreviates the following full conclusion, universally in k in (a,b), the initial real control phase chi and every five-component initial phase vector theta. The controls K(t)=k+st and C(t)=chi obey OriginalControl(B(Z),1,K,C). The actual polygon q with vertices (k,chi,theta) and (k+s,chi,theta) obeys Admissible(B(Z),1,q). For every t in [0,1], q(t)=(k+st,chi,theta). For every real t, HasDerivAt(K,s,t) and HasDerivAt(C,0,t). Thus the same open-loop velocity command (s,0) applies to every legal starting height and all independent starting phases.
The probability segment is a convex combination of its two legal endpoints and stays strictly inside the original interval. Both controls are affine, hence absolutely continuous, and C has zero total variation. The unchanged polygon_admissible theorem of FiniteRectangleTransport supplies the actual state ODE, probability derivative law and integral increment on the single leg. Its LawfulLeg hypothesis holds because both phase increments are zero. Arbitrary initial phases are retained. Choosing the initial relation lift consistently with theta therefore gives an original lawful continuation, including for every fixed preparation phase.
Affine(Z,s,a,b) below means that there exist one real linear map D from R4 to R4 and one offset c in R4, fixed for the complete interval and both phase circles, such that response(r,Z,k+s,alpha,beta)=c+D(response(r,Z,k,alpha,beta)) for every k,alpha,beta. No regularity, block restriction or zero-offset assumption is placed on D and c.
To prove its negation, keep alpha fixed and subtract the responses at beta=0 and beta=pi. Their difference is 4sqrt(kZ) times the third coordinate axis. This cancels the offset and every possible contribution from the first pair. The third output coordinate consequently forces sqrt((k+s)Z)=sqrt(kZ)q, where q is the third coordinate of D applied to that axis, a single real number independent of k. Squaring is legitimate because k and k+s are positive and Z>0. It gives (k+s)Z=kZq^2. Apply this equality at k=(2a+b)/3 and l=(a+2b)/3. Both heights belong to (a,b), and k<l. Subtracting forces q^2=1; substitution then gives s*Z=0, contradicting s nonzero and Z>0. This argument covers arbitrary offset and mixing across all four coordinates.
Prepared observations and the full current-ray domain
The negative state convention produces the original positive sine orientation. If psi(i)=sqrt(p)exp(-itheta) and psi(j)=sqrt(q)exp(-iphi), then 2conjugate(psi(i))psi(j)=2sqrt(pq)exp(i(theta-phi)) for nonnegative probabilities. Its real and imaginary parts are the ordered doubled cosine and sine outputs. Its squared complex norm is 4pq. In the original 02 block, p=p0=1-Z-X-Y+k and q=Z>0. Hence k=norm(y02)^2/(4Z)-(1-Z-X-Y), for every interior current height and every fixed preparation and current phase increment. This recovers the height without an angle choice, including either wall and their intersection. For equality of the complete five ordered pairs, this height formula first forces equal heights. Positive amplitudes then cancel, and the fixed preparation rotations cancel as well. The 02 edge determines exp(ih0), since h2=0; the 01 and 03 edges determine exp(ih1) and exp(ih3); the 1,13 edge determines exp(i*h13). Conversely equal height and these four circle values give identical outputs. This is exactly the equality criterion for the actual middle-positive Projectivization representatives. Thus the unchanged ten expectations separate every current ray, with arbitrary fixed preparation phases and every wall regime. The native smooth embedding follows from the explicit amplitude reconstruction and local charts described below.
For an arbitrary OriginalControl, define theta(t)=thetaInitial+the integral of phaseWeight(k)chi prime from zero to t. The integrated law gives h2=0, charge(h)=chi(T)-chi(0) and both conditional wall increment equations, with legal terminal height. The representative used above is exactly exp(ithetaInitial(2)) times this original negative-exponential state at T. This is one constant gauge change, independent of height and history. Each original doubled coherence pair is exactly twice conjugate(psi(i))*psi(j) for this transported state and has the positive sine orientation. Thus the ray and observation equalities apply directly to every original history with arbitrary fixed preparation; they do not identify the source with the history or its real lifted record.
The response coordinates have an exact curved coordinate image. Write a=z(0)^2+z(1)^2 and b=z(2)^2+z(3)^2. For Z>0 and 0<k<r/2, the response gives a=4k(r/2-k), b=4kZ, hence 0<b<2rZ and a=rb/(2Z)-b^2/(4Z^2). Conversely, every real four-vector with these two conditions has k=b/(4Z) in (0,r/2). The identity for a then becomes a=4k(r/2-k). Regard each coordinate pair as a complex number and choose its complex argument to obtain alpha and beta; norm times cosine and sine of the argument recovers the pair exactly. These real arguments are existence witnesses, not a global smooth angle chart. For any such k,alpha,beta, take u=beta and v=beta-alpha and the original increment (u,v,0,v,u). The exact prepared finite-prefix construction realizes it from the one fixed initial height and arbitrary preparation. The original five ordered output pairs equal the fixed prepared double-wall decoder applied to this same four-vector. Thus every point of this curved image is actually reachable in the original source.
Literal phase quotient, inherited topology and smooth reconstruction
The next correspondences require the actual inherited projective topology, the literal period quotient, native manifold charts and native immersion/embedding bridges. Their complete derivations are retained here; their independent exact source/object verification remains outstanding.
For the actual variable-probability Projectivization over C of five complex amplitudes, use psi(i)=sqrt(p(i))exp(-i(thetaInitial(i)-thetaInitial(2)+h(i))), with h(2)=0. The middle entry is the same positive sqrt(Z) at every height and fixes any scalar identifying two such rays to one. Squared modulus at mode13, index4, then forces equality of heights. Every remaining amplitude is nonzero; cancellation gives equality of all Circle.exp(h(i)). Conversely equal height and those circle values give identical representatives. Pinned complex-exponential periodicity identifies this condition with h(i)-hPrime(i)=2pin(i) for integer n(i), in every coordinate. When both increment vectors belong to U(b), their difference belongs to U(b), so this is exactly the lattice U(b) intersect 2piZ^5. Arbitrary preparation phases cancel in this comparison. Give U(b) its inherited real-vector topology and quotient it by exactly this literal period lattice. Off both walls, coordinates (h0,h1,h3,h13) are a homeomorphism U(b) to R4. On Eminus alone use (h0,h1,h3), on Eplus alone use (h0,h1,h13), and on both use (h0,h1); the inverses repeat exactly the applicable increment coordinates and insert the zero middle coordinate. Coordinatewise Circle.exp is a surjective continuous open map, by the pinned circle covering map and finite-product open-quotient theorem. Its kernel on U(b) is exactly the displayed lattice relation, so the quotient-map homeomorphism gives the full product of four, three, three or two circles respectively, with its quotient topology. No finite quotient is added. These facts establish the literal topological phase quotient. The local phase exponential charts below give its smooth identification with the inherited projective source.
The source topology is the inherited projective quotient topology. Give Projectivization over C of five complex amplitudes the quotient topology of nonzero vectors under nonzero scalar multiplication. The domain where the middle component is nonzero is open: its preimage under the quotient map is exactly the open nonvanishing condition on component2. On this domain the four normalized component ratios form a homeomorphism to C4. More generally, at any chosen index i the inverse chart inserts component1 at i and the prescribed ratios at all other indices; scale cancellation and the restricted quotient-map continuity theorem prove both inverse identities and continuity. Multiplying the normalized ratios by sqrt(Z) recovers the unique middle-positive representative used here. For the reachable family, its mode13 squared modulus recovers k continuously. Each original nonzero component then recovers its phase circle by conjugating the component, dividing by its norm and multiplying by the fixed negative preparation phase. These inverse formulas identify the actual projective source, with its inherited topology, with J(b) times the group-constrained five-circle domain. That circle domain has middle1, with z0=z13 on Eminus and z1=z3 on Eplus. The explicit independent-circle coordinates give products of four, three, three or two full circles. Conversely, taking component arguments gives real increments in U(b), including exactly the applicable wall equalities and middle zero, and reconstructs the original negative-exponential state. Thus this topological source carrier is exactly the original current-ray carrier already realized by the finite prepared controls. Combining with the literal lattice quotient identifies both topological descriptions of the same source, without an extra finite quotient. The smooth atlas and native embedding are obtained from the same phase lifts as follows.
Let W(b) be the real submodule of five increments with middle zero and the applicable two wall equalities. The component projections give continuous linear equivalences to R4, R3, R3 or R2; no hypothesis equates preparation phases. Coordinatewise Circle.exp maps W(b) onto the constrained phase-circle domain and is a local homeomorphism, by the pinned circle covering map and finite products. On J(b) times W(b), the original nonmiddle amplitudes are sqrt(p_i(k))exp(-i(eta_i+h_i)). This map is real analytic at every legal height. Its actual Frechet differential is injective: after cancelling the nonzero exponential, a zero amplitude differential has real part dp_i/(2*sqrt(p_i)) and imaginary part -sqrt(p_i)*dh_i, so both vanish. Mode13 gives dk=0, all nonmiddle modes give dh_i=0, and dh_2=0 holds in W(b). The analytic inverse-function theorem applied to a thickening by a linear complement supplies actual local immersion normal forms. This proves native IsImmersionAt, rather than substituting derivative injectivity for that predicate. Local inverse charts of the phase exponential, paired with the open height chart, cover the source. Their transitions are smooth because composing a continuous transition with the target amplitude immersion gives the source amplitude parametrization; the pinned immersion smoothness criterion then applies. Transporting these charts through the established projective-source homeomorphism preserves its inherited topology. In these actual charts the middle-positive amplitude map has the same immersion normal form. Finite-dimensional complements have the constant codimension, giving native IsSmoothEmbedding into the rescaled middle projective chart. The chart-model dimensions are therefore 5,4,4,3 respectively. The two wall equations hold together exactly when X=Y=(1-Z)/2. This is the three-dimensional condition within the declared fixed-mean, full-support model.
There is also a smooth inverse using the unchanged coherence menu without a global angle choice. Write the five original ordered output pairs as complex numbers y01,y02,y03,y1,13,y3,13, and let a_i denote the nonmiddle amplitudes in the positive-middle representative. Then a0=conjugate(y02)/(2*sqrt(Z)), a1=sqrt(Z)y01/y02, a3=sqrt(Z)y03/y02, and a13=y1,13conjugate(y02)/(2sqrt(Z)*conjugate(y01)). These are exact identities for the original negative state exponential and positive sine output. The denominators are nonzero throughout the source. The formulas are real analytic on their nonvanishing domain. Their composition with the original polynomial coherence map is the identity on the nonmiddle amplitudes. Differentiating this identity makes that polynomial map injective on tangent directions. Composing with each original source-lift differential therefore remains injective; the same analytic immersion constructor and actual source charts give a native smooth immersion of the source into the five ordered complex pairs. The continuous reconstruction and the already embedded amplitude source give a topological embedding, hence a native IsSmoothEmbedding of this original output map. Complex notation identifies each ordered pair with its real and imaginary parts and does not replace the original Euclidean output metric. These inverse formulas provide the smooth reconstruction on the positive image in every wall regime and for every fixed preparation.
Prepared decoders and full-family affine capacities
The following lower bounds require all phases in each stated slice to be realized by the same original prepared finite-prefix construction, and the upper bounds require one decoder on the complete variable-height source. No fixed-height or closed-loop restriction discharges those full-family obligations.
The original double-wall decoder sends a four-vector z=(za,zb) to five ordered pairs (za,zb,za,Jza,Jza), with J=diag(1,-1). For any v,w its squared L2 distance is 4*((v(0)-w(0))^2+(v(1)-w(1))^2)+(v(2)-w(2))^2+(v(3)-w(3))^2. The ten outputs live in EuclideanSpace over the product of five edges and two real coordinates. Rotating each output pair by its arbitrary fixed preparation phase preserves the sum of the ten squares, because cos(delta)^2+sin(delta)^2=1. Thus the same exact identity holds for the original prepared outputs and the decoder has Gram matrix diag(4,4,1,1). This uses the original output Euclidean metric and imposes no new metric on the current source.
The original preparation acts by one fixed real orthogonal rotation on each doubled pair. Removing this rotation gives, on Eminus, the ordered complex pairs (zAlpha,zBeta,zGamma,conjugate(zAlpha),conjugate(zGamma)); on Eplus it gives (zAlpha,zBeta,zAlpha,zGamma,zGamma). These are real linear decoders from three complex coordinates, equivalently six real coordinates. They are fixed across every current height and have zero offset. The Eminus identities use p0=p13 and h0=h13; the Eplus identities use p1=p3 and h1=h3. Thus they are distinct decoders, and impose no equality on arbitrary preparation phases. On the double wall both identities give (za,zb,za,conjugate(za),conjugate(za)), with two complex coordinates. Including the fixed preparation rotations recovers exactly the same original five ordered doubled-coherence pairs. Complex notation here packages each ordered real cosine/sine pair and does not change the original ten-dimensional Euclidean metric.
For the no-wall phase domain, take four independent unit circles in the order (h0,h1,h3,h13). The five original edge-character exponents are (1,-1,0,0), (1,0,0,0), (1,0,-1,0), (0,1,0,-1), and (0,0,1,-1). Adjoin their five negatives and the zero exponent. The resulting eleven complex multiplicative characters are distinct: evaluating at the four points with one coordinate i and the others one separates these exponent vectors, whose entries are zero, one or minus one. The pinned linearIndependent_monoidHom theorem gives their complex functional independence. Applying span_flip_eq_top_iff_linearIndependent then gives full complex span of the eleven-coordinate evaluation vectors. This is an exact application on the full phase torus. For a real relation among the constant and the ten real sine/cosine coordinates, use coefficients (aCos-iaSin)/2 on each character and (aCos+iaSin)/2 on its inverse. Their sum is the corresponding real relation, and complex independence forces every real coefficient to vanish. At any fixed legal height, each original amplitude is positive. Divide by that amplitude and its arbitrary fixed preparation rotation to recover exactly these characters. The circle arguments give real increment representatives with middle zero and no wall constraints. The exact prepared finite-prefix construction realizes every such representative from the common preparation, so this independence concerns the original reachable slice.
On Eminus alone, use independent circle angles alpha,beta,gamma and increments (beta,beta-alpha,0,beta-gamma,beta). The first three normalized original edges give exactly these three circles. On Eplus alone use (beta,beta-alpha,0,beta-alpha,beta-alpha-gamma); edges 01,02,1-13 give the three circles. On both walls use (beta,beta-alpha,0,beta-alpha,beta); edges 01 and 02 give two independent circles. These representatives obey precisely the applicable increment equations. At any fixed legal height their amplitudes are positive, and the prepared finite-prefix construction realizes the whole slice. The constant together with the real and imaginary coordinates on g independent circles are real linearly independent: compare the point with all circles one with the point obtained by changing one circle to minus one, then to i. These comparisons force its cosine coefficient and sine coefficient to vanish; evaluation then forces the constant coefficient to vanish. This yields six independent real output coordinates plus the constant on either single wall, and four plus the constant on both.
For every natural n, arbitrary encoder z into Rn, fixed real linear decoder D and arbitrary fixed offset c, augment an input by one scalar coordinate. The linear map sending (t,w) to (t,tc+Dw) contains all augmented output evaluation vectors in its range. Independence of the constant and m output functions makes those evaluations span R^(m+1). Surjectivity and the finite-dimensional rank bound give m+1<=n+1, hence m<=n. Apply this after the fixed-height normalization and edge projections above, or after the no-wall character normalization. The argument allows arbitrary mixing and nonzero offsets and uses no regularity or linearity of the encoder. The explicit fixed decoders supply zero-offset upper bounds 10,6,6,4 in literal real coordinates, while the realized slices give the same lower bounds. Consequently the whole variable-probability prefix capacities are 10 off both walls, 6 on either single wall and 4 on both. These same bounds hold with the encoder defined directly on the actual Projectivization carrier. Let the source be the set of middle-positive projective rays represented by legal heights and increments in U(b). Select any legal representative of each ray. The ray-equality and original-output equivalences prove that its ten real outputs are independent of that selection. Evaluating the displayed encoder on the selected representative gives one encoder on rays and the same fixed zero-offset decoder. Conversely, composing any encoder on rays with the representative-to-ray map and applying the real lower bound gives the same bound for every n, decoder and offset. The exact prepared finite-prefix construction realizes every member of this actual projective source by an Admissible polygon and OriginalControl, with the prescribed arbitrary preparation and initial real control phase. Thus the capacity statement concerns the actual reachable rays and the original ten real outputs. This affine capacity and the chart-model intrinsic dimension are distinct properties of this same source.
Original finite rectangles, native fields and sphere correspondence
The native-field, sphere and contact applications require the original control-to-tangent correspondence, the inherited source charts, the standard sphere atlas and the descended differential-form identities on the same source. Coordinate formulas alone do not discharge these bridges.
For every legal k,k+s and every real A, the original singleton rectangle has four finite affine legs and returns both k and the real relation control phase. On the double wall the original phase weight is (1/2-k/r,-k/r,0,-k/r,1/2-k/r), so its exact increment is (-sA/r,-sA/r,0,-sA/r,-sA/r). Translating the initial real control phase by any c0 preserves OriginalControl, and adding the same arbitrary preparation to the actual transported integrals gives these increments on the original prepared state. For s nonzero and any desired common phase t, take A=-r*t/s; the finite rectangle then realizes exactly (t,t,0,t,t). Both signs of s and A are allowed whenever the two heights are legal.
Along the real local flow (k,u-t/r,v-t/r), the original 02 coherence pair, with its fixed preparation phase delta=thetaInitial(0)-thetaInitial(2), is exactly 2sqrt(kZ)exp(i(delta+u-t/r)). Its actual derivative is this complex pair times -i/r, and its Euclidean norm is 2sqrt(kZ)/r, strictly positive at every legal height. Complex norm here is the original Euclidean norm of the ordered real pair. The middle reference stays fixed and positive. The actual source charts have identity transition differentials: their phase lifts differ by locally constant periods and their height coordinate is unchanged. Consequently their tangent trivializations identify the tangent model with R times W(b). On the double wall the continuous linear coordinate equivalence sends (dk,dh) to (dk,dh0,dh1). Under this equivalence the original velocity (a,cphaseWeight(k)) is exactly aP+c*Q, with P=(1,0,0) and Q=(0,1/2-k/r,-k/r). The actual Mathlib manifold Lie bracket of these fields is (0,-1/r,-1/r), transported back by that same equivalence. The two fields are independent at every actual source point, their span has real dimension two, and adjoining their bracket gives three independent tangent vectors. Thus this is the native distribution of the original ODE on the inherited projective source. The finite rectangle and the original02 derivative above refer to those same fields; no limiting bracket or coordinate-only substitute is needed.
The two-amplitude correspondence retains all fixed preparation phases. Put eta(i)=thetaInitial(i)-thetaInitial(2). The fixed plus vector has entries exp(-ieta(0))/sqrt(2) and exp(-ieta(13))/sqrt(2) at modes 0 and 13 and zero elsewhere. The fixed minus vector has the analogous entries at modes 1 and 3. In the original complex Euclidean five-mode space they are orthonormal: their supports are disjoint and each squared norm is one. With zPlus=sqrt(2k/r)exp(-iu) and zMinus=sqrt(1-2k/r)exp(-iv), the same middle-positive original state is exactly sqrt(r)(zPlusplus+zMinus*minus)+sqrt(Z)*middle. The scalar identities sqrt(r)sqrt(2k/r)/sqrt(2)=sqrt(k) and sqrt(r)sqrt(1-2k/r)/sqrt(2)=sqrt(r/2-k) give the component equality. The existing two-amplitude sphere calculation puts precisely these two nonzero complex amplitudes on the unit sphere and recovers k,u,v from every sphere point with both amplitudes nonzero. Every actual point of this open unit sphere is attained from the same fixed legal initial height, arbitrary preparation and initial real control phase: recover k,u,v by the sphere inverse, then apply the prepared finite-prefix construction to (u,v,0,v,u). Its original Admissible polygon and OriginalControl have exactly these terminal transported phase integrals, and the original five-mode state decomposes using that very sphere point. On the actual projective source, extracting these two amplitudes is a fixed real linear map of the middle-positive nonmiddle amplitudes: multiply components0 and1 by their fixed positive preparation rotations and divide by sqrt(r/2). The inverse inserts the two amplitudes with those original negative preparation phases. These maps restrict to mutually inverse smooth maps between the actual source and the open subset of the standard Euclidean unit3-sphere where both components are nonzero. Smoothness uses the native source immersion and the actual standard sphere atlas, so the correspondence is a native diffeomorphism, with its inherited topologies on both sides. The original prepared controls realize every sphere point as above. This preserves their simultaneous phase, which changes the bottom modes relative to the measured middle reference. It supplies neither a Hopf quotient nor additional free controls.
Contact form on the actual source and the remaining interfaces
On the real coordinate lift x=(k,u,v), lambda(x) is the continuous alternating one-form 2kdu+(r-2k)dv. Its actual exterior derivative, using the normed-space differential-form operator, evaluates on vectors a,b as 2(a_k(b_u-b_v)-b_k*(a_u-a_v)). This follows by differentiating the coefficients and alternating the two derivative slots. The actual exterior product is the alternating tensor product of this one-form and its exterior derivative, scalarized by real multiplication. Reindexing its slots to (dk,du,dv) and using the factor 1/(1!2!) in full alternatization gives, on every three tangent vectors, 2r times their determinant. This identifies the computed product with the pinned AlternatingMap.domCoprod operation and proves lambda wedge d lambda=2rdk wedge du wedge dv, nonzero for r>0. Together with the original local kernel computation, the same one-form has precisely span(P,Q) as its kernel. On the actual complex Euclidean two-amplitude space, the standard continuous alternating one-form is alpha(z)(w)=Im(inner_C(z,w))=Im(conjugate(zPlus)wPlus+conjugate(zMinus)wMinus). For the original negative-exponential map F(k,u,v)=(zPlus,zMinus), its actual normed-space pullback alpha(F(x)) composed with the Frechet derivative of F evaluates to -(2kdu+(r-2k)dv)/r at every legal height. Differentiating sqrt(p)exp(-it) shows that the imaginary part of conjugate(amplitude) times its derivative is -pdt; the real radial derivative contributes zero. The two probabilities are 2k/r and 1-2k/r, giving the stated negative sign and factor. On the actual projective source, define lambda by transporting this one-form through the tangent coordinate equivalence. It equals the original probability-weighted phase form sum_i p_idtheta_i, with the middle phase fixed. Its kernel is exactly the native span of P and Q. In every actual source chart its pullback is the displayed coordinate form composed with the same linear equivalence. The actual extDeriv_pullback theorem, together with the identity chart differentials, identifies the exterior derivative of that chart pullback with the descended two-form. The actual alternating product domCoprod therefore evaluates to 2*r times the determinant of the three tangent vectors in (dk,du,dv) coordinates, and a coordinate basis gives a nonzero value. These chart identities establish descent through the literal phase periods. Finally the actual manifold derivative of the sphere-amplitude map pulls the ambient standard form back to -lambda/r on every actual source tangent vector. Restricting that form to the native sphere gives the same pullback. Thus the negative sign, exterior derivative, contact kernel and nonvanishing product hold on the inherited projective source, as well as on its real local lifts.
At the fixed initial height, imposing exp(i*charge(h))=1 recovers exactly the original loop phase domains. On the double wall it restricts alpha to the circle classes 0 and pi. The original closed-loop affine capacities remain 6,4,3 in their respective regimes, as established in the FiniteRectangleTransport exposition; the actual zero-winding history restriction retains capacity2. A nonzero even winding can have the same endpoint but is excluded from that history restriction. The prefix values 10,6,4 concern a different domain, without averaging over heights or controller records. Neither the three-dimensional current-ray manifold nor its contact plane field selects the fixed means. The observer and harmonic interfaces still require their own common linear source, calibrated distance, ordered responses, rotational intertwining and closure under all declared generators. These conditions do not follow from the present nonlinear source and plane field. No physical spatial dimension, memory or acquisition bound follows from them.
Classical provenance and the continuation boundary
The classical tools have explicit correspondences here. Keith Conrad, Linear Independence of Characters, Theorem2.1, concerns distinct homomorphisms to the nonzero complex numbers; its pinned Lean supplier is linearIndependent_monoidHom applied to the exact eleven no-wall characters including the trivial character. John Etnyre, Introductory Lectures on Contact Geometry, arXiv math/0111118v2, section2, Example2.12 and equation(7), uses the unit-sphere form sum_j(x_jdy_j-y_jdx_j). The actual ambient form and negative-exponential pullback above use that precise convention. These are applications of classical results to the original five-mode source, without a worldwide novelty claim or an additional physical realization premise.
In particular the middle pair changes by the deterministic factor sqrt((k+s)/k). It remains determined by the current state and the specified command. The result concerns the failure of a single affine update in these four current coordinates; it supplies no additional control, distribution on histories, acquisition claim or linear predictive interface. The finite prefix construction, the inherited projective-source charts and the native original-output embedding refer to this same common preparation and original control law.
These applications preserve the full original source domain and its unfinished obligations. In particular, the current four-coordinate affine-update obstruction does not establish the projective/manifold, contact, capacity or later observer/harmonic bridges. No metric, physical spatial dimension, predictive linearity, memory bound or acquisition bound is inferred from their source-level exposition.