Bounded automation pilot — actual results

Historical pilot baseline

This page preserves the original run, including its P10 failure and its then-missing Lean checks. Current shared-proof wave: checked P10, rational foundations, composition pieces and independent Lean checks.

What actually passed

8 local arithmetic leaves passed fresh ordinary-HA replay: 3 full pilot instances and 5 supporting subleaves. 0 irrationality parent obligations closed; 0 library admissions. P07 covers signed-integer frequencies only; its quadratic-field lift remains open. No independent Lean rebuild was performed in this baseline.

All 15 exported arithmetic premises were regenerated and freshly replayed first. Modified certificate bodies and false original targets were rejected. Contract-specific mathematical mutation witnesses are a separate remaining validation task.

Native proofs and untrusted solver outcomes

Two CPU seconds per solver call. A classical hit is not an HA certificate. The two experimental arms use the same native proof factory: solver hits gate an independent native reproof, not a proof-log translation. This measures an integration baseline, not solver acceleration.

Recorded run: 72.49 wall seconds. Native-only child CPU: 20.20 s; solver-gated native replay: 20.31 s; solver/version probes: 25.83 s; checked basis setup: 0.39 s. One proof/solver worker at a time.

Proof workers made no model calls. Agents wrote and reviewed contracts, generators and infrastructure; that engineering cost is not measured as zero.

The large-number boundary is still open

P10 unresolved: original RSS stop; changed-strategy retry stopped at the internal copy-work cap. No further retry or limit increase.

P04 finite composition, P09 confluent trace, P10 large arithmetic assembly, and P12 CApprox trace are not proved. P10 has a separately elaborated full closed statement.

Next: assemble bounded per-operation proof DAGs, then the finite-composition and approximation traces. No larger search or memory allowance is implied.

Reproducible local evidence

Machine-readable results · Complete original run report (gzip) · Original twelve planning contracts. Certificates use the existing canonical bundle codec. Gzip is storage only; hashes bind the exact decompressed bytes. These observations are local, not promoted or deployed.

P01 · Full pilot contract · HA checked

RatEq addition for arbitrary signed numerator pairs; all four input denominators and both output products are nonzero naturals (therefore positive). Equality and product guards are in the actual target.

forall p m d P M D q n e Q N E. ~(d=0) -> ~(e=0) -> ~(D=0) -> ~(E=0) -> p*D+M*d=m*D+P*d -> q*E+N*e=n*E+Q*e -> (~(d*e=0) /\ (~(D*E=0) /\ ((p*e+q*d)*(D*E)+(M*E+N*D)*(d*e)=(m*e+n*d)*(D*E)+(P*E+Q*D)*(d*e))))

Download the actual canonical certificate (gzip) · 95,397 proof-body nodes.

Uncompressed SHA-256: b795adb8448c940d154eb897ee0d073935fe74f17e7bbc2130b299dea0d1954d

Planning parent: IR002 · Open its prerequisite cone. This parent remains unproved.

P02 · Supporting subleaf only · HA checked

Subtraction-free norm polynomial identity over natural coefficients. The lift to all signed coefficient pairs in P02 remains separate and is NOT closed by this target.

forall a b c d. (a*c+2*b*d)*(a*c+2*b*d)+2*(a*a)*(d*d)+2*(b*b)*(c*c)=2*(a*d+b*c)*(a*d+b*c)+(a*a)*(c*c)+4*(b*b)*(d*d)

Download the actual canonical certificate (gzip) · 95,721 proof-body nodes.

Uncompressed SHA-256: 31fc96456fd099820eafa28a3c5ba05d63bf6dc5e558dc2ed3e724a2b8a388f5

Planning parent: IR031 · Open its prerequisite cone. This parent remains unproved.

P03 · Supporting subleaf only · HA checked

One algebraic induction step with an explicit equality hypothesis. Rational representation and power/fold trace links in the full P03 contract remain open.

forall x y X Y T. X+y*T=Y+x*T -> x*X+y*(X+y*T)=y*Y+x*(X+y*T)

Download the actual canonical certificate (gzip) · 37,560 proof-body nodes.

Uncompressed SHA-256: 1db8573b8bebac8e38bb6f2aa3e236771115bb0c54ca74ef92269262e52d2081

