ENG001/002 must freeze the exact formulas and authenticated premises first. Compare native-only and solver-hint runs on identical inputs; both share 60 CPU seconds / 90 wall seconds per child, 768 MiB RSS and 8 MiB output, with a 1,200-second aggregate ceiling and one local worker. No unchanged retries; a single changed-strategy repair uses the original reservation. External solver success counts only after reconstruction of the original HA target.
P01 · IR002
Addition respects RatEq for two pairs of positive-denominator triples: clear denominators and emit the cross-multiplied polynomial identity.
Method: native-ring.
Required hostile check: Drop one positive-denominator guard or swap a numerator sign.
This is the original planning contract. See actual bounded execution and exact coverage. A successful child does not close its universal parent.
P02 · IR031
For four arbitrary signed integers A,B,C,D, (AC+2BD)^2-2(AD+BC)^2=(A^2-2B^2)(C^2-2D^2), encoded as a subtraction-free natural equality.
Method: native-ring.
Required hostile check: Replace the coefficient 2 in the quadratic product by 3.
This is the original planning contract. See actual bounded execution and exact coverage. A successful child does not close its universal parent.
P03 · IR009
Power-difference induction STEP only: from witnessed e-th powers and their telescoping-sum identity derive the (e+1)-st identity using the sum recurrence. Freeze the exact induction hypothesis as a premise.
Method: native-ring.
Required hostile check: Omit the induction hypothesis or shift the final summand exponent.
This is the original planning contract. See actual bounded execution and exact coverage. A successful child does not close its universal parent.
P04 · IR079
Constant-coefficient BASE of formal exp(A): for the fixed positive-degree inner series with A_0=0, the coefficient of degree zero of the finite composition is 1.
Method: native-numeral.
Required hostile check: Allow a nonzero constant term in the inner series.
This is the original planning contract. See actual bounded execution and exact coverage. A successful child does not close its universal parent.
P05 · IR080
Recurrence STEP for k>=2 after f_k=f_(k-1)=2: justify the candidate f_(k+1)=2 in (k+1)f_(k+1)=2f_k+(k-1)f_(k-1). The k=0,1 boundaries stay separate parent obligations.
Method: native-ring.
Required hostile check: Use k instead of k+1 on the left-hand coefficient.
This is the original planning contract. See actual bounded execution and exact coverage. A successful child does not close its universal parent.
P06 · IR020
Single tail-contraction step: for x>=0, j>=0, j+1>=2x and t=x^j/j!>=0, the successor term x*t/(j+1)<=t/2. Clear strictly positive denominators and keep the product-order lemma explicit.
Method: native-order.
Required hostile check: Omit j+1>=2x and require a counterexample to be detected.
This is the original planning contract. See actual bounded execution and exact coverage. A successful child does not close its universal parent.
P07 · IR045
Two-frequency moment INSTANCE: M0=b0+b1, M1=b0*l0+b1*l1 imply M1+b0*l1=l1*M0+b0*l0. Signed values use coefficient-pair encoding; arbitrary N is not inferred.
Method: native-ring.
Required hostile check: Exchange b0 and b1 only on one side of the identity.
This is the original planning contract. See actual bounded execution and exact coverage. A successful child does not close its universal parent.
P08 · IR055
First reciprocal-coefficient step for the fixed factor (d+w)^(-m), m>=1,d!=0: c0=d^(-m), c1=-m*d^(-m-1), so d*c1+m*c0=0. Powers and inverse witnesses are explicit.
Method: native-ring.
Required hostile check: Change the sign of c1 or remove the nonzero-denominator premise.
This is the original planning contract. See actual bounded execution and exact coverage. A successful child does not close its universal parent.
P09 · IR056
Finite confluent INSTANCE r=1, ell*=3, x_j=j*L0 (j<7), 1/4<=L0<=1/2: the degree-7 monomial functional equals 1. Generate its exact reciprocal coefficients, clear 7!*(720L0)^7 and replay the resulting identity; no universal r claim.
Method: native-ring.
Required hostile check: Give the selected node multiplicity 1 instead of 2.
This is the original planning contract. See actual bounded execution and exact coverage. A successful child does not close its universal parent.
P10 · IR064
Closed constant inequality 2^55*3^11*7^5<=2^88. Compute exact integers and generate a double-and-add arithmetic certificate, not a floating-point comparison.
Method: native-numeral.
Required hostile check: Lower the right exponent to 85; the resulting inequality is false.
This is the original planning contract. See actual bounded execution and exact coverage. A successful child does not close its universal parent.
P11 · IR069
Precision-bridge arithmetic: K,S,J>0 and e>=12KSJ imply 3/e<=1/(4KSJ). Introduce an explicit product witness V=KSJ, prove its positivity, clear denominators, then isolate the linear leaf e>=12V.
Method: native-order.
Required hostile check: Replace 12 by 8 and demand rejection or a rational counterexample.
This is the original planning contract. See actual bounded execution and exact coverage. A successful child does not close its universal parent.
P12 · IR071
Fixed rational certificate INSTANCE a=3,b=2,n=6: generate the specified CApprox trace and prove |2*u_6-3|>4*2^(-6) in the unchanged kernel. This instance does not prove accuracy or universal irrationality.
Method: native-numeral.
Required hostile check: Mutate one approximation trace entry while retaining the claimed result.
This is the original planning contract. See actual bounded execution and exact coverage. A successful child does not close its universal parent.