# Complete mathematical proof companion

Generated verbatim from the literate proof strings in `src/ProofGuide.jl` by `scripts/export_guides.jl`.

These are mathematical arguments with exact Julia certificates at the stated interfaces. Julia does not kernel-check the universal logical, real, or calculus inferences. `THEOREM_GUIDE.md` maps all 147 original declarations individually.

## P01 — CONSTANTS AND RATIONAL ENCLOSURES (Constants.lean)


Definitions: phi=(1+sqrt(5))/2; epsilon=pi/648000; delta=epsilon/2;
s=sin(delta), c=cos(delta); lambda=phi/(phi+pi); mu=pi/(phi+pi).
The square root is the nonnegative real square root; pi is the usual positive
circle constant. Q=339949771344778, S=10^15, q=Q/S, D={0,...,32767}.

1. Let R=sqrt(5). R>0 and R^2=5. Then
   phi^2-phi-1=(R^2-5)/4=0 and phi>1/2>0. For positive L<U above 1/2,
   x^2-x-1 is strictly increasing: f(y)-f(x)=(y-x)(x+y-1)>0.
   Exact integer squaring, or rational evaluation of f, gives
   f(1.61803398874989484820)<0<f(1.61803398874989484821).
   Thus these are strict bounds on phi. This is the proof of phi_bounds;
   checking only floating-point approximations would not prove it.

2. This companion independently supplies the pi enclosure by Machin's identity.
   Put theta=atan(1/5), eta=atan(1/239). The addition formula gives
   tan(2 theta)=5/12, tan(4 theta)=120/119, and
   tan(4 theta-eta)=(120/119-1/239)/(1+120/(119*239))=1.
   All displayed denominators are positive. From
   atan(x)=integral_0^x 1/(1+t^2) dt, for x>0,
   x/(1+x^2)<atan(x)<x. Also pi=4 atan(1)>2.
   Consequently 0<4*(1/5)/(1+1/25)-1/239<4 theta-eta<4/5<pi/2.
   On (0,pi/2), tangent is injective. Therefore 4 theta-eta=pi/4,
   proving pi=16 atan(1/5)-4 atan(1/239), with the branch justified.
   For |x|<1, integrating the finite geometric-series identity for 1/(1+t^2)
   proves the alternating arctangent expansion and a remainder strictly between
   zero and the next term, with that term's sign. Exact partial sums therefore
   enclose both arctangents. Subtracting intervals with reversed endpoints gives
   strict rational pi bounds. The program checks these lie strictly inside
   (3.14159265358979323846,3.14159265358979323847), reproducing the bounds used
   by Constants.lean through a separate analytic route.

3. The isqrt certificate also encloses sqrt(5): if M=10^digits and
   n=isqrt(floor(5 M^2)), then n^2<=5 M^2<(n+1)^2. Division by M^2 and the
   increasing nonnegative square root give n/M<=sqrt(5)<(n+1)/M.
   The general sqrt_enclosure uses floor(x M^2) for nonnegative rational x.
   phi and pi are positive; phi+pi>0. Thus lambda>0, lambda<1,
   lambda+mu=(phi+pi)/(phi+pi)=1, and mu=1-lambda.
   The function f/(f+p) increases with positive f and decreases with positive p:
   subtracting two such fractions gives a numerator p(f2-f1), respectively
   f(p1-p2), over a positive denominator. Thus the computed endpoint formulas
   for lambda enclose its exact real value. Exact cross multiplication checks
   q<lambda_lo<=lambda<=lambda_hi<q+1/S.
   This proves lam_bounds, q_lt_lam, lam_lt_q_plus with strict outer bounds.

4. Since pi>0 and 0<1/1296000<1/2, 0<delta<pi/2. Standard sine/cosine signs
   on that interval imply s>0 and c>0. The identity sin^2(t)+cos^2(t)=1 follows
   by differentiating the left side, obtaining zero, and evaluating it at t=0.
   In particular s^2+c^2=1. The rational Taylor enclosures provide additional
   certified sign checks for this particular seed: on [0,1] the alternating
   sine/cosine terms decrease, and the next term bounds the remainder. Cosine
   is positive there (cos x >= 1-x^2/2>0), hence sine increases and cosine
   decreases, justifying evaluation at the appropriate interval endpoints.
   Finally (pi/648000)*(180/pi)*3600=1, since pi!=0 and 180*3600=648000.

