Completed component-labelled implicit-stratum construction
Construction and dependency ledger, 2026-11-06

Both original connectivity languages now have unconditional native PSPACE
membership theorems in LeanCanny/Connectivity/NativeConnectivityPSPACE.lean:
pointLanguage_mem_PSPACE and connectedLanguage_mem_PSPACE. The full guard
checker, original frontier-edge test, and point/whole graph wrappers are
constructed internally. No component, evaluator, radius or selection oracle
is a theorem premise. Empty whole spaces are accepted; malformed inputs and
ill-scoped, inconsistent or nonunique endpoint descriptions are rejected.

The ledger below preserves the construction plan and historical milestones.

Acceptance target (met)

For original joint packet u, bounded zero-count index K, and two prescribed
old candidate labels a,b, construct a polynomial-space bounded checker such
that its accepted words exist iff the actual joint stratum has a real point
whose two closed-source projections belong to the components named by a,b.
Both directions must use the SAME decoded point. No caller-supplied JoinedIn,
component association, native evaluator, complete square system or expanded
product Term is an acceptable missing implementation.

1. Actual implicit equation

Use the existing JointCoefficientCatalogue, with its actual integer features
f_i and binary count M. Put P(T,x)=product_{i<M}(T+f_i(x)^2).
Let C(x) be the literal joint Core polynomial, U_K=[T^K]P, and L_K=0 for K=0,
otherwise [T^(K-1)]P. Add ONE last variable z and define

  Q(x,z)=C(x)^2+L_K(x)^2+(U_K(x)*z^2-1)^2.

Q=0 enforces the actual Core and exactly K zero features. All x columns stay
literal. No product Term is serialized. If feature degree/mass charges are
d,h, set dP=M*(2*d+1), hP=M*(2*h+1). A safe degree charge is
D=max(2*dC,2*dP+4), and a safe mass exponent is H=2*max(hC,hP)+4.
Dimension m=jointDimension+1 is unary; D,H,M,K are binary. Modular coefficients
come from a fixed number of renames, sums and convolutions of the Core and
the already constructed product-coefficient Source. Loops enumerate exponent
splits with polynomial-length counters; coefficient integers are not emitted.

2. Finite grid instead of an expanded critical sampler

For each coordinate i, use the actual CoerciveBoxGramEliminant G_i(epsilon,T)
of Q. This is a fixed padded block determinant, with no chosen maximal minor
or universal-resultant quotient. Existing theorems prove G_i nonzero and
G_i(epsilon,x_i)=0 at actual coercive critical points.

Let W be the binary size of the maximum of the homogeneous degree and
Macaulay level, N=2^((m+1)*W), and L=(m+3)*N. Both parameter degrees of G_i
are bounded by L. The block determinant has binary degree/mass charges and
PSPACE coefficient access from the actual homogeneous Q rows.

A short table Gamma stores (tau_i,r_i), each at most L. Set p_i=[epsilon^tau_i]G_i
and let h_i=p_i when its r_i coefficient is nonzero, otherwise h_i=1.
Nonzeroness is internal on EVERY table: one witnessed nonzero coefficient,
or the constant-one fallback. Its test uses modular coefficient access and
an integer-zero program, not an exponentially long exact coefficient.
The encoded Gamma length is at most (6*size(L+1)+6)*m. True trailing tau_i and suitable r_i exist
by G_i nonzeroness. Soundness does not require Gamma to be trailing.

Build diagonal rows h_i(X_i), with annihilators h_i. Completeness is then a
direct row-evaluation identity; repeated roots use the existing squarefree
grid machinery. Decode an OWN exact-width complete-sampler word and test
Q=0 at that SAME tuple using the native polynomial-sign test. Arbitrary grid
points are not assumed to satisfy Q.

Component hit uses ONE actual critical-limit vector in the original stratum
component. All G_i pass to their true trailing coefficients at that same
limit. The resulting grid point still satisfies Q, remains in that component,
and has an exact OWN word. CoerciveGramComponentGrid formalizes this geometric
step. Native Gram access, the actual equation Source and the word/filter
assembly are separate implementation steps; that geometric file is not the
completed sampler.

3. External-point component association

Use a typed endpoint provider OLD(candidate) or EXTERNAL(own grid point).
The connected spatial source stays the old closed-circular polynomial in
both cases. Its integer marked prelude retains n+8 leaves:

  y_1,...,y_n, u,0,v,0, radius,regularization,beta,penalty.

Only coordinate/slack sources and Replay matching vary. For EXTERNAL, use
the selected coordinate annihilators and the actual fixed external algebra.
Compute slack characteristic polynomials using selected coordinate references.
Compare ALL derivative signs to the external OWN point; annihilator roots
alone admit wrong conjugates. Derive the correlated prelude realization and
validate the actual lift equations. Neither projection equality to an old
candidate nor an association premise is permitted.

