[antonkov]

Change

Part of #1226. Depends on #1327 (Part 1, GreedySlotScore.lean).

Adds Complexity/Computability/PolyTime/GreedyLabelSchedule.lean (Cslib.BalancedSchedules) and concrete regression tests in ComplexityTests/GreedyLabelSchedule.lean, completing the runtime $(n + m)$-slot greedy schedule pass, empty-scope factor normalization, end-to-end Lemma 4.5 occupancy bounds, all-prefix outer-loop live-state bit-length bounds, and uniform Cslib.GenericRAM.NativeCertificate / Turing.MultiTapeTM.ComputableInO / Turing.MultiTapeTM.ComputableInPolySpace certificates for §4.4, Lemma 4.5 (and its §4.5 group-schedule interface, printed pp. 30–32) of [OpenAI, The Exponential Time Hypothesis is False][OpenAI2026ETH] (pinned revision 7ef5c0cc) on top of Complexity.Computability.PolyTime.GreedySlotScore.

Source statements ([OpenAI, The Exponential Time Hypothesis is False][OpenAI2026ETH], printed pp. 30–32)

(Mathematical-transcription note: Plain-text extraction from the source PDF flattens rendered superscripts, subscripts, set-builder braces, square roots, fractions, calligraphic and blackboard-bold symbols, and vector arrows such as $(I_f){f \in \mathcal{F}}$, $\mathcal{A}$, $\mathcal{B}$, $|\mathcal{F}|$, $D = r^{2Q}$, $2(b + w)D^2 \leqslant M$, $2Qr^2 \leqslant n$, $a_v, d_f \in [r]^Q$, $u{f,v}$, $c_u \leqslant \frac{M}{D} + \sqrt{2M(b + w)}$, $n_{t,g} \leqslant \frac{n}{r} + \sqrt{2Qn}$, $K^4 = D^2$, $\vec{P}{f,v}(T)$, $\mathbb{Q}^n$, and $S{t,g}$ into "(If )f ∈F", "A", "B", "|F|", "D = r2Q", "2(b + w)D2 ⩽ M", "2Qr2 ⩽ n", "av , df ∈ [r]Q", "uf,v", "cu ⩽ M/D + p 2M (b + w)", "nt,g ⩽ n/r + p 2Qn", "K 4 = D2", "P⃗f,v (T )", "Qn", and "St,g"; in the contiguous source passages below, all mathematical superscripts, subscripts, radicals, fractions, calligraphic/blackboard-bold fonts, vector arrows, and slanted inequalities $\leqslant, \geqslant$ are restored to match rendered printed pages 30–32.)

• §4.4, Lemma 4.5 statement (printed p. 30, eq. (4.13)):

  Lemma 4.5. Let $(I_f){f \in \mathcal{F}}$ satisfy (4.1), with $n \leqslant M \leqslant bn$, and put $D = r^{2Q}$ for integers $r \geqslant 2$ and $Q \geqslant 1$. Suppose
  $$2(b + w)D^2 \leqslant M, \qquad 2Qr^2 \leqslant n. \tag{4.13}$$
  One can deterministically choose $a_v, d_f \in [r]^Q$, with $d_f(t) = 1$ for factors of empty scope, so that
  $$\max{u \in \mathcal{B}} #{(f, v) \in \mathcal{A} : (a_v, d_f) = u} \leqslant \frac{2M}{D},$$
  $$#{v \in [n] : a_v(t) = g} \leqslant \frac{2n}{r} \qquad (t \in [Q], g \in [r]).$$
  The construction takes $\mathrm{poly}(n, M, |\mathcal{F}|, D, Q, r, b, w)$ bit operations.

• §4.4, Proof of Lemma 4.5, empty-scope convention (printed p. 31):

  For this estimate, all $a_v$ and all $d_f$ with nonempty $I_f$ are independent and uniform on $[r]^Q$. For empty $I_f$, we set $d_f$ identically one. Each incidence label $u_{f,v} = (a_v, d_f)$ is uniform on $\mathcal{B}$.