The algebra normalizer uses phi^2=phi+1 and c^2=1-s^2 only after these analytic
identities have been established. Its reduction of sc_identity is a consistency
check under that relation, not an independent proof of trigonometry.

## P02 — MARKED CONSTRUCTION AND SELECTED READOUT (Geometry.lean)


For real a,z put p(a,z)=(ac,az), identified with ac+i az in C. Define
z0=s, z1=1+s, z2=phi^2+s. The six levels are -z2,-z1,-z0,z0,z1,z2.
The outline is the image of gamma_a(t)=a(cos t,sin t) for
delta<=t<=2pi-delta, together with p(a,[s,phi^2+s]) and
p(a,[-(phi^2+s),-s]). This is a parametric union, not a sampled polygon.

1. At t=delta the circle point is p(a,s); periodicity and parity give
   gamma_a(2pi-delta)=p(a,-s). Re(p)=ac and Im(p)=az for every real a,z.
   Complex conjugation sends p(a,z) to p(a,-z). Sequential extensions give
   p(a,s)+ia=p(a,1+s), and p(a,1+s)+ia phi=p(a,phi^2+s), because 1+phi=phi^2.
   Negating the imaginary displacements gives the two lower equations.
   Consecutive level gaps are phi,1,2s,1,phi, all positive by P01; hence the
   levels are strictly ordered. Any labeled six complex points with these
   real and imaginary coordinates agree pointwise with marks(a). Extensionality
   proves uniqueness under those labeled coordinate rules, including a=0.

2. For a>0, p(a,z)-p(a,w)=(0,a(z-w)), so its Euclidean norm is a|z-w|.
   The inner length is a|(1+s)-s|=a; the upper outer length is
   a|(phi^2+s)-(1+s)|=a phi, and the lower outer length is the same.
   The complete extension length is a phi^2. The seed chord is 2as.
   The upper outer interval [1+s,phi^2+s] is contained in [s,phi^2+s].
   Its lower reflection is likewise contained in the lower extension. Thus
   both measured straight segments belong to the specified outline.

3. gamma'_a(t)=a(-sin t,cos t); its squared norm is a^2, so for a>0 its
   speed is the constant a. The oriented integral from u to v is a(v-u)
   for all real u,v. It is geometric arc length when u<=v. This is precisely
   the total interval-integral definition used by arc_length in Lean; the
   companion does not interpret a negative oriented integral as a length.
   The opposite semicircle interval [pi/2,3pi/2] lies in [delta,2pi-delta],
   by delta<pi/2. Image inclusion places it in the retained major arc and
   hence in the outline. Its speed integral is C=a*pi.
   To prove no retracing, equal circle points for a!=0 imply t-u=2m*pi for
   an integer m. Two parameters in the major interval satisfy
   |t-u|<=2pi-2delta<2pi, so m=0 and t=u. Thus the retained parametrization
   is injective for a>0.

4. Define G as the AVERAGE of both outer lengths; this selected measurement
   gives G=(a phi+a phi)/2=a phi. Set W=G+C. Then W=a(phi+pi)>0 and
   G/W=lambda, C/W=mu, after cancelling the positive a. Choosing this readout
   is part of the specification; evaluating it is a derived metric identity.
   The complete outline component length is
   a(2pi-epsilon)+2a phi^2. Subtracting W gives a(pi-epsilon+phi+2)>0,
   because epsilon=pi/648000<pi. W is therefore distinct from outline length.
   No uniqueness of the selected observables among all possible readouts is
   used or asserted.

## P03 — PLACEMENT, SCALING, AND GEOMETRIC RECONSTRUCTION (Placement.lean)


Let V be a real normed vector space, alpha in V, and E:C->V a real linear
isometric embedding. Set P(z)=alpha+E(z). These are the full theorem hypotheses;
the exact rational matrix API covers only computable examples of them.

1. P(z)-P(w)=E(z-w), whose norm is ||z-w||. Hence all distances are preserved.
   A linear isometry is continuous. The chain rule gives
   (P o gamma_a)'(t)=E(gamma'_a(t)); its norm equals ||gamma'_a(t)||=|a|
   for every real a, and equals a when a>0. Translation has zero derivative.
   The placed outer mean equals G and the placed semicircle integral equals C
   for every real a; for a>0, P02 gives a phi, a pi and the same lambda.
   This covers every such embedding and any center without reading that data
   from the integer ledger.

