Alphabeta Math
AlgorithmAlgorithm: Literature-sourcedProof: Not applicablePipeline-generated
How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

  • Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
  • AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
  • AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Finite pseudo-arclength continuation of phase-fixed periodic orbits

Definition

Let f(x,μ) be a C2 one-parameter family in the map convention of Ck Euclidean maps and diffeomorphisms, and let G(x,T,μ) be the parameterized phase-bordered shooting map of Certified residual, Jacobian, trajectory, and monodromy enclosures for periodic shooting. For its static-parameter augmented field g(x,μ)=(f(x,μ),0), supply the common-tube hypotheses of A C2 vector field has a C2 flow on a common compact tube on each continuation neighborhood: an open set of initial states whose solutions exist on an open interval containing the required period range and remain in one compact convex subset of the field domain. That theorem makes the shooting map C2 on the declared neighborhood. The branch residual is F=G:Rd+2→Rd+1. If a fold check is requested, additionally supply a verified C3 neighborhood of the shooting map G on the fold subtube, as required by Finite-budget pseudo-arclength continuation with a certified local corrector; C2 regularity of f alone is not this evidence. Without it, retain fold status inconclusive and do not invoke the fold callback, while ordinary continuation may proceed without a fold request. A finite periodic-orbit continuation request supplies a valid certified Euclidean seed section-root ball with its isolating curve-chart neighborhood and rank certificate, as required by Finite-budget pseudo-arclength continuation with a certified local corrector, a unit orientation, step size, requested step count, finite continuation/corrector budgets, residual tolerance, angle margin, and the sound flow/jet range provider.

At a certified root, a tangent routine must certify a unit vector in ker⁡DF and a rank-d+1 condition. The predictor is advanced along that tangent. The periodic procedure Finite-budget phase-fixed periodic-orbit correction and validation in section mode supplies a separate Krawczyk certificate for the square shooting/section residual. Forward its complete finite input package: the candidate mode and any required differentiable pointwise/segment evaluators (or choose its enclosure-guided mode), rational initial candidate, arbitrary rational physical validation box and its open convex shooting domain, nonzero rational phase covector and rational reference point, validated-jet step counts and arithmetic caps, dyadic preconditioner and exact rational inverse witness for its normalized residual, physical minimum box width, and box/update budgets. It uses its affine dyadic unit-box chart for positive side lengths, retains the exact physical box and complete mapped partition, and returns inconclusive for validation on degenerate boxes while retaining their candidate use. For possibly nonrational tangent/predictor data, forward certified outward rational enclosures of the affine section row and its derivative; unavailable bounds return inconclusive. For every jet query reorder physical (x,T,μ) to the jet's (x,μ,T) coordinates, and return its Jacobian columns to (x,T,μ) before appending a section row. Preserve this rule in candidate, Krawczyk and continuation-evaluator calls.

Run Finite-budget pseudo-arclength continuation with a certified local corrector using its actual exact-evaluation or bounded-error branch and its own certified Euclidean root balls. A periodic Krawczyk box alone is not its ball certificate. Use the generic exact-evaluation branch only with separately supplied exact physical point-evaluation data; interval jet enclosures alone use the bounded-error branch. The local inverse and chart suppliers remain A simple neutral multiplier and transverse phase make the shooting Jacobian invertible and A transverse pseudo-arclength section has a locally quadratic Newton corrector, with every generic tangent, previous-normal, chart-angle, predictor-offset and finite-budget check retained. Supply the following finite-return evaluator and ball-certificate interfaces; an unavailable input returns the generic declared failure rather than an accepted step.

Physical evaluator bridge. At each exact queried point y=(x,T,μ), obtain a certified finite rational box containing y within the shooting domain and the declared physical continuation tube; use its singleton when y is rational. Every augmented range-provider tube inclusion required by the jet is checked separately in its own augmented coordinates. A nonrational query requires supplied certified coordinate enclosures, not substitution of a nearby rational point. Run the validated jet on that physical box with the stated coordinate/column permutation. Its residual and physical Jacobian intervals enclose F(y) and DF(y). Coordinatewise rational midpoints and the sums of the coordinate/entry radii give the generic evaluator's certified Euclidean residual error and operator-Jacobian error by Rational boxes admit dyadic enclosure boundaries and exact affine root charts. For its current affine section form the square residual G(y)=(F(y),τkT(y−zp)) and its physical Jacobian, appending sound interval enclosures of the affine row and its constant term; include all row uncertainty in the square midpoint/error data g^,A^,ϵg,ϵJ. These are derivatives in physical coordinates, not the normalized Krawczyk columns DF D. If only normalized data are retained, undo their known positive diagonal chart exactly and enclose the physical columns before forming these bounds. Missing finite point/row/error enclosures returns root-certificate-inconclusive; a certified domain/tube exit keeps the generic tube-exit status.

Required Euclidean ball certificate. At a generic candidate y, the callback supplies R>0, verifies that the whole B‾2(y,R) lies in the declared smooth shooting domain, physical continuation tube and current isolating chart neighborhood Vk, and supplies a sound finite L≥0 with ∥DG(u)−DG(v)∥op≤L∥u−v∥2 throughout that ball. This whole-ball bound is additional certified input, for example from a separately justified second-derivative bound on a covering tube. It is not inferred from first-derivative intervals, Krawczyk inclusion or the mere existence of a C2 field. The callback supplies an exact rational inverse witness V for the rational midpoint matrix A^, checked by both products VA^=A^V=I, or another sound inverse-bound certificate. For the exact witness take β^=∑i,j∣Vij∣. Verify the actual tests of A bounded residual and derivative error give a local root certificate: β^ϵJ<1,β=β^1−β^ϵJ,ρ=∥g^∥2+ϵg,q=βLR<1,βρ≤(1−q)R. A certified upper bound for ∥g^∥2 may replace the norm conservatively. Only a passing ball with the full chart/angle record can be appended by the generic algorithm. Missing witness, whole-ball Lipschitz, domain, chart or error data returns root-certificate-inconclusive; finite arithmetic failures and all generic budget/status distinctions remain explicit. A small residual, an exhausted Newton budget or a successful periodic Krawczyk call alone cannot append a continuation ball. If both a generic ball and a physical Krawczyk box are claimed to represent the same section root, additionally certify inclusion of the entire ball in that Krawczyk unique-root image box, or provide another sound common-root certificate; otherwise retain them as separate records without claiming coincidence.

When the fixed-parameter phase-bordered (x,T) Jacobian is certified invertible, the full derivative DF has row rank d+1: its (x,T) columns already span Rd+1. Thus a fold in the parameter projection does not by itself make the branch singular. Missing tangent/rank evidence, tube exit, failed Krawczyk inclusion, unresolved angle, or exhausted finite budgets returns the corresponding inconclusive status; no global branch-completeness claim is made. Any requested fold certificate is emitted only when the generic continuation algorithm's separate fold checks succeed.

The generic section keeps the supplied previous unit orientation fixed as its normal during each attempt, while the predictor uses the current certified tangent candidate. Forward this previous normal and certify its angle with the current true kernel, along with the generic predictor-offset/chart inequalities. Finite termination is conditional on every invoked flow/jet, tangent, section and fold callback returning in finite time; an outer work budget is not a timeout for a nonreturning callback.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

64 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources