C6 remaining verification obligations¶

Retained bounded-search failures and unresolved certification conditions.

Part of Cycle winding under Coupling: scope and retained evidence. Section numbers are stable across the collection; hypotheses and model changes remain local to each result.

Archived research record. This preserves conditional derivations and source-bound evidence. Its local next-step language is historical and does not schedule work.

62. B68: a shared-source control and the boundary of local progress¶

The B67 source41 gate is evaluated completely: both disjoint conditioned preimages, all twelve incoming arc identities, both parent-root cases and all twenty-one other path records. The old observation-containment links are not used to delete histories. A small adapter, artifacts/research/c6_shared_source_refinement.py, caches twelve source cover/guard intersections around the sealed B67 two-intersection protocol. Every call position and argument is checked; all twenty-four branch-specific pullbacks remain separate. The underlying layer, nodal word audit and exact DBM operations retain their existing owners.

One positive branch and one negative control¶

Of 24 candidates, 18 are empty and six survive:

B67 frontier index	Surviving incoming arcs	Source vertices	Complete nodal word
9	209, 3895	19, 245	`18 -> 40 -> 18 -> 48 -> 8`
13	209, 381, 1095, 1337	19, 35, 64, 83	`18 -> 40 -> 16 -> 26 -> 48 -> 8`

All root intersections are empty. Each return is one nodal step. Arc209 is shared but its two preimages remain different alternatives, as required by the two disjoint target-conditioned parents.

The exact parent differences have four and zero pieces. The first branch strictly shrinks; the second branch's incoming union reconstructs its entire old preimage. Reducing twelve candidates to four in that second branch supplies no geometric gain. It is an explicit negative control for candidate-count-based progress claims.

None of the five distinct surviving sources belongs to the B64 local federation. The existing-cover reuse stage therefore retains all six exterior pieces and yields no additional restriction; no new local cover is generated. After restoring all twenty-one unselected paths, the old 23-piece endpoint union is replaced by 27 pieces. It strictly shrinks: the exact difference has six components against old frontier index9 and is empty against each of the other22 old endpoint pieces. The complete observation hull is unchanged. The original target remains nonempty.

Charged work is1,976 DBM operations: two parent-root checks, twelve shared source-guard intersections, twenty-four distinct target pullbacks, six child-root checks,46 parent-difference operations,64 selected-family difference operations,30 no-change reuse-difference operations and1,792 whole-observation difference operations. Sharing saves twelve source-guard meets; it does not reduce the number of predecessor obligations. Hash/source binding, arc enumeration, path/subset audits, independent replay and cache controls are accounted separately.

The report is artifacts/research/c6_b68_shared_source41.json; the producer and independent validator are c6_b68_shared_source41.py and validate_b68_shared_source41.py. No scientific source, physical parameter, B47 origin or runtime trajectory changes. The regional result remains 41/56 excluded, 15 pending. These local reductions do not supply a convergence rate for the proof search or guarantee eventual global closure. The clipped origin-history cover describes behavior before an original cube exit; it is not by itself an invariant of the un-clipped nodal map. Leaving the chosen cube would not, by itself, prove an unbounded trajectory.

Coordinate-coset relevance: real geometric gain, no modular closure¶

A separate bounded control reuses the B53 exact residue adapter instead of adding another history layer. Write carried coordinates as X = a + q*k, where a is the exact B47 EPI-plus-remainder origin and q = 2^-113. Rebuilding all64 canonical pressure rows and their exact nodal increments gives the coordinate gcds

g_i = gcd_m |h * DeltaNFR_i(m) / q| = (1,1,4,8,8,8).

The origin has k=0; every declared nodal shift preserves k_i=0 mod g_i before exit from the original cube. This is a necessary arithmetic condition, not an origin-reachability characterization. With common modulus8, enumerate the128 allowed residues. For each DBM B and residue r, the quotient constraints are

z_i - z_j <= floor((B_ij - r_i + r_j)/8),  k = 8*z + r,  k_6 = 0.

An integer quotient potential supplies an explicit membership witness; emptiness would require excluding all128 residues. Every one of the27 retained endpoint pieces has a witness in the first residue class, as does every one of the six removed difference pieces. All33 points round to the original mask8 EPI row, and each removed witness lies outside the entire new27-piece union. The test uses33 quotient closures against a declared worst-case cap of4,224. Canonical-pressure rebuilding and independent witness verification are separate costs.

Consequently, the geometric improvement removes coordinate-coset-admissible possibilities, while imposing these cosets alone excludes none of the remaining pieces. The witnesses are hypothetical states, not trajectories from B47. Records and independent checks are retained in c6_b68_coset_relevance.py/.json and its matching .validation.json under artifacts/research; b68_final_validation.json seals both B68 studies.

Whole-label coverage has remained41/56 since B61. B66–B68 have demonstrated strict geometric improvements, but no bound on the number of further refinements needed for closure. B68 also exhibits a branch where fewer candidates buy no geometric improvement, and its modular control cannot close a survivor. Further predecessor depth is therefore deferred as the automatic next action.

The subsequent audit asks whether existing exact separator obstructions still apply to the retained history cover and the stated origin-to-target obligation. Its selected bounded case is result0 of c6_b56_affine_frontier_probe.json:64 supported inequalities at backward depth6 for the mask8 lower target, over11 RN modes and77 affine coefficients. Completion requires classifying every witness and target implication, and rechecking the exact weighted dual identity. It must bind the original root, complete guarded relation, current target-conditioned pieces and exact certificate template. An old dual witness cannot be transferred merely because the displayed RN modes match: history labels and guard geometry may change its admissibility. Failure to transfer an old obstruction does not prove that a new separator exists. This applicability audit precedes any new floating proposal or large search; the detailed gate is recorded in artifacts/research/c6_b68_progress_and_next_gate.md.

63. B69: direct dual transfer fails, and a short entry-policy obstruction¶

B69 completes the selected B56 result0 audit without another LP or predecessor expansion. B55 and B63 have identical B47 state, affine origin, quantum, timestep, all64 RN rows and pressure values. The old64 supported inequalities are rebuilt from their labeled points and returns, including their sparse coefficient encoding, in the original77-dimensional affine space with normalization 2^59. All weights are strictly positive; the weighted vector sum is exactly zero and the strict mass is positive. The old certificate therefore remains valid in its original declared domain.

Direct applicability to the current histories¶

Each fixed witness is tested against every matching retained history and complete guarded arc. For an ingress, its source point is recovered by subtracting the exact return shift; checking only its endpoint is unsound. Target points are checked against the current27 endpoint pieces and all136 recorded physical positions on their existing paths. Intermediate atomic guards are retained. Telescoping a return-level potential uses the active membership of return endpoints; a transient middle alone does not require an additional potential coordinate.

Old constraint kind	Total	Directly admitted	Failing direct admission
Internal drift	51	14	37
Strict ingress	7	2	5
Target nonpositivity	6	0	6
Total	64	16	48

All37 failed drift witnesses and all five failed ingress witnesses lack an admitted current source point. Ingress index40 has an admitted endpoint but no admitted source; it is rejected. None of the six old target points belongs to any current retained history, endpoint piece or recorded suffix position. Their original depth-six target obligations cannot be identified with the newer endpoint union merely by the common mask8 label.

All64 old fixed points also violate the necessary coordinate cosets; in particular every point violates coordinate5's modulus. This does not invalidate the old common-grid affine-domain result. Nor does it exclude possible convex or algebraic derivations of related inequalities on a narrower domain: those implications have not been audited. The precise negative outcome is failure to reuse the published dual by direct admission of its fixed witnesses, not existence of a positive separator or absence of every possible obstruction. A history-indexed coefficient space would likewise require a newly balanced dual.

The audit uses5,607 point-membership and existing-path subset checks, separately records one916-vertex/7,165-arc index construction and4,928 rational weighted component products, and performs no optimizer call. Evidence: artifacts/research/c6_b69_obstruction_applicability.py/.json and the matching independent validation.

Five inequalities expose the cost of blanket entry positivity¶

A distinct certificate uses an already retained, coordinate-coset-admissible path. B68 endpoint9 is B67 normalized frontier10. Its fixed witness follows

history vertices: 89 -> 125 -> 21 -> 97 -> 180
original arcs:    1461, 2011, 217, 1542
RN states:       32 -> 16 -> 26 -> 48 -> 8