2. For all real k,a,z,t, k p(a,z)=p(ka,z) and k gamma_a(t)=gamma_ka(t).
   The parameter intervals are independent of a. Apply these pointwise
   identities to their images and use that image commutes with union: scaling
   the outline gives outline(ka), including k=0. Furthermore
   alpha+k(P(z)-alpha)=alpha+E(kz). Thus the homothety centered at alpha
   carries the placed outline of a to the placed outline of ka.
   For k>0,a>0, P02 gives G(ka)=kG(a), C(ka)=kC(a). Negative k still satisfies
   the set identity, but that signed scaling is not this positive-readout law.

3. By P09, recover(Q,S,encode(Q,S,n,d))=d for every integer d, n>=0.
   Substitution into the radius h*d gives the exact same placed outline for
   every real h and fixed alpha,E. This is curve_reconstruction; it consumes
   the retained scale, center and frame in addition to the ordered ledger.
   A positive-radius provenance statement requires h*d>0. At radius zero,
   the descriptor is the degenerate termination object. Equality as a set is
   still meaningful there. The positive h checked reconstruction API is an
   explicitly narrower, validated realization of this substitution identity.

## P04 — AFFINE DIMENSION, CENTERED RANK, AND GRAM MATRIX (Dimension.lean)


1. For every real a, all marks have first coordinate ac; equivalently
   p(a,z)=(ac,0)+az(0,1). They are collinear, even when a=0. If a>0,
   p(a,s)-p(a,-s)=(0,2as)!=0 because s>0. Their affine span is consequently
   exactly that line, with direction span((0,1)) and dimension one.

2. Given (x,y) in R^2, with a>0 and c,s>0, define
   b_plus=(x/(ac)+y/(as))/2, b_minus=(x/(ac)-y/(as))/2.
   Then b_plus*(ac,as)+b_minus*(ac,-as)=(x,y), coordinate by coordinate.
   Both denominators are nonzero. The two seeds span R^2, so all six marks
   span the plane relative to the center. That span has dimension two.
   Adjoining the center 0 to an affine generating set makes its affine
   direction equal to its linear span: combinations with coefficients summing
   to one use the remaining coefficient on 0. Thus its affine dimension is two.

3. Form the 2-by-6 coordinate matrix X, first row ac, second row a z_i.
   Symmetric levels sum to zero. Direct multiplication gives
   X X^T=diag(6(ac)^2,2a^2[s^2+(1+s)^2+(phi^2+s)^2]).
   The equality is valid for every a; if a>0 both diagonal entries are positive,
   so X has rank two. Equivalently its seed-column minor is -2a^2cs!=0.
   The Gram entry (X^T X)_ij is a^2(c^2+z_i z_j).
   For any real vector v, v^T X^T X v=||Xv||^2; hence ker(X^T X)=ker(X).
   Rank-nullity therefore gives rank(X^T X)=rank(X)=2. This is an analytic
   rank proof; an approximate singular-value cutoff is not used.

4. An injective real linear map E restricts to an isomorphism between the
   two-dimensional span and its image, so that dimension is preserved. The
   ambient dimension can exceed two. Translation is handled relative to the
   retained center; it does not turn the six-mark affine dimension into two.

## P05 — EUCLIDEAN METRICS (Metrics.lean)


For arbitrary real a,z,w, the dot product of p(a,z) and p(a,w) is
a^2(c^2+zw). For a>0, squaring the norm gives a^2(c^2+z^2); both the norm
and a sqrt(c^2+z^2) are nonnegative, so they agree. Since c>0, these radii
are nonzero. The definition of the cosine of the unoriented Euclidean angle
as dot/(norm*norm) therefore gives
  cos(angle(p(a,z),p(a,w)))=(c^2+zw)/(sqrt(c^2+z^2)*sqrt(c^2+w^2)).
For z=s,w=-s, c^2+s^2=1 reduces this to c^2-s^2=cos(2delta)=cos(epsilon).
Both the unoriented angle and epsilon belong to [0,pi]. Cosine is injective
on that interval, so the seed angle equals epsilon, exactly.

