Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

The Actual Boolean Obstruction and Original Upper Contract

Abstract

One actual Boolean addition family defeats every subcritical exponent alongside the complete original upper bound.

Theorem 1.1 (Exact integer scaling of the attained rational dual).

Proof. Machine-checked in Lean as D5/S3/Observer/Separation/FixedSkeletonWeightedInclusion.integer_optimal_certificate (✓ std3). ∎

Source. Repository-derived.

Commentary.

For finite nonempty A,B and finite Z, phi:A times B -> Z is onto its effective alphabet. The preserved real/rational primal-dual theorem supplies the actual nonnegative optimal rational w. Its finite matrix denominator gives an integer L>0 and natural ell_z, with sum_z ell_z=L tau and every actual row sum at most L. R_x is the actual image phi(x,B). Zero weights are included. No rationality, optimum value or denominator is assumed.

Theorem 1.2 (Actual Boolean signatures at every original layer).

Proof. Machine-checked in Lean as D5/S3/Observer/Separation/FixedSkeletonWeightedInclusion.raw_layer_signature_bounds (✓ std3). ∎

Source. Repository-derived.

Commentary.

R and S index the original designated and ordinary pairs. Fix an ordinary k, N_k its strict designated containment neighborhood, and the actual product selector phi_N on XP=product_N X_i, YP=product_N Y_i, ZP=product_N Z_i. Let m>=2, L be natural and ell:ZP->Nat have sum_z_in_phi_N(x,YP) ell_z<=L for every actual x. K is the heterogeneous table product_z ZMod(m^ell_z). Only k’s two endpoint alphabets and effective output are K; its map is addition transported through the original conditional alphabet equivalences. Every other ordinary alphabet is Bool with fixed ignored XOR. The total scalar task is decide((a+b)_(phi_N(x,y))=0). kappa(t) uses the actual full labelled suffix at raw cut t. For all natural t: before a_k, kappa<=card XP; between a_k and b_k, kappa<=card XPm^L; after b_k, kappa<=card XPcard YP*m^L. The middle signature retains x and a restricted to that actual row. The final signature retains x, the observed designated Y extension and positive-weight zero flags. Zero-weight cells have modulus one and forced true flags. Ignored reads do not enlarge these signatures. The row condition here is discharged internally by the attained certificate in the final theorem.

Theorem 1.3 (One common normalized suffix distinguishes all tables).

Proof. Machine-checked in Lean as D5/S3/Observer/Separation/FixedSkeletonWeightedInclusion.normalized_table_injection (✓ std3). ∎

Source. Repository-derived.

Commentary.

Use the same original R+S skeleton, fixed designated effective onto maps and constructed one-addition-block Boolean family. At the actual normalized half cut immediately after k’s first label, lowerPrefix(a) varies exactly that table input and fixes every other read endpoint. All selectors in N_k remain unread. Given two distinct tables, choose a differing selector coordinate z; onto product designated maps realize z in a common suffix, whose second table is -a. The actual scalar response for a is true and the other response is false. The ResponseMap(lowerPrefix) notation denotes a -> the actual normalized response at lowerPrefix(a). L denotes <= and LT denotes <. This map is injective on K, hence m^(sum ell_z)<=Wcn for nonzero m. Full designated tuples and full selected tables are identified before dependent coordinate evaluation; input construction uses the same inverse equivalences.

Theorem 1.4 (The literal minimum and the attained least uniform real exponent).

Proof. Machine-checked in Lean as D5/S3/Observer/Separation/FixedSkeletonWeightedInclusion.original33_bound_and_boolean_obstruction (✓ std3). ∎

Source. Repository-derived.

Commentary.

R,S are finite nonempty original labelled pair index types, and the fixed oriented skeleton is arbitrary. For every finite nonempty designated endpoint family and fixed onto designated maps, all ordinary endpoint alphabets/maps and the finite nonempty output type O and total outer task G vary. Each ordinary map has some surjective row and some surjective column. Define tau,T,D,Theta and actual labelled widths as above. Allowed(s,psi) abbreviates exactly these assumptions, not a width or geometry premise. The conclusion combines the same-task literal minimum with a fixed k,L>0,ell chosen before real alpha and C. k attains Theta, ell is the internally scaled actual optimal product dual. FamilyAllowed holds for every natural m: the maps agree with the fixed designated maps, each ordinary map has some surjective row and some surjective column, and every effective output is attained. This algebraic condition does not assert finiteness of the alphabets. For nonzero m, the constructed endpoint and effective alphabets are finite and nonempty; at m=0, any positive ell_z gives an infinite ZMod 0 coordinate. For every alpha0, an integer m>=2 therefore gives a finite nonempty family satisfying the original assumptions and makes C Wpi(F_m)^alpha<Wcn(F_m). Only k’s addition block varies; all others remain fixed ignored Boolean XOR and F_m has scalar Boolean output. The original-width coefficient is card XP*card YP, independent of m, with all raw cuts bounded by that coefficient times m^L. The normalized lower bound is m^(L Theta). For alpha<0 use Wpi>=1, which gives Wpi^alpha<=1; for alpha>=0 use the positive exponent gap L(Theta-alpha). Thus exponent Theta is attained with coefficient D and every smaller real exponent fails uniformly. Empty N_k, Theta=1, singleton effective images, zero ell and modulus one remain in the construction; universal upper bounds also include constant tasks and initial/half/terminal layers. No sharp-coefficient or order-optimization claim is made.

References