All four returns are direct nodal steps. The exact B47-relative carried points, RN rows, coordinate cosets, original/partition guards and retained cover membership are checked. Four shared-kernel steps reproduce the points with zero nodal-balance residual, after rebuilding all64 canonical pressure rows. This is a hypothetical admitted path, not an execution from the B47 initial point.

Use the old eleven-mode active set solely to define a current-endpoint certificate policy: positivity on every geometrically admitted entrance from outside, nondecrease on every internal return, and nonpositivity on the complete current27-piece endpoint target. Mode32 is outside, while 16,26,48,8 are inside. Writing b_j for the potential at the four inside states, the policy demands

b_1 > 0,
b_2 - b_1 >= 0,
b_3 - b_2 >= 0,
b_4 - b_3 >= 0,
-b_4 >= 0.

Their sum is 0 > 0, a contradiction. The retained affine certificate has five77-component vectors, all weights one, exact zero sum and strict mass one. The same telescope applies to arbitrary consistent real state-function values under these identical entry, internal and endpoint conditions. Increasing polynomial degree or adding history coefficients cannot repair this policy while keeping all five requirements at the displayed states.

This is not a transfer of the old depth-six target dual. Its endpoint target is explicitly different. It does not refute an origin-conditioned global barrier, a different active domain or an entry restriction separately proved from B47. The geometric ingress premise includes a hypothetical state whose reachability is unknown; that is the overly strong requirement. Evidence: c6_b69_entry_obstruction.py/.json and its independent validation under artifacts/research.

Root-conditioned continuation¶

Retire blanket positive-entry requirements for this active-region endpoint template. The next formulation must carry the actual origin information through the retained history graph. In B63,910 of916 history zones are nonempty; root vertex260 is the singleton reached by the first direct 57 -> 58 return. Its B47-relative coordinate is that nonzero return shift, not the zero vector. A global certificate must admit this exact root and the already checked initial sentinel/terminal bridge, constrain all relevant guarded transitions, and separate the complete current target. Proof coefficients would be verification functionals, not new nodal forces or physical parameters. The measured formulation has6,370 coefficients, 7,150 fully clipped ordinary arcs and27 target pieces at vertex180: 7,178 root/drift/target verification obligations. A naive robust DBM dualization would add301,434 nonnegative multipliers. This is a size count, not a runtime estimate. The reproducible read-only inventory is c6_b69_next_gate_inventory.py/.json. Specification, exact-verifier cost and sparsity checks precede any candidate search.

Both studies and the documentation checkpoint are sealed by artifacts/research/b69_final_validation.json; the design boundary is in c6_b69_scope_and_next_gate.md. The result remains 41/56 excluded, 15 pending. No actual origin trajectory is extended; no new cover, positive global barrier, C6 instability or indefinite boundedness is proved.

64. B70: executable history-affine obligations and exact verification¶

The B69 proposal now has one complete executable specification. The 910 nonempty history vertices retain independent six-coordinate gradients and offsets. Its sole root is vertex 260 at the exact nonzero first-return image of B47; all 7,150 ordinary clipped arcs and all 27 endpoint pieces remain separate obligations. The original sentinel, terminal and complete-target bridge is retained as a previously verified premise. Storage and local verification do not independently re-prove that bridge.

For beta_v(k)=a_v dot (k/2^59)+b_v, the drift on an arc (v,w,H,s) is

c = (a_w-a_v)/2^59
d = b_w-b_v + a_w dot s/2^59
beta_w(k+s)-beta_v(k) = c dot k+d.

The target check applies the same lower-bound kernel to -beta_180 on each target DBM. Root evaluation requires beta_260(r)>=1; a zero function is insufficient. The normalization and all certificate coefficients are proof representations, with no change to nodal pressure, capacity or evolution.

Exact sparse certificate, complete history checks¶

For a finite closed integer DBM k_i-k_j<=B_ij, k_6=0, a supplied sparse family lambda_ij>=0 proves the affine lower bound if

sum lambda_ij (e_i-e_j) = -c       [coordinates 0..5]
c dot k+d >= d-sum lambda_ij B_ij >= 0.

