# Translation conventions and evidence boundary

## What “proof in Julia” means in this package

There are three distinct components:

* **Mathematical proof:** complete analytic arguments, written as Julia raw strings in `ProofGuide.jl`, including induction and every interface in the central theorem. Standard real analysis and linear algebra are stated foundations. Running a string does not check its mathematical inference.
* **Executable certificates:** exact arithmetic identities, soundly enclosed transcendental quantities, polynomial reductions under established relations, and a finite conjunction over every state in the declared domain. These rely on the Julia implementation, compiler, runtime, GMP arithmetic, and hardware.
* **Implementation tests and numerical illustrations:** bounded signed-ledger and placement tests, and separately labeled BigFloat examples. They exercise executable implementations. They do not prove unbounded quantifiers.

The unchanged supplied Lean project remains the kernel-oriented formalization. Its archived build and axiom reports are preserved as supplied evidence; they were not freshly re-executed for this Julia translation. This package does not claim to reproduce Lean's kernel trust model or to create 147 Julia proof objects.

## Exact arithmetic and enclosure construction

Canonical integer arithmetic converts operands to `BigInt` before multiplication. All certificate endpoints are `Rational{BigInt}`. No decimal string is parsed as a binary floating-point input to a certificate.

`sqrt_enclosure` uses integer `isqrt` and a decimal denominator. The floor and square-root inequalities are established in P01. `pi_enclosure` uses finite alternating arctangent sums and the analytically proved, branch-checked identity `pi=16*atan(1/5)-4*atan(1/239)`. This is an independent route to the 20-decimal pi enclosure used by the source. The sign of the next term bounds the alternating-series remainder. Interval subtraction reverses the subtrahend endpoints.

The lambda enclosure uses monotonicity of `phi/(phi+pi)` in each positive argument. A rational outward coarsening to denominator `10^36` keeps the finite census efficient. Both its enclosure relation and its strict margins from `q`, `q+1/S`, `L`, and `U` are checked before use. A floor is certified only when both enclosing endpoint floors coincide.

The sine/cosine enclosures use eight-term rational Taylor sums at certified delta endpoints. Their monotonicity and remainder bounds are proved analytically in P01. They are additional exact sign certificates; they do not make calculus a finite computation.

`certified_truncation(p)` refines exact enclosures until the integer truncation is determined. It raises an error if its stated resource limit is reached. It never guesses an unresolved floor. The theorem for every natural `p` follows from monotonicity and the exact floor interval, independent of any ability to compute every precision in finite resources.

## Symbolic polynomial normalizer

`PolynomialCertificates.jl` represents sparse polynomials with exact rational coefficients and a fixed variable ordering. Every monomial reduction substitutes `phi^2=phi+1` or `c^2=1-s^2`. These relations are first established analytically. Each substitution preserves the value under any real assignment satisfying them; sums and products preserve equality. Therefore a zero reduced residual is a sufficient identity certificate under the relations.

The normalizer is ordinary readable Julia code, not a trusted proof kernel. Its use of the defining relations is explicit: a zero residual for `sc_identity` is a consistency check under that identity, not a new derivation of trigonometry. Some certificates verify a substitution or a cleared algebraic step after an analytic result. There are 97 labeled zero residuals, not 97 independent new theorems. Nonzero controls and an independent binomial expansion exercise the normalizer. Nonzero denominators, norm signs, module linearity, differentiation, and induction are supplied in the written proofs.

## Domain and API mapping