Planning parent: IR009 · Open its prerequisite cone. This parent remains unproved.

P04 · Not dispatched

A precisely fixed finite composition and its coefficient witnesses remain to be connected to HA; 1=1 is not a replacement.

Planning parent: IR079 · Open its prerequisite cone. This parent remains unproved.

P05 · Full pilot contract · HA checked

Set k=n+2, so k>=2. a=f_k and b=f_(k-1) are explicitly assumed 2. The proposed next coefficient is the literal 2; this proves only the fixed recurrence step, not coefficient uniqueness or its base cases.

forall n a b. a=2 -> b=2 -> (S (S n)+1)*2=2*a+S n*b

Download the actual canonical certificate (gzip) · 13,109 proof-body nodes.

Uncompressed SHA-256: ed937acba56411b7789716e1ae0b4463d1e5eddb724cd7ab26e056d05849f32e

Planning parent: IR080 · Open its prerequisite cone. This parent remains unproved.

P06 · Supporting subleaf only · HA checked

The product-order algebra with an explicit nonnegative slack h. Positive rational denominator and factorial/power witness links remain required for full P06.

forall p u h C. C=2*p+h -> 2*(p*u)+h*u=C*u

Download the actual canonical certificate (gzip) · 13,211 proof-body nodes.

Uncompressed SHA-256: dbdbf733ccf8d084b3142e0d2007160d63cf284ea4f32e5691be0848f67b45a0

Planning parent: IR020 · Open its prerequisite cone. This parent remains unproved.

P07 · Full pilot contract · HA checked

The two-frequency identity for four arbitrary signed integers, represented by eight natural components. M0 and M1 are inlined by exact signed-pair addition/multiplication. The arbitrary-N quadratic moment theorem IR045 remains open.

forall a A b B c C d D. (((a*c+A*C)+(b*d+B*D))+(a*d+A*D))+((d*(A+B)+D*(a+b))+(a*C+A*c))=(((a*C+A*c)+(b*D+B*d))+(a*D+A*d))+((d*(a+b)+D*(A+B))+(a*c+A*C))

Download the actual canonical certificate (gzip) · 66,860 proof-body nodes.

Uncompressed SHA-256: ea174da14eb5e94cb02379430554e6120b71241ef6720fbda77da47488af45f9

Planning parent: IR045 · Open its prerequisite cone. This parent remains unproved.

P08 · Supporting subleaf only · HA checked

Cancellation algebra assuming the reciprocal recurrence d*v=u. This does not establish nonzero d, rational inverse existence, powers, or full P08. Removing d!=0 is not a falsehood test of THIS weaker conditional identity.

forall d u v m. d*v=u -> d*(m*v)=m*u

Download the actual canonical certificate (gzip) · 11,520 proof-body nodes.

Uncompressed SHA-256: 85ebc993da1043a31589d1daf95097a49411dfeb08df389d4324d73fb51569a5

Planning parent: IR055 · Open its prerequisite cone. This parent remains unproved.

P09 · Not dispatched

Exact r=1 coefficient tables are separately elaborated; native trace and denominator-clearing links remain required.

Planning parent: IR056 · Open its prerequisite cone. This parent remains unproved.

P10 · Not dispatched

The full closed statement is separately elaborated, but the binary certificate assembly hits its copy-work cap. Small binary proofs pass; this large target remains unresolved. Do not increase unary norm_num limits.

Planning parent: IR064 · Open its prerequisite cone. This parent remains unproved.

P11 · Supporting subleaf only · HA checked

Constructively transports an explicit additive witness for 12V<=e into the cleared precision comparison. The product V=KSJ and denominator positivity are still separate obligations; no rational interpretation is assumed by this formula.

forall V e. (exists h. 12*V+h=e) -> exists w. 3*(4*V)+w=e

Download the actual canonical certificate (gzip) · 5,369 proof-body nodes.

Uncompressed SHA-256: 0a345476732ce13319c24cfeea1c4d2728fce47ff08279d4d721c01ae94937fa

Planning parent: IR069 · Open its prerequisite cone. This parent remains unproved.

P12 · Not dispatched

The full fixed CApprox execution trace must be connected to its final rational comparison by HA proofs.

Planning parent: IR071 · Open its prerequisite cone. This parent remains unproved.