The existing two-prefix geometry can then compare OLD and EXTERNAL through
one common genuine critical point. The initial count stays n+8, but source,
Replay, initialization and width wrappers must be generalized honestly.
For external algebra rank B, log B is polynomial; coordinate and slack
degree bounds are binary (including 2B and spatialDegree*B). Choose one
unary scalar width covering both providers BEFORE either prefix word.

4. Essential distinction: containment and joining radius

This construction first gives Assoc_R: membership in the same component
INSIDE the chosen ball. Head height/degree root bounds and the old candidate
bound give endpoint containment. They do not bound a joining path.
The old closed-circular source can be unbounded; proper projection does not
make its entire zero set bounded.

EffectivePolynomialBallConnections now proves the needed geometric contract
directly. For an integer polynomial q with degree at most D and coefficient
mass at most 2^H, a cutoff radiusExponent(n,D,H) has BinaryFn controls.
For every R above that cutoff and every pair of endpoints already in the
literal bounded zero set, JoinedIn and connectedComponentIn agree with the
entire original zero set. Singular and unbounded zero sets are covered.
No regularity, parameter head, exclusion interval or stabilization oracle
is an input. Actual boundary Gram heads derive a small-residual critical
band exclusion; proper two-circle transport and compact residual limits
then identify the bounded and original connections.

Consequently a correct bounded two-provider association checker at this
common radius will also decide unbounded component association. It need not
first transport every record word as R varies. The bounded checker and its
correctness remain necessary; the geometric theorem does not supply them.

Milestones and stopping rule

A. Closed actual Q Source; implicit Gram reader; diagonal OWN word/filter;
   component-hit and original polynomial certificate budget.
B. Actual EXTERNAL n+8-leaf prelude with derived Source.Access and Replay;
   two-provider bounded association correctness and PSPACE cost.
C. Effective original ball cutoff (proved); use B to identify unbounded
   association and prove both-label feasibility iff (integration remains).
   The prototype is complete only after that iff is proved.

Use bounded checkpoints at these interfaces. Record the exact missing
contract if a checkpoint fails; do not replace it with more unrelated
catalogues or conditional wrappers. Full interval features/frontier edges
and the original two PSPACE endpoints remain later obligations.

Implemented checkpoint A

FormulaSignSlotRadialJointStratumSampler.mem_PSPACE is the closed native
checker theorem for the actual Q Source. No source, row, matrix, evaluator,
complete-system or component-association hypothesis is supplied by a caller.
accepted_iff tests the literal Core and zero-count certificate at its OWN
decoded point. component_hit constructs bounded Gamma and an exact-width
own word whose decoded point is joined to the requested point INSIDE Q=0.
The original-header tableBound and ownwordBound are UnaryFn; nonempty_iff
identifies source feasibility with bounded accepted certificates.

The generic construction is ImplicitSourceComponentSampler: actual fixed
Gram determinants, witnessed nonzero slices with a total fallback, derived
diagonal Inputs.Access and Complete, original-header word envelope, and
same-point source equation test. Positive-dimensional, singular and
unbounded zero sets are covered. The actual implicit binary-count feature
family is instantiated without expanding it into a Term.

This proves sampling, not association with either prescribed old candidate
label. The actual OLD/EXTERNAL coordinate algebra, marked root vectors,
full causal record backend and native atomic checker are now constructed.
Both root vectors realize the actual planned saved prelude at the complete
record horizon. The geometric cutoff for C is proved, but bounded association
correctness and its integration with both labels remain open. The full component-labelled prototype and both original
connectivity PSPACE endpoints therefore remain unproved.

Checkpoint verification: strict three-library build (21634 jobs), the
focused actual-sampler fixture, complete axiom and native-space audits,
and the existing native-roadmap regression all pass. Every new whole source
also passes at 200000 heartbeats with warnings as errors and strict implicit
variables. See ROADMAP-PROOF-AUDIT.txt, section 59, for recorded evidence.

Implemented native provider foundation for B

FormulaSignSlotRadialProviderAtomic.mem_PSPACE decides the actual seven-part
atomic predicate: checked grammar, one complete OWN word, all earlier cut
and creating-critical guards, latest coordinate companions, literal integer
leaves/regular/mark equations, and actual OLD or EXTERNAL replay. The source,
all native controls and caller-modulus bounds are derived. EXTERNAL replay
checks a canonical source/header/side association and actual Q=0 at the SAME
own grid point; it never requires the prescribed old label to name that
external point. All original coordinates compare every derivative sign.

Canonical OLD and EXTERNAL endpoints supply actual n+8 root vectors whose
first n+4 coordinates equal the canonical marked lift. Both vectors realize
the actual planned record saved state, with its full record cap and width.
ProviderPair.oldOf changes only the role flag and retains all joint metadata;
the two actual radii and spatial sources are proved equal. Provider-only
vertex and OWN-word budgets are UnaryFn. Original joint-header bounds remain
an integration obligation.