| Lean source convention | Julia translation |
|---|---|
| Natural canonical states | `F`, `rho`, and `iterate_state` reject negative states and use `BigInt` |
| Total signed Euclidean quotient/remainder | `ediv(x,b)=0` at `b=0`; otherwise `sign(b)*fld(x,abs(b))`. `emod(x,0)=x`; otherwise `mod(x,abs(b))` |
| Euclidean identity for every divisor | Preserved, including zero and negative divisors |
| `roundtrip` with `A!=0`, arbitrary `B` | `encode` and `recover` preserve this domain; `decode_checked` is an explicitly narrower validated API |
| `admissible_roundtrip` requires only `B>0` | Written proof and separate tests include `A=0`; the nonzero-multiplier hypothesis is not silently added |
| Source total `seedFromRemainder` on natural `r` | Public `seed_from_remainder` validates that `r` is even and in `[0,S)` before applying the same inverse formula. This is sufficient for all canonical remainder theorems and is an explicit API restriction |
| Real scalar roundtrip for every `h` | `scalar_encode_total` preserves totalized zero division on exact rational inputs; validated `scalar_encode` requires `h>0` |
| Real lambda | Its definition and analytically justified rational intervals are retained; `q` is used as the lambda floor only through the certified domain interface |
| Real module homotheties and observations | Universal proofs use module and linear-map laws; the polynomial certificates check the scalar algebra after those laws |
| Arbitrary real normed ambient space with real linear isometry | Universal proof in P03; `ExactPlacement` implements rational orthonormal frames in finite Euclidean spaces as a computable subclass |
| Arbitrary real signed scale in set identities | Written identities keep the full domain; `outline_spec` accepts signed rational radii. The positive-readout theorem retains its positivity requirement |
| Complete smooth curve as a parametric set | `outline_spec` stores exact angle coefficients, exact symbolic marks, and defining parameter rules; it is a full descriptor rather than a sampled polygon |
| Point and curve reconstruction for arbitrary retained real scale | Universal substitution proofs retain that scope. Checked executable reconstruction takes a positive rational grid scale |

Julia's ordinary `div` and `%` truncate toward zero, so they must not be substituted for the signed Euclidean interface. In the inverse ledger steps where the numerator is known divisible by the nonzero multiplier, all usual exact quotient conventions coincide; the implementation still retains the explicit interface.

## Explicit explanatory repairs and preserved source

The source archive is unchanged. Two clarifications are made in the new proof text:

1. The finite-certificate prose uses `0 <= S*(lambda-q)*d <= d` before the strict gap comparison. The inequality against `d` is strict for positive `d`, and becomes equality at `d=0`. This repairs the strict-at-zero wording in the supplied prose without changing the theorem or constants.
2. `arcLength(a,u,v)` is an oriented speed integral in the Lean definition. Its identity `a*(v-u)` holds for arbitrary `u,v` with `a>0`; an ordinary nonnegative length interpretation uses `u<=v`. The actual major-arc and semicircle intervals have this order.

The exact theorem `finite_certificate_inequality` itself only asserts the natural-number comparison `32767 < 34535026732`. P11 explains how that comparison participates in the complete real floor argument.

The generic `Ledger.lean` opening prose mentions positive numerator and denominator, but its individual theorem declarations deliberately include weaker hypotheses. The translation follows the declarations, including nonzero negative multipliers and, where permitted, zero or negative divisors.

## Finite verification populations

The canonical census covers every `d=0:32767`. It verifies the independent exact lambda-enclosure floor, the rational quotient and remainder, both endpoint conventions of the exact interval, the minimum gap, first-remainder decoding, scalar factorization, and all 23 ordered transitions. The reverse reconstruction compares every recovered intermediate state with the forward state, not merely the terminal result.

The generic generated-ledger population is `A=-7:7`, `B=-5:5`, `d=-30:30`, `n=0:5`. Conditional checks use exactly the applicable theorem hypotheses. The separate proposed-record population uses `A` in `{-3,-2,-1,1,2,3}`, `B=1:4`, terminal `t=-3:3`, lengths `0:3`, and each proposed remainder in `-1:B`. It compares admissibility against an independently enumerated encoding image. For `|t|<=3`, a reverse predecessor satisfies `|d| <= (B|t|+B-1)/|A|`; recursing its ceiling gives a sufficient seed range, so no valid candidate's preimage is omitted. Additional proposed-record checks cover the source's `A=0` admissible-roundtrip case.

These finite populations support implementation correctness. P09 supplies the universal integer proof; it is not inferred by extrapolating from these tests. Likewise, the 31 BigFloat scale examples are labeled numerical illustrations and are never premises of an exact result.