The coefficient on the fixed-zero coordinate is immaterial. The local checker uses exact rational arithmetic, rejects floating inputs and duplicate facets, verifies closure/consistency, and checks the whole coefficient identity. A sufficient dual need not be optimal. The full checker binds the complete decoded specification by canonical JSON hash, requires exactly one coefficient block and proof record for every declared identity, and includes the translated shift term above. Its rational bit limit is a verification resource limit, not a physical assumption or a mathematical impossibility criterion.

Integer and rational algebraic fixtures exercise positive acceptance; shift-sign, nonzero-root, missing-history, missing-target and stale-binding controls exercise rejection. Two controls on the full C6 specification evaluate all 7,178 obligations: the zero function fails only the root and the constant-one function fails all 27 targets. Neither is a candidate search, and no positive C6 certificate is supplied.

Equivalent geometry and an existing exact extremum owner¶

Exact equality permits storage of 7,108 DBMs for 7,177 uses. The 69 repeated geometries share computation, while their history coefficients and proof obligations remain distinct. There are no duplicate complete history/shift/ geometry obligations to discard. Sequential deletion of an inequality only when the remaining system implies it reduces the weighted facet count from 301,434 to 97,228. All final closures equal their original DBMs, with 11 to 22 retained inequalities per geometry. This procedure uses 312,752 closures within a fixed 320,000 cap; the largest bound has 61 magnitude bits. The chosen irredundant description is order-dependent and is not asserted to have globally minimum cardinality.

The existing _linear_extremum in c6_carried_excursion.py already solves an exact integer transport dual and checks an attaining primal point. A rational adapter factors c into a positive rational scalar times primitive integer weights, reuses that owner and rescales its dual. It independently checks c dot point+d and the lower-bound certificate. A negative minimum gives a violating point for that fixed affine candidate; it does not show that the point is reachable from B47. For seven anchored coordinates, the positive-to-negative transport graph has at most 12 possible edges. That bound is for a fixed signed coefficient vector; an LP with unknown signs cannot silently replace all robust constraints by one fixed such graph.

After B71's verification-boundary preparation below, the bounded step is candidate discovery followed by complete exact verification, with the scope and resource caps in artifacts/research/c6_b70_verifier_and_next_gate.md. Geometry reduction and local extremum calculations neither establish a global separator nor close another first-exit label. The checkpoint is b70_final_validation.json: 41/56 exclusions and 15 pending, on the unchanged B63 scientific source.

65. B71: mechanism reuse and explicit verification boundaries¶

The central B71 audit owns the 308-file inventory, scoped verification-boundary defects and repair plan. None demonstrates a false certificate in the recorded normal C6 validation. The actual root has sum(k)=-4; rank-six controls exclude a nonzero shared- gradient exact invariant on all arcs, not the history-affine barrier family. The known 908-history corridor offers only modest optional savings; rational sink completion need not preserve discovery norm or bit limits.

B71's repair plan requires explicit execution/input boundaries and one validated affine-obligation transform, preserving independent validators. B72 implements it below before the first bounded candidate attempt. No LP ran, origin trajectory was extended or scientific source changed. The checkpoint is b71_final_validation.json: 41/56 excluded, 15 pending, with indefinite C6 boundedness open.

66. B72: shared exact verification and the first bounded LP¶

The central mechanism and verification report owns B72's source repairs, shared history-affine owner and search outcome. The owner unifies admission, translated forms, point rows, exact extrema and final checks. Validation records 451 tests, 11 independent mutation controls, 7,177 matching historical forms/rows and 62 matching local extrema. Nodal pressure, capacity and phase evolution remain unchanged; historical artifacts retain their original source bindings.

The single LP reaches its time limit with no primal candidate (20.051 solver seconds, status 1), so no exact scan, oracle call or second LP follows. B73 below completes the gate removing only norm-objective auxiliaries in a separately versioned feasibility-only point LP: one 20-second attempt, 6,370 free coefficients, zero objective and the same 7,178 point constraints. Finite feasibility is equivalent, with no guarantee of faster solving. Full exact acceptance and coefficient limits remain unchanged. The checkpoint is b72_final_validation.json (artifacts/research/b72_final_validation.json, local evidence): 41/56 excluded, 15 pending, with indefinite C6 boundedness open.

67. B73: feasibility-only control and equivalent proof coordinates¶