The determinant is (ac)(aw)-(az)(ac)=a^2 c(w-z). Half its absolute value
is a^2 c |z-w|/2, because a^2>=0 and c>0. This last area identity holds
for every real a, including zero and negative values. The formulas have
arbitrary signed levels and therefore cover all fifteen distinct mark pairs.

## P06 — WEIGHTED MEAN, HOMOTHETIES, AND GRID COORDINATES (Affine.lean)


1. Let a>0,x real. By P01-P02 the weighted mean denominator is a(phi+pi)>0.
   Subtracting 1 from (a phi x+a pi)/(a phi+a pi) gives
   a phi(x-1)/(a(phi+pi))=lambda(x-1). Therefore it equals
   T(x)=1+lambda(x-1). In particular T(x)-1=lambda(x-1).
   Induct on n: n=0 gives x=1+1*(x-1); applying T to the induction
   hypothesis yields 1+lambda^(n+1)*(x-1). Thus the affine iterate formula
   holds for every natural n and every real x, without rounding.

2. In any real module define H_k(z)=alpha+k*(z-alpha), with k real.
   Substitution and the distributive/module laws give H_k(H_l(z))=H_(kl)(z)
   and H_1(z)=z. For a real linear L, put v_L(z)=1+L(z-alpha).
   Since L(k*(z-alpha))=kL(z-alpha),
   v_L(H_k(z))=1+kL(z-alpha)=1+k(v_L(z)-1).
   Apply k=lambda^n and part 1 for observation_iterate. No injectivity of L
   is required. With arbitrary intercept b, subtraction gives
   [b+kL(z-alpha)]-[1+k(b+L(z-alpha)-1)]=(1-k)(b-1).
   For all k the centered convention b=1 supplies the interface; for the
   special k=1 any intercept works, as the defect formula also records.

3. lambda>0 permits real powers defined by lambda^t=exp(t log(lambda)).
   The exponential addition law gives lambda^(t+u)=lambda^t lambda^u for
   all real t,u. Combining with H_k H_l=H_(kl) proves real_time_semigroup.
   This is an analytic proof, not a check at finitely many real times.

4. Define quantize_h(y)=h floor(y/h) and K_h(y)=quantize_h(lambda*y).
   If h>0 and d is any integer, lambda*(h*d)/h=lambda*d, so
   K_h(h*d)=h floor(lambda*d). This is a grid-coordinate identity; it does
   not assert a finite floor certificate for negative d or unrestricted d.
   The natural-domain certificate and repeated-quantization induction are P07
   and P10. In particular the unquantized affine iterate in part 1 cannot be
   substituted for repeated grid quantization.

## P07 — FLOOR DYNAMICS AND THE EXACT PARAMETER INTERVAL (Floor.lean)


1. Exact integer comparisons show 0<Q<S. For each natural d, Euclidean
   division gives Qd=S F(d)+rho(d), 0<=rho(d)<S, with F(d)=floor(Qd/S).
   Dividing by S>0 gives F(d)<=qd<F(d)+1, proving floor_q. F(0)=0.
   If d>0, Qd<Sd, so F(d)<d; for d=0 equality holds, hence F(d)<=d in all
   cases. Therefore D is forward invariant. Q>0 also gives monotonicity:
   d<=e implies Qd/S<=Qe/S and taking floors preserves that inequality.

2. Let L=4196/12343 and U=7039/20706. Exact cross multiplication verifies
   L<q<U. The strict rational enclosure in P01 lies inside (L,U), so L<lambda<U.
   Suppose d is natural with d<32768 and k is an integer with Ld<k<Ud.
   Then X=12343k-4196d and Y=7039d-20706k are positive integers, at least 1.
   The exact determinant 7039*12343-4196*20706=1 yields
   d=20706X+12343Y>=33049, contradicting d<32768. No such interior boundary
   exists. This is a universal integer argument, not a sampled search.

3. Fix any real r with L<=r<U. At d=0 all floors are zero. At d>0 put f=F(d).
   If rd<f, then Ld<=rd<f<=qd<Ud, so integer f is a forbidden boundary.
   If f+1<=rd, then Ld<qd<f+1<=rd<Ud, so f+1 is forbidden. Consequently
   f<=rd<f+1 and floor(rd)=F(d) throughout D.
   Conversely, floor-table equality at d=12343 uses F(12343)=4196 and gives
   r>=4196/12343. Equality at d=20706 uses F(20706)=7038 and gives
   r<7039/20706. Thus for EVERY real r,
     (for every d in D, floor(rd)=F(d)) iff L<=r<U.
   The lower endpoint is included and the upper excluded. This proves
   exact_parameter_interval and, by L<lambda<U, certified_floor_equality.