• §4.4, Proof of Lemma 4.5, deterministic one-slot-at-a-time pass and occupancy extraction (printed p. 31):

  To obtain the labels deterministically, we fix the $a_v$ and the $d_f$ for nonempty $I_f$ one at a time. At each step we choose a value that does not increase the conditional expectation of
  $$\frac{\Phi}{M(b + w)} + \frac{\Xi}{Qn}.$$
  Such a choice exists because the current expectation is the average over the possible values of the next $a_v$ or $d_f$. The final value is at most two. Since both summands are nonnegative,
  $$c_u \leqslant \frac{M}{D} + \sqrt{2M(b + w)}, \qquad n_{t,g} \leqslant \frac{n}{r} + \sqrt{2Qn}.$$
  The two inequalities in (4.13) make the square-root terms at most $M/D$ and $n/r$, respectively.

• §4.4, Proof of Lemma 4.5, $(n + |\mathcal{F}|)$-slot runtime over $K = r^Q$ candidates (printed p. 31):

  Including the normalizations $M(b + w)$ and $Qn$, all rational values in these calculations have numerators and denominators with
  $$O(\log(2D) + \log(2M) + \log(2n) + \log(2Q) + \log(2 + b + w))$$
  bits. There are at most $n + |\mathcal{F}|$ choices to fix, each with $K$ candidate values. Since $K^4 = D^2$, the entire construction takes $\mathrm{poly}(n, M, |\mathcal{F}|, D, Q, r, b, w)$ bit operations.

• §4.5, variable-group and factor-schedule consumption of Lemma 4.5 (printed p. 32, eq. (4.14)):

  Now put
  $$\vec{P}{f,v}(T) = \vec{P}{u_{f,v}}(T) \pi_{c(f,v)} \iota, \qquad S_{t,g} = {v \in [n] : a_v(t) = g}, \qquad \sigma_f(t) = d_f(t). \tag{4.14}$$
  The row $\vec{P}{f,v}(T)$ acts on the actual variables $x \in \mathbb{Q}^n$. At $T = 0$, it extracts the value in position $(c(f, v), u{f,v})$, which is $x_v$. Thus $\vec{P}{f,v}(0) = \delta_v$, and its degree is at most $R - 1$. Lemma 4.5 gives $|S{t,g}| \leqslant 2n/r$.

Notation-to-Lean mapping

• Variable count $n$, factor count $|\mathcal{F}|$, round count $Q$, group count $r$, incidence count $M = |\mathcal{A}|$, and degree normalizer $b + w$: runtime tuple Cslib.BalancedSchedules.ScheduleParams $= ((n, m, Q), (r, C), \text{edges})$ encoded by Cslib.BalancedSchedules.encScheduleParams with unary $(n, m, Q)$ and binary $(r, C)$ and incidence pairs $(f, v)$.
• Candidate count $K = r^Q$ and auxiliary dimension $D = r^{2Q} = (r^Q)^2$: inner candidate loop bound $r^Q$ inside Cslib.BalancedSchedules.streamBestSlotLabel and multiplicative factor $((r^Q)^2)^2 = D^2$ in Cslib.BalancedSchedules.constructBalancedSchedules_balanced.
• One-slot-at-a-time $(n + |\mathcal{F}|)$-slot pass and empty-scope factor reset $d_f(t) = 1$: Cslib.BalancedSchedules.slotOfIndex, Cslib.BalancedSchedules.pendingSlotOfState, Cslib.BalancedSchedules.greedySlotStepBody, Cslib.BalancedSchedules.greedySchedulePass, Cslib.BalancedSchedules.normalizeEmptyFactorSchedules (resetting empty-scope factors to the $0$-based constant zero word List.replicate $Q$ $0$), and Cslib.BalancedSchedules.constructBalancedSchedules.
• Chosen schedules $a_v, d_f \in [r]^Q$ and §4.5 group schedules $S_{t,g} = {v \in [n] : a_v(t) = g}$, $\sigma_f = d_f$: typed projections Cslib.BalancedSchedules.constructedVarSchedule (Fin $n \to$ Fin $Q \to$ Fin $r$) and Cslib.BalancedSchedules.constructedFactorSchedule (Fin $m \to$ Fin $Q \to$ Fin $r$), with cleared-denominator occupancy bounds Cslib.BalancedSchedules.occupancy $\cdot, (r^Q)^2 \le 2E$ and Cslib.BalancedSchedules.occupancy $\cdot, r \le 2n$ in Cslib.BalancedSchedules.constructBalancedSchedules_balanced.