The B73 result and next-gate note (artifacts/research/c6_b73_result_and_next_gate.md, local evidence) owns the complete outcome. The zero-objective LP retains all 7,178 point rows with 6,370 free coefficients and 100,288 nonzeros. It reaches the 20-second solver limit without a primal candidate; no exact scan, oracle call or new counterexample cut follows. This is inconclusive. The unchanged B72 source supports reuse of 451 tests and 62 extrema; neither was rerun.

Independent preflight checks all 7,177 drift/target rows plus the root, seven malformed proposals and optimized-execution refusal. The 27 target identities remain, despite only 12 distinct anchored rows. Full guarded obligations cannot be removed on that basis. Two equivalent proof charts are checked: first-evaluation centering reduces nonzeros to 59,682, while the signed-tree chart gives 100,282. The selected chart worsens the largest within-column magnitude ratio; sparsity does not prove better conditioning. Its 2,454 zero point columns may be omitted only with a lift to all 6,370 slots; new cuts require a new active-column audit. B74 below completes binary64 materialization/scaling and inverse original-coordinate preflight before one separately versioned 20-second translated proposal. No further LP ran in B73. The checkpoint is b73_final_validation.json (artifacts/research/b73_final_validation.json, local evidence): 41/56 excluded, 15 pending, with indefinite C6 boundedness open.

68. B74: scaled proposal, full guarded rejection and retained witnesses¶

The B74 result (artifacts/research/c6_b74_result_and_next_gate.md, local evidence) retains all 7,178 sampled conditions in a 3,916-column proposal. Exact positive scaling of 22 rows prevents loading losses in the installed solver; all 59,682 entries, bounds and the objective are checked byte for byte. Independent full-row preflight and nine reconstruction controls pass. The single LP returns a candidate in 7.629 seconds, with no change in nodal dynamics. Reconstruction returns to all 6,370 original slots before checking root normalization, denominator/bit limits and every guarded condition.

The complete scan and independent primal/dual verification reject 5,949 conditions: 5,922 drifts and all 27 targets. Total experiment time is 18.501 seconds. The raw exact lift has 1,688 negative drift anchors; the limited candidate has 1,546, despite floating solver success. Separately, 4,403 failed guarded conditions have nonnegative limited anchors. The raw lift also fails at 5,933 of the retained negative witnesses, so denominator limiting alone does not explain the rejection. None of these points is certified reachable.

The next bounded refinement reuses at most 256 verified witness constraints, starting with all 27 target identities, while preserving all initial rows. New points require recomputing active columns and scaling before another single, separately versioned 20-second proposal and complete exact scan. No further LP or new cut was executed in B74. The current candidate does not refute the full affine family. Source and coverage remain unchanged; the checkpoint is b74_final_validation.json (artifacts/research/b74_final_validation.json, local evidence): 41/56 excluded, 15 pending, with indefinite C6 boundedness open.

The B75 result (artifacts/research/c6_b75_result_and_next_gate.md, local evidence) implements the preceding refinement: all 7,178 initial rows plus 256 verified B74 witnesses, including every target identity. New points reactivate 134 columns; independent preflight checks the resulting 7,434-by-4,050 matrix and all 62,379 entries. Exact positive scaling applies to 81 rows. The full proof problem still has 6,370 original coefficient slots and 7,177 guarded checks.

Its single LP reaches the 20-second limit after 20.023 solver seconds, without coefficients. No exact scan or new extremum follows. Original-point and witness evaluations are unavailable, rather than passed or failed. The intermediate primal-status message is not a mathematical infeasibility certificate. Independent post-run validation passes; nodal dynamics and source remain unchanged.

A no-optimization audit confirms that selecting highs-ipm preserves every outgoing B75 model array and changes only the solver selector. A deferred comparison would use a separately versioned 20-second run on the frozen B75 matrix after independent preflight; only the execution plan can reopen it. No further cuts or history would be added; any candidate retains the same reconstruction, root/cap and exact full-guard requirements. Algorithm choice guarantees no speed or feasibility gain. The checkpoint is b75_final_validation.json (artifacts/research/b75_final_validation.json, local evidence): 41/56 excluded, 15 pending, with indefinite C6 boundedness open.