Dilation: computation and proof scope
checks/dilation_type.py uses exact fractions.Fraction arithmetic for its finite assertions. It checks the algebraic fixed-width and interval-propagation conditions for rational scales and weights, the positive homogeneous weight-polynomial majorant, derivative bounds on a normalized simplex, the improved total-variation coefficient bound, and a distinct ordered-tree evaluation against the recurrence. Scalar examples and the explicit real type constants are displayed at high precision separately from exact assertions.
The finite checks do not establish universal analytic conclusions. The growth and convergence results depend on the proofs in Appendix A. Historical priority is a separate literature question. No numerical fit is presented as evidence that a type limit exists.
The earlier moving-width lower argument used a fixed \(\alpha<1\); it proved orders below \(\rho\) and then recovered the order by \(\alpha\uparrow1\), but did not establish positive lower type at \(\rho\). This is a limitation of that argument, not a counterexample. The fixed-width comparison closes precisely that missing implication. The evidence archive retains execution failures, their causes and the subsequent corrected runs.
Coupled growth: scope and open questions
The decisive extension is from a scalar positive comparison to a comparison weighted by a positive eigenvector. The fixed-width integral controls the lower type at the exact exponent. A fixed proportional interval \([\alpha R,R]\), with \(\alpha<1\), would only give a smaller exponent through \(\alpha^sP(s)\). Letting \(\alpha\) tend to one recovers exact order but does not, by itself, yield positive lower type. This is a limitation of that alternative route, not a failure of the theorem.
The complete proofs in Appendix F close the target on the strictly positive contraction domain. No computed example is used as a universal analytic premise. The displayed rational Taylor coefficients were evaluated directly from the exact recurrence with Python fractions.Fraction as a transcription check. Their independent algebraic residual checks belong to the archived exact computation record.
Remaining questions include the existence and value of ordinary type limits, possible oscillations, zeros, angular growth, connection formulas, and regimes with zero, negative, complex, or noncontracting scales. Positivity and strict contraction are hypotheses of the results here. This route makes no historical priority claim and no claim of a Lean formalization.
The preserved self-review checked coefficient and eigenvector notation, logarithm and power domains, seed and child interval endpoints, and both vector orientations. Its recorded conclusion was that no unresolved gap had been identified in that argument. This is a statement about the scope and outcome of that review, not a substitute for independent verification.
Coupled inverse: verification scope
The identities above are algebraic and the proofs use exact positive parameters. The companion check script compares the first coefficients against the full independent recursion, verifies the factorization over a rational grid, checks the candidate-selection formulas, and tests both reduction surfaces by comparing many exact Taylor coefficients. Finite checks test the implementation and the worked examples. The equivalence and recovery theorems follow from the proofs.
Historical priority of these specific statements remains a separate literature question.