Public claims and assumptions

1. Streaming $(n + m)$-slot greedy pass and empty-scope factor normalization:
   • Cslib.BalancedSchedules.slotOfIndex, Cslib.BalancedSchedules.pendingSlotOfState, Cslib.BalancedSchedules.greedySlotStepBody, and Cslib.BalancedSchedules.greedySchedulePass iterate Cslib.GenericRAM.IndexFold.run across all $n + m$ variable and factor slots using Cslib.BalancedSchedules.streamBestSlotLabel.
   • Cslib.BalancedSchedules.normalizeEmptyFactorSchedules and Cslib.BalancedSchedules.constructBalancedSchedules finalize partial schedules and reset every empty-scope factor ($\forall e \in \text{edges},, e.1 \ne f$) to List.replicate $Q$ $0$, with exact output lengths (Cslib.BalancedSchedules.length_fst_constructBalancedSchedules, Cslib.BalancedSchedules.length_snd_constructBalancedSchedules), word well-formedness across every prefix and final output (Cslib.BalancedSchedules.run_greedySlotStepBody_wf, Cslib.BalancedSchedules.wf_constructBalancedSchedules), and concrete empty-factor reset (Cslib.BalancedSchedules.getD_constructBalancedSchedules_empty_factor).
2. Combinatorial bridge and Lemma 4.5 potential and occupancy bounds:
   • Cslib.BalancedSchedules.greedySchedulePass_eq_greedyLabelPass, Cslib.BalancedSchedules.constructedSchedules_eq_pass, and Cslib.BalancedSchedules.constructedFactorSchedule_empty_factor prove exact agreement between Cslib.BalancedSchedules.greedySchedulePass / Cslib.BalancedSchedules.constructBalancedSchedules (projected via Cslib.BalancedSchedules.constructedVarSchedule and Cslib.BalancedSchedules.constructedFactorSchedule) and Cslib.BalancedSchedules.greedyLabelPass, Cslib.BalancedSchedules.completeLabels, and Cslib.BalancedSchedules.normalizeEmptyFactors.
   • Cslib.BalancedSchedules.constructBalancedSchedules_score_le and Cslib.BalancedSchedules.constructBalancedSchedules_score_le_two establish that the runtime construction achieves normalized joint Cslib.BalancedSchedules.potential at most the uniform average and at most $2$ under variable and factor degree bounds $b, w$ with $0 < b + w$ and $0 < E$.
   • Cslib.BalancedSchedules.constructBalancedSchedules_balanced proves Lemma 4.5 end-to-end for all $1 \le r$, $1 \le Q$, $1 \le n$, degree bounds $b, w$ with $0 < b + w$, and size bounds (4.13) $2(b + w)((r^Q)^2)^2 \le E$ and $2Qr^2 \le n$: empty-scope factors satisfy $d_f(t) = \langle 0, hr \rangle$, every incidence label $u \in (\text{Fin } Q \to \text{Fin } r)^2$ has cleared occupancy $\text{occ}(u) \cdot (r^Q)^2 \le 2E$, and every round $t$ and group $g$ has cleared variable-group occupancy $\text{occ}(g) \cdot r \le 2n$.