Source-aware point/frame/signature readback and BOTH replay-to-prelude
projections are proved. Genuine OLD candidates and accepted EXTERNAL own
points construct fresh accepted depth-zero seeds in the same marked-source
component, preserving every initial marked coordinate. Retained histories
preserve actual prefix algebras, all earlier bank values, critical guards,
full cut receipts and replay on independently sampled own words.

Fresh accepted recursive children now realize any prescribed eligible point,
preserve the literal provider and all earlier fields, and increase depth by
one. All seven native acceptance gates are derived from the fresh own word.
Every accepted parent with depth room also has an equal-point child joined
by an actual native identity edge. Native NoCritical and NoBad are equivalent
to critical-height freedom and bad-set freedom on the original frozen slice.
The NoBad equivalence derives all decoder bounds and fresh probes internally.
Genuine matched slab interiors construct accepted proper children with the
prescribed entire endpoint points, SAME literal provider and earlier fields.
Every actual Local/Proper edge gate is now derived internally. Native Local
incidence gives a path through its whole MID anchor; midpoint signatures
identify the entire shared point, so every raw native path is sound.
Full frozen-depth induction proves completeness, and at depth zero native
reachability is equivalent to original provider-source joinedness.
A genuine path from a seed to its OWN initial marked vector constructs a
reachable terminal native marked anchor, retaining all initial fields.
This attachment is not inferred from Atomic.Valid alone.
Native current-point OLD/EXTERNAL association has a geometric iff. The
anchored native checker also requires reachable markers in BOTH providers;
it does not equate current points with their marked preludes. Same-provider
marked preludes are joined via their equal original projections; auxiliary
phases need not agree. Original joint-header bounds now cover both provider
graphs, with the sampler choosing its bounded metadata internally.
One bounded two-label checker uses the SAME kind/Gamma/OWN sample on both
sides. Its native witness iff and exact original stratum-label equivalence
are proved. The extended feature catalogue preserves actual anchor-grid
membership during component sampling. A genuine descriptor lifts to the
actual stratum, retaining both labels and the entire radial tuple. Complete
principal/value interval guards and Boolean frontier integration remain open.
Native identity and cross-point
comparisons read the entire current point; recursive edges retain one literal
provider, while cross-point comparison requires the same original and radius.
Native NoBad/NoCritical/Near cost theorems alone do not supply geometric iff.
Vertex PSPACE and Replay alone imply none of those component statements.
The guarded two-label feasibility equivalence and both original unconditional
connectivity PSPACE endpoints remain open. This checkpoint introduces no
component, path, model, native evaluator or solvability oracle.

Native guard and frontier integration checkpoint, 2026-11-06

The original cover's actual relative-frontier edge is now equivalent to:
projected auxiliary-sample equality, or guarded joint feasibility in either
orientation. Guarded feasibility includes both original labels, the actual
anchor grid and every cut on the radius interval. A raw radial descriptor
and this literal original-header feasibility predicate imply each other.
The native guarded-feasibility decider now implements this characterization.

The enlarged joint feature family includes actual grid, coordinate-head,
principal and value interval controls while preserving every old coefficient
index. Principal and value interval truth is invariant along actual stratum
JoinedIn. Native grid testing now selects and verifies perturbation/degree
receipts internally, evaluates every grid equation on the SAME own sample,
and is in PSPACE without a supplied Selections premise.

There is also a checked endpoint route through existing samples. Conjoining
tautologies containing both endpoint formulas leaves the space unchanged.
Original subformula truth is constant on each sign piece. Thus, if an endpoint
formula denotes a singleton, every piece containing it has that endpoint as
its existing sample. Original point connectivity consequently reduces to walks
between these samples with the singleton tests retained. No reserved endpoint
frontier edges are needed for this route.

Completed: native interval checking, its same-word conjunction with the
two-label witness, and the original bit-graph PSPACE wrappers. The endpoint
formula tautologies retain the original space and make both endpoints actual
existing samples. Native singleton validation and bounded word searches reject
all malformed or invalid queries.

Final checked route

1. FormulaSignSlotRadialGuardedFeasibilityNative.word_decider checks the actual
   sampler filter, grid, coordinate leading cuts, squarefree branch cuts,
   VALUE cuts and margin cuts on the SAME complete OWN word.
2. FormulaSignSlotRadialGuardedFeasibility.language_iff_feasible identifies
   bounded two-label acceptance with literal geometric joint feasibility.
3. CanonicalAuxiliaryNativeFrontier.edge_eq identifies the constructed native
   edge with the original Boolean cover's frontier relation.
4. CanonicalAuxiliaryNativeDecision and CanonicalAuxiliaryNativePointSearch
   supply the two original total graph decision procedures.
5. NativeConnectivityPSPACE instantiates both with the concrete guard decider.

The final statements refer to the original pointLanguage and connectedLanguage,
without a computational premise. Explicit roadmap output is outside these
language-membership statements.