4. For any such r, realStep(r,d)=max(0,floor(rd)) agrees with F on D, since
   these successors are nonnegative. At depth zero their iterates are d.
   If equality holds for depth n at every state in D, one-step agreement
   followed by forward invariance applies that hypothesis at F(d). This
   proves trajectory_equality for every finite depth, not merely depth 23.

The companion additionally intersects the exact inequalities
F(d)/d<=r<(F(d)+1)/d for 1<=d<32768 and computes their maximum lower and
minimum upper endpoints. That exhaustive finite verification checks the same
L,U independently of the determinant argument.

## P08 — DECIMAL PRECISION (the truncation theorems in Floor.lean)


Define q_p=floor(10^p lambda)/10^p for every natural p, including zero.
The denominator is positive and floor(x)<=x, so q_p<=lambda. If
m=floor(10^p lambda), then 10m is an integer <=10^(p+1)lambda; hence
10m<=floor(10^(p+1)lambda), which proves q_p<=q_(p+1). Induction gives
monotonicity for any p<=r. Exact bounds on lambda certify
q_7=3399497/10^7 and q_8=33994977/10^8. Exact comparison gives q_7<L<=q_8.

If p<8, then p<=7 and q_p<=q_7<L, which violates the necessary lower
endpoint in P07. If p>=8, then q_p>=q_8>=L and q_p<=lambda<U, so P07
gives complete floor agreement. Therefore agreement holds iff p>=8 for
ALL natural p. The finite sweep 0:18 is additional verification. It is not
the proof for precisions beyond that sweep, and it does not replace q=Q/S.

## P09 — ORDERED EUCLIDEAN LEDGERS (Ledger.lean)


The source's integer division is total Euclidean division: for B!=0,
q=sign(B)*floor(x/abs(B)), r=x-Bq in [0,abs(B)); for B=0, q=0,r=x.
These conventions preserve x=Bq+r even for zero/negative divisors. Julia's
ediv/emod implement them explicitly; ordinary div/% are not silently used.
Let step(A,B,d)=ediv(Ad,B), rem(A,B,d)=emod(Ad,B).

1. For all integers A,B,d, Ad=B step+rem. If B>0, 0<=rem<B.
   If A!=0, ediv(B step+rem,A)=ediv(Ad,A)=d, with no restriction on B.
   Encoding n steps retains (d_n,[r_0,...,r_(n-1)]) in forward order.
   Recovery is recover(t,[])=t and
   recover(t,r::rs)=ediv(B recover(t,rs)+r,A); thus it consumes the right end
   first. Induct on n: the empty ledger recovers d; the induction hypothesis
   recovers the first successor from the tail, and the one-step inverse
   recovers d. This proves roundtrip for A!=0, every B and every integer d.
   The same recursion gives list length n, even when A=0 or B=0.

2. Admissible(t,[]) is true. A nonempty r::rs is admissible exactly when
   the tail is admissible, 0<=r<B, and emod(B recover(t,rs)+r,A)=0.
   Generated ledgers are admissible when A!=0 and B>0: by induction the tail
   is admissible, P09.1 gives the remainder bounds, and roundtrip identifies
   B recover(t,rs)+r with Ad, divisible by A.
   If B>0, Ad=Be+r, and 0<=r<B, division by B yields e<=Ad/B<e+1.
   Therefore step(A,B,d)=e and the Euclidean identity then forces rem=r.
   This is canonical_division, which itself does not require A!=0.

3. Conversely take any admissible record with B>0. Induct on its length.
   For the empty record, encoding its terminal with depth zero is itself.
   Put e=recover(t,rs), d=ediv(Be+r,A). Admissibility implies Ad=Be+r.
   If A=0, the modulus-zero convention makes Be+r=0 and d=0, so this equality
   still holds. Canonical division gives precisely the required e,r.
   Apply the induction hypothesis to the tail; encoding d returns exactly
   (t,r::rs). This proves admissible_roundtrip with the source's weaker
   hypothesis B>0, not an unannounced assumption that A!=0.

