Alphabeta Math
ExampleConstruction: AI-generatedVerification: AI-generatedPipeline-generatedprecheck pass
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.

The constant-code slope transform at a=100: the invariant slope of h↦1/(2r+−h) and the cone constants

Example

Take a=100, so L=74, k=1/2, and let r+=1+101 be the constant-code value of the all-+1 code. The fixed slope of the forward transform Φy(h)=1/(2y−h) at y=r+ is the small root of h=1/(2r+−h), i.e. of

h2−2r+h+1=0:h=r+−r+2−1=1r++r+2−1,

and one has 0<h<1/2. Moreover λ=2L−k=274−12>1 and Φr+ maps [−1/2,1/2] into [−λ−1,λ−1]⊆[−1/2,1/2] with Lipschitz constant λ−2<1/2.

Facts & Assumptions

Given: The parameter a=100, the constants L=74, k=1/2, r+=1+101, and the slope maps of Stable and unstable cones, invariant line slopes, stable and unstable sets, and transverse homoclinic points of the quadratic family.

[L1]

Slope transform data (Stable and unstable cones, invariant line slopes, stable and unstable sets, and transverse homoclinic points of the quadratic family, Cone invariance and expansion, and convergence of the slope graph transforms to unique invariant stable and unstable line fields): for L≥2, 0<k<1, k(2L−k)≥1, ∣y∣≥L and ∣h∣,∣h′∣≤k, the forward slope map satisfies ∣Φy(h)∣≤(2L−k)−1 and ∣Φy(h)−Φy(h′)∣≤(2L−k)−2∣h−h′∣; under these hypotheses the cone Cku is invariant under DF at points with second coordinate of absolute value at least L, with expansion factor 2L−k>1.

[L2]

Constant-code check using The square-root recurrence Ts(x)n=sna+xn−1+xn+1 is a contraction of BR with a unique coded solution, clause 4: for the given r+=1+101, direct expansion gives r+2=100+2r+ and 0<r+<12<13=R. Thus the constant sequence xn=r+ lies in BR and satisfies r+=100+2r+; uniqueness of the coded fixed point identifies it with the all-+1 code.

[L3]

Square roots and inequalities (Square roots exist: a unique a≥0 with (a)2=a; the positives are {x2:x≠0}, Absolute value in an ordered field, Basic properties of the absolute value): r+>10 because 101>10; r+2−1>r+−1; 274>17 because 4⋅74=296>289=172.

Verification

technique · direct; solve the fixed-slope equation exactly and evaluate the cone constants at $a=100$
1.1givenL2L3algebra

Fixed slope: the equation h=1/(2r+−h) is equivalent to h2−2r+h+1=0, whose roots are r+±r+2−1; the small root is h=r+−r+2−1=1/(r++r+2−1). Since r+>10 and r+2−1>9, one has 0<h<1/(10+9)<1/2.

2.1givenstep 1.1L1L3algebra∎

Cone constants: L=74>8≥2 and 0<k=1/2<1. Also r+>10>L, since 74<100. By [L3], λ=274−12>17−12>1; also k(2L−k)=12(274−12)>12⋅16>1, so the invariance and expansion hypotheses of [L1] hold with λ=274−12. The induced bounds are ∣Φr+(h)∣≤λ−1<1/2 and ∣Φr+(h)−Φr+(h′)∣≤λ−2∣h−h′∣ with λ−2<1/2, in agreement with [L1].

Remarks

  • The fixed slope h is the slope of the invariant unstable line at the fixed point in the cone C1/2u; the computation uses only the exact fixed-point relation r+2=100+2r+ and rational estimates for the two square roots.

Depends on

Dependency tree · 2 levels

Sources