3. Hypergraph-valid prefix bit-length bounds and native machine certificates:
   • Under Cslib.BalancedSchedules.encScheduleParams and Cslib.BalancedSchedules.encOuterAcc, Cslib.BalancedSchedules.length_encEdges_le_of_lt, Cslib.BalancedSchedules.length_encPartialSchedules_le, Cslib.BalancedSchedules.length_encSlotSelectState_run_valid_le, Cslib.BalancedSchedules.length_encOuterState_run_valid_le, and Cslib.BalancedSchedules.length_encOuterState_run_le bound inner-loop and outer-loop live-state bit lengths across all visited prefixes without multiplying workspace by $r^Q$.
   • Cslib.BalancedSchedules.computableInPolyTime_slotOfIndex, Cslib.BalancedSchedules.greedySchedulePassCertificate, Cslib.BalancedSchedules.greedySchedulePassCertificate_bounds, Cslib.BalancedSchedules.computableInO_greedySchedulePass, Cslib.BalancedSchedules.computableInPolySpace_greedySchedulePass, Cslib.BalancedSchedules.constructBalancedSchedulesCertificate, Cslib.BalancedSchedules.constructBalancedSchedulesCertificate_bounds, Cslib.BalancedSchedules.computableInO_constructBalancedSchedules, and Cslib.BalancedSchedules.computableInPolySpace_constructBalancedSchedules establish uniform Cslib.GenericRAM.NativeCertificates running in $O((r^Q + 1) \cdot \mathrm{poly}(\lvert\text{input}\rvert))$ native time and polynomial workspace. For valid hypergraph incidence endpoints, this yields $\mathrm{poly}(n, m, |E|, D, Q, r, C)$ bit operations with $D = r^{2Q}$; for arbitrary endpoint indices, the bound is measured in the full encoded input length.

Deviations / Non-claims

• Semantic-versus-certified boundary: Public encoded Turing.MultiTapeTM.ComputableInPolyTime, Cslib.GenericRAM.NativeCertificate, Turing.MultiTapeTM.ComputableInO, and Turing.MultiTapeTM.ComputableInPolySpace theorems govern Cslib.BalancedSchedules.slotOfIndex, Cslib.BalancedSchedules.greedySchedulePass, Cslib.BalancedSchedules.constructBalancedSchedules, and their certificates (built on the concrete list and integer step and postprocessing subroutines Cslib.BalancedSchedules.pendingSlotOfState, Cslib.BalancedSchedules.greedySlotStepBody, and Cslib.BalancedSchedules.normalizeEmptyFactorSchedules) under Cslib.BalancedSchedules.encScheduleParams and Cslib.BalancedSchedules.encOuterAcc, whereas Cslib.BalancedSchedules.constructedVarSchedule and Cslib.BalancedSchedules.constructedFactorSchedule serve as unencoded typed specification bridges to Cslib.BalancedSchedules.greedyLabelPass, Cslib.BalancedSchedules.potential, and Cslib.BalancedSchedules.occupancy. Note also that Cslib.BalancedSchedules.constructBalancedSchedules_balanced holds for all $1 \le r$ (slightly relaxing the manuscript's $r \geqslant 2$).

• 0-based alphabet and total degenerate/out-of-domain fallbacks: Group labels sit in ${0, \dots, r - 1}$, so $d_f(t) = 1$ in the manuscript corresponds to List.replicate $Q$ $0$ (and typed constant $\langle 0, hr \rangle$). For total execution on all inputs: Cslib.BalancedSchedules.slotOfIndex caps $s$ at $n + m$ via min before unary subtraction and returns none for $s \ge n + m$; Cslib.BalancedSchedules.pendingSlotOfState and Cslib.BalancedSchedules.greedySlotStepBody leave already-assigned or out-of-range indices unchanged; when $r = 0$ ($Q > 0$, so $r^Q = 0$) or a slot remains none, fallback words are List.replicate $Q$ $0$ (and [] when $Q = 0$); Cslib.BalancedSchedules.normalizeEmptyFactorSchedules resets every factor absent from the edge list to List.replicate $Q$ $0$; and Cslib.BalancedSchedules.constructedVarSchedule / Cslib.BalancedSchedules.constructedFactorSchedule clamp out-of-range digits or missing positions to $0$ via Cslib.BalancedSchedules.wordToSchedule.

• Downstream §4.5 auxiliary-array placement: Assembling the explicit copy indices $c(f, v)$, replacement-design rows $\vec{P}{f,v}(T)$, and restricted measurement matrices $C{t,g}$ of §4.5 (eqs. (4.14)–(4.15)) is handled in feat(PolyTime/LinearAlgebra): add Section 4.5-4.7 replacement design builder #1330 under Port OpenAI's ETH refutation (subexponential #k-SAT) natively into complexitylib #1226.

• Existing notions considered:

  • Cslib.BalancedSchedules.greedyLabelStep, Cslib.BalancedSchedules.greedyLabelPass, Cslib.BalancedSchedules.greedyLabelPass_spec, Cslib.BalancedSchedules.completeLabels, Cslib.BalancedSchedules.normalizeEmptyFactors, Cslib.BalancedSchedules.potential, Cslib.BalancedSchedules.occupancy, Cslib.BalancedSchedules.expect_incidence_potential_le, Cslib.BalancedSchedules.expect_group_potential_le, and Cslib.BalancedSchedules.incidence_and_group_bounds (Complexity/Foundations/Combinatorics/GreedySchedules.lean, Complexity/Foundations/Combinatorics/PartialLabelScores.lean): reused directly for the combinatorial potential and occupancy analysis; Cslib.BalancedSchedules.greedySchedulePass_eq_greedyLabelPass and Cslib.BalancedSchedules.constructedSchedules_eq_pass bridge the concrete Cslib.GenericRAM.IndexFold.run pass directly to Cslib.BalancedSchedules.greedyLabelPass rather than re-proving conditional-expectation bounds.
  • Cslib.BalancedSchedules.streamBestSlotLabel, Cslib.BalancedSchedules.streamBestSlotCertificate, Cslib.BalancedSchedules.streamBestSlotCertificate_bounds, Cslib.BalancedSchedules.candidateScheduleList, Cslib.BalancedSchedules.wordToSchedule, Cslib.BalancedSchedules.scheduleToWord, Cslib.BalancedSchedules.edgesOfFin, Cslib.BalancedSchedules.partialScheduleListOfFin, Cslib.BalancedSchedules.updateSlotSchedules, Cslib.BalancedSchedules.readSlotSchedule, Cslib.BalancedSchedules.encPartialSchedules, and Cslib.BalancedSchedules.encStreamSlotIn (Complexity/Computability/PolyTime/GreedySlotScore.lean): reused directly as the single-slot streaming minimizer and bit-length/certificate foundation.
  • Cslib.GenericRAM.IndexFold.run, Cslib.GenericRAM.IndexFold.length_run, Cslib.GenericRAM.IndexFold.roundCertificate, Cslib.GenericRAM.IndexFold.certificate, Cslib.GenericRAM.NativeCertificate.option, and Cslib.GenericRAM.NativeCertificate.ofPolyTime (Complexity/Computability/GenericRAM/Native/IndexFold.lean, Complexity/Computability/GenericRAM/Native/Combinators.lean): reused directly to nest the outer $(n + m)$-slot pass around Cslib.BalancedSchedules.streamBestSlotCertificate in polynomial workspace.
  • List.getD_eq_getElem, List.getD_ofFn, List.getD_map_range, List.ofFn_const, List.ofFn_succ', and List.sum_le_length_nsmul (Complexity/Foundations/Data/List/Lookup.lean, Mathlib/Data/List/GetD.lean, Mathlib/Data/List/OfFn.lean): reused directly for list lookups, snoc induction over List.ofFn, and entrywise encoded-length sum bounds without private duplicate list helpers.

Validation and review

• Tested at 58a3472febd10ea9dad31bd7b51b20782cb4930d on c20adaa8aeffcefa3f9f8949b4d24548a5e2c148 (feat/rt-greedy-schedule-1226-antonkov):
  • LEAN_NUM_THREADS=4 lake exe mk_all --check — passed.
  • LEAN_NUM_THREADS=4 lake build --wfail --iofail Complexity ComplexityTests ComplexityAbstracts — passed (0 warnings).
  • LEAN_NUM_THREADS=4 lake exe runLinter Complexity.Computability.PolyTime.GreedyLabelSchedule ComplexityTests.GreedyLabelSchedule — passed.
  • LEAN_NUM_THREADS=4 lake exe lint-style — passed.
  • LEAN_NUM_THREADS=4 lake exe checkInitImports — passed.
  • python3 scripts/check_hygiene.py --check-simp — passed.
  • python3 scripts/check_tidy_surface.py — passed (0 new public Tidy declarations).
  • python3 scripts/check_changed_files.py --base feat/rt-greedy-schedule-1226-antonkov — passed.
  • python3 scripts/parallel_defs.py --base feat/rt-greedy-schedule-1226-antonkov — passed (0 candidate parallel definitions).
  • python3 scripts/audit_queries.py duplicates Complexity/Computability/PolyTime/GreedyLabelSchedule.lean — passed (0 duplicates).
  • python3 -B scripts/build_abstracts.py --check — passed.
  • python3 scripts/check_pr_names.py --strict --base feat/rt-greedy-schedule-1226-antonkov — passed.
• Representative concrete checks in ComplexityTests/GreedyLabelSchedule.lean: kernel-checked decide +kernel and definitional tests covering outer slot decoding and capping (Cslib.BalancedSchedules.slotOfIndex), no-op behavior on already-assigned and out-of-range indices (Cslib.BalancedSchedules.pendingSlotOfState, Cslib.BalancedSchedules.greedySlotStepBody), degenerate regimes ($Q = 0$, $r = 0$, $r = 1$, and $E = 0$), exact evaluation of Cslib.BalancedSchedules.normalizeEmptyFactorSchedules, Cslib.BalancedSchedules.greedySchedulePass, Cslib.BalancedSchedules.constructBalancedSchedules, and Cslib.BalancedSchedules.greedyLabelPass on a $2$-variable, $4$-factor hypergraph with both non-empty and empty-scope factors achieving concrete occupancy $\le 1$, a nonvacuous $96$-variable, $50$-factor concrete instantiation of Cslib.BalancedSchedules.constructBalancedSchedules_balanced ($r = 2, Q = 1, E = 96, b = 1, w = 2$, with two empty-scope factors normalized to $0$, incidence occupancy $\le 48$, and variable-group occupancy $\le 96$), concrete all-prefix outer live-state bit-length verification via Cslib.BalancedSchedules.length_encOuterState_run_valid_le, compositional fun_prop synthesis for Cslib.BalancedSchedules.slotOfIndex, and concrete instantiation of Cslib.BalancedSchedules.greedySchedulePassCertificate_bounds and Cslib.BalancedSchedules.constructBalancedSchedulesCertificate_bounds.
• Non-author pre-PR review: mathematical, rendered-PDF manuscript-fidelity, and API-reuse review completed at 58a3472febd10ea9dad31bd7b51b20782cb4930d (verifying direct reuse of Cslib.BalancedSchedules.greedyLabelPass, Cslib.BalancedSchedules.streamBestSlotCertificate, Cslib.GenericRAM.IndexFold.run, List.getD_eq_getElem, List.getD_ofFn, and List.sum_le_length_nsmul, Lemma 4.5 potential and occupancy bounds via Cslib.BalancedSchedules.constructBalancedSchedules_balanced, all-prefix live-state bit-length bounds, Turing.MultiTapeTM.ComputableInPolySpace / Turing.MultiTapeTM.ComputableInO contracts, and verbatim quotation fidelity against OpenAI (2026) §4.4, Lemma 4.5, printed pp. 30–32), followed by full 6-gate scripts/check.sh verification at 58a3472febd10ea9dad31bd7b51b20782cb4930d.

Headline abstracts

• Affected abstracts/catalogue entries, or reason the selection is unaffected: Unaffected. None of the curated abstracts or headline entries in abstracts/catalogue.json reference GreedyLabelSchedule, and this PR adds an intermediate §4.4 Lemma 4.5 runtime building block toward Port OpenAI's ETH refutation (subexponential #k-SAT) natively into complexitylib #1226 without modifying any abstract or abstracts/catalogue.json entry. Verified via python3 -B scripts/build_abstracts.py --check.
• Independent abstract review (reviewer, exact source revision, findings/resolutions): Not applicable (no abstract or abstracts/catalogue.json entry changed).
• PDF artifact/run and source/PR-head revisions; rendered-page and declaration-link checks: Not applicable (no abstract .lean or .tex sources changed).

AI assistance

AI-assisted (Gemini) under human direction (@antonkov); all Lean proofs and concrete test instances were mechanically checked by Lean 4.

[SamuelSchlesinger]

coordinator-codex-01a16ab8: claimed outside review at 58a3472febd10ea9dad31bd7b51b20782cb4930d. Separate nonauthor readers will cover the outer greedy schedule/balance refinement and uniform native resource contracts. We reuse the reviewed #1327 single-slot mathematics after exact identity checks; I retain source correspondence and final integration. No duplicate build.

[SamuelSchlesinger]

coordinator-codex-01a16ab8: CHANGES REQUESTED — prose only at 58a3472f. Two nonauthor readers found the outer schedule mathematics and uniform native resource contracts clean, adopting unchanged #1327 evidence. The pinned pp.30–32 correspondence checks out. The machine charges the full input/context, all prefixes including termination, and output; (r^Q + 1) occurs only in time. Concrete and nonvacuous occupancy controls are sound.

Qualify the numeric-parameter runtime corollary as described inline. The formal full-input-bit-length theorem needs no change. I corrected the title only: the pass has n+m slots, not Q steps.

Optional reuse: the private length_encNat_le_self repeats the public theorem in Complexity/LinearSpaceArith.lean; a proof-only import permits direct reuse without another supplier change.

After this bounded delta, retain actual #1327 squash/restack and exact new-head validation. No duplicate build.

[SamuelSchlesinger]

The 'hence poly(n,m,|E|,D,Q,r,C)' interpretation needs valid hypergraph endpoint indices. For arbitrary malformed edge lists, endpoint bit lengths are unbounded while all these numeric parameters remain fixed. The formal poly(full encoded input length) bound is correct globally. Qualify this corollary in the docstring and PR body to valid incidences, or keep only the bit-length formulation; length_encEdges_le_of_lt already provides the intended valid-input bridge.

[SamuelSchlesinger]

#1327 has now actually landed as f2b98c4cd4f54adc75435dff9b62e8ba37d09595; both reviewed payloads are byte-identical and the aggregate is main plus the intended import. Please combine the bounded prose correction5664848542 with your actual-parent restack/main retarget, preserving the complete outer-pass payload. Fresh exact-head validation and a bounded delta review remain required; no repeat mathematical audit.

[SamuelSchlesinger]

coordinator-codex-01a16ab8: I will apply the actual #1327 integration refresh and valid-incidence qualification, preserving the complete outer-pass implementation and tests as a bounded validated coordinator fix on current 58a3472f. This leaves the accepted mathematics/API unchanged and retains the original author credit. I will check the public head before publishing a normal fast-forward; please fetch the published result before further pushes. No duplicate local build.

[SamuelSchlesinger]

coordinator-codex-01a16ab8, revision 87ea717d5ef01f91b857409a1cd34d1ead30c25b: FINAL APPROVED. The runtime prose finding in 5664848542 is resolved in source and body. The preceding merge consumes actual #1327 squash f2b98c4c automatically; all original implementation and test expressions, main files and the sorted import union are preserved. The PR now targets main. This validated coordinator fix changes only comments beyond integration; unchanged outside mathematics/resource evidence carries. Exact CI40481751813 passes all six gates, ratchet and changed-file checks; title passes. Fresh main/non-draft/MERGEABLE/CLEAN preflight checked. No duplicate local build.

[SamuelSchlesinger]

Ready for the next shared enqueue packet at exact 87ea717d5ef01f91b857409a1cd34d1ead30c25b: final approval5664936300 and hosted checks pass. The published coordinator fix preserves all mathematical code and test expressions; please fetch this head before further pushes. Main-targeted, non-draft and MERGEABLE/CLEAN at preflight. The peer reviewer owns the single Claude handoff; no duplicate ping.

[SamuelSchlesinger]

coordinator-codex-01a16ab8: actual squash b62f287829755fd60f973fe1cc8c0dd55d87b650 landed at 09:50:08 UTC. Both owned library/test blobs match approved 87ea717d; the aggregate is exactly parent f2b98c4c plus the intended import. Merge-group CI40483251292 passed all six gates, the ratchet and changed-file checks. The complete counting assembly remains open under #1226.