4. For A!=0, equality of two encoded records implies equality of their
   recoveries by part 1, hence equality of their seeds: encoding_injective.
   Combine parts 2-3 with that injectivity to prove, for A!=0,B>0,
     admissible(t,rs) iff there exists exactly one integer d whose encoding
     with depth length(rs) equals (t,rs).
   Applying step repeatedly to the reconstructed seed recovers all later
   states, for every natural j, including j beyond the retained depth.

5. Define V([])=0, V(r::rs)=A^length(rs)*r+B V(rs).
   For any admissible record (without extra restrictions on A,B), induction
   gives A^n recover(t,rs)=B^n t+V(rs). At the induction step put m=length(tail).
   Admissibility gives A*d=B*e+r; multiply by A^m and substitute
   A^m e=B^m t+V(tail):
     A^(m+1)d=B*(B^m t+V(tail))+A^m r
             =B^(m+1)t+[A^m r+B V(tail)].
   The empty case uses A^0=B^0=1, including 0^0=1 in this polynomial context.
   For generated records with A!=0,B>0, use roundtrip and length n to obtain
     A^n d_0=B^n d_n+sum_(j=0)^(n-1) B^j A^(n-1-j) r_j.
   The sum equals the recursive V: separate the head and multiply the tail
   coefficients by B. The order of remainders is retained, not discarded.

## P10 — SCALAR INTERFACE, RESIDUAL TYPES, AND GRID TRAJECTORIES (Interface.lean)


1. Define e=floor(y/h), residual=y-h*e, D_h(e,r)=h*e+r. Substitution proves
   D_h(E_h(y))=y for all real h,y under Lean's total convention y/0=0.
   scalar_encode_total preserves that convention on exact rational inputs.
   If h>0, floor bounds multiplied by h give 0<=residual<h.
   Conversely if e is an integer and 0<=r<h, then
   e<=(he+r)/h<e+1, so E_h(he+r)=(e,r). These are the two scalar coordinate
   directions of the frozen external interface. No SRSD algorithms are added.

2. Euclidean division with Q,S gives rho(d)/S=qd-F(d) for every natural d.
   On D, P07 gives floor(lambda*d)=F(d); hence
     lambda*d-floor(lambda*d)=rho(d)/S+(lambda-q)*d.
   Since lambda>q, the correction is strictly positive for positive d, and
   zero at d=0. Floor agreement does not equate these two residuals.
   Likewise E_S(Qd)=(F(d),rho(d)) by scalar canonicality, and the signed
   ledger step and remainder at Q,S and natural d coincide with F and rho.

3. For h>0 and d in D, P06.4 and P07 give K_h(hd)=hF(d). Induct on n,
   starting with hd at n=0; invariance ensures the induction hypothesis
   applies to F(d). Thus K_h^[n](hd)=hF^[n](d) for every natural n.
   The counterexample is d=26: F(26)=8, F(8)=2. Exact rational lambda bounds
   verify 3<26*lambda^2<4, so one rounding after unquantized squaring yields 3.
   These are different operations.

4. For B>0 and any integers A,d,e, step(A,B,d)=e iff
   Be<=Ad<B(e+1), immediately from floor bounds after multiplying by B.
   With a retained real scale h, center alpha and linear frame L:R->V,
   the realized point is alpha+L(h*d). P09 roundtrip substituted for d
   proves point_reconstruction for every real h, with no injectivity of L
   required for this equality. P03 gives the analogous outline substitution.

## P11 — FINITE GAP CERTIFICATE AND FIRST REMAINDER (Finite.lean)


1. The Euclidean algorithm on the displayed integers gives gcd(Q,S)=2.
   Put M=S/2=500000000000000 and H=Q/2=169974885672389.
   Exact multiplication verifies
     H*281419755786509=1+95668581631527*M.
   Thus I=281419755786509 is a multiplicative inverse of H modulo M.
   Write Hd=Mk+r with 0<=r<M; then Qd=Sk+2r, so rho(d)=2r and
   rho(d)/2=(Hd) mod M. Multiplication by I gives
     (I*(rho(d)/2)) mod M=d mod M.
   If 0<=d<M, the right side is d; this proves first_remainder_reconstruction.
   Equal remainders give equal reconstructed seeds, so rho is injective on
   that full period and hence on D, since 32768<M. Seeds differing by M
   have the same remainder; the restricted domain is essential.

2. Independently of the determinant proof, enumerate d=256b+i with
   0<=b<128 and 0<=i<256. Exact division of Qd by S for every pair proves
     S-rho(d)>=34535026732.
   The program writes each block's minimum and an exact state table; the
   universal finite statement is exactly the conjunction of those 32768
   checked inequalities. Its minimum is attained at d=20706. Every d in D
   has exactly one such block representation, from Euclidean division by 256.
   Exact comparison gives 32767<34535026732.

3. By P01, 0<lambda-q<1/S. For d in D,
     0<=S*(lambda-q)*d<=d<=32767<34535026732<=S-rho(d),
   with the second inequality strict when d>0 and equality at d=0.
   Thus 0<=rho(d)/S+(lambda-q)*d<1. In Qd=S F(d)+rho(d) this proves
   F(d)<=lambda*d<F(d)+1. This is the complete finite-certificate proof of
   floor agreement, including zero. The original prose's strict '<d' at
   d=0 is explicitly repaired in this new explanation; reference files remain
   unchanged. This Julia finite conjunction is checked by Julia/GMP, not Lean's
   kernel. The original Lean finite theorem and its proof remain in reference/.

## P12 — EXTINCTION THRESHOLDS (Extinction.lean)


For natural d,t, with Q,S positive,
F(d)<t iff Qd<St iff d<St/Q iff d<ceil(St/Q).
The last equivalence uses integrality of d; at t=0 both sides are false.
For nonnegative integer St, ceil(St/Q)=floor((St+Q-1)/Q).
Set t_0=1 and t_(n+1)=ceil(S t_n/Q). At depth zero,
F^[0](d)=0 iff d=0 iff d<t_0. If the assertion holds at depth n, then
F^[n+1](d)=0 iff F(d)<t_n iff d<t_(n+1). This proves extinction_threshold
for all natural n,d. Exact integer recurrence evaluation yields
  1,3,9,27,80,236,695,2045,6016,17697,52058.
Since every d in D is below 52058, every seed is zero by step ten.
It is nonzero at step nine iff d>=17697, so precisely 17697:32767 need
the tenth step. F(0)=0 implies by induction F^[j](0)=0 for every j;
composing ten steps with thirteen more proves the twenty-three-step result.

## P13 — CENTRAL PROVENANCE THEOREM (Main.lean)


Take any real normed V, center alpha in V, real linear isometric embedding
E:C->V, and positive real scales a,h. P01-P03 prove the placed readouts
G=a phi, C=a pi and G/(G+C)=lambda. P06 proves the selected weighted mean
(Gx+C)/(G+C)=1+lambda(x-1) for every real x. P07 proves
floor(lambda*d)=F(d) for all d in D; P10 gives the repeated grid identity
for every natural depth n. P09, specialized to A=Q!=0 and B=S>0, proves
roundtrip for every integer seed and finite depth, and characterizes exactly
the records belonging to unique initial integers by admissibility.
Conjoining these established statements gives precisely the central theorem.
P03 and P10 also prove geometric reconstruction when scale, center and frame
are retained. No one of those retained data is inferred from the ledger.

Typed dependency chain:
INPUTS/DEFINITIONS: positive scale; phi; one-arcsecond seed; labeled extension
rules; parametric curve; center and isometric frame.
DEFINITION: select the mean outer length and opposite semicircle length.
DERIVED METRICS: G=a phi, C=a pi, W=G+C=a(phi+pi).
NORMALIZATION: divide by positive W to obtain lambda,mu.
ALGEBRAIC IDENTITY: chosen weighted affine mean and centered homothety observation.
COORDINATE INTERFACE: independent grid scale h and floor quantizer.
FINITE-DOMAIN EQUALITY: real-lambda floor table equals canonical rational table
exactly on D, using either P07 or P11, extended to trajectories by invariance.
ENCODING: terminal state plus ordered Euclidean remainders, with admissibility.
ADDITIONAL REALIZATION DATA: h, alpha, E and positive radius when invoking the
positive geometric provenance result. Reconstruction uses these explicitly.

The scale-independent readout is supplied by the specified marked geometry
together with its selected measurement rule. This statement does not require
the selected rule to be the unique possible measurement of an unmarked outline.