Reference
Signed rationals
136 modules in src/rainbow/math/rational/signed/. All folders
| Module | What it proves | Theorems |
|---|---|---|
| math.rational.signed.absolute | Native absolute value for signed rational proof data. | 5 |
| math.rational.signed.absolute-algebra | Quotient-safe algebra for native signed absolute value. | 5 |
| math.rational.signed.absolute-convex | Absolute value is convex -- the canonical non-smooth convex function, the basis of L1 / robust / minimax objectives. | 1 |
| math.rational.signed.absolute-multiply | Brick 3 of limit-product: |a * b| ~ |a| * |b| over signed rationals. | 1 |
| math.rational.signed.absolute-reciprocal | B5 of the limit-reciprocal arc: the absolute value of a reciprocal, kept through the SAME magnitude(x*x) representative (avoids the absent magnitude-respects / nnrat reciprocal-respects lemmas -- the nnrat-radius-cancel philosophy). | 1 |
| math.rational.signed.absolute-reciprocal-times-self | B6f prerequisite: the multiplicative absolute reciprocal identity. | 1 |
| math.rational.signed.absolute-sign | Sign characterization of absolute value over signed rationals: 0 <= w => |w| ~ w w <= 0 => |w| ~ -w Foundational reusable lemmas (needed by the sign case-splits in limit-product's distance-multiply and absolute-multiply bricks). | 2 |
| math.rational.signed.add-associative | Associativity of signed-rational addition up to Grothendieck equivalence. | 1 |
| math.rational.signed.add-zero-reflection | A zero sum of two nonnegative signed rationals has zero summands. | 2 |
| math.rational.signed.additive-distance | Distance bounds from two-sided additive signed inequalities. | 4 |
| math.rational.signed.affine-convex | Affine functions are convex (indeed the convexity inequality is an equality) -- the first substantive instance of signed/convex-on, and the fact that makes linear/affine LP objectives convex (KKT/Lagrangian relevance). | 1 |
| math.rational.signed.big-m | Soundness of the indicator ("big-M") reformulation. | 2 |
| math.rational.signed.clamp | Projection of a signed rational into a closed interval. | 7 |
| math.rational.signed.close-of-distance | B6f lever: build a closeness band from a distance bound (the converse of dist-of-close). | 1 |
| math.rational.signed.close-product | Brick 4 (band) of limit-product: the product close-band. | 1 |
| math.rational.signed.close-radius-monotone | Band weakening: a closeness band only widens with its radius. | 1 |
| math.rational.signed.constrained-duality | Lagrangian duality with a CONCRETE penalty: an explicit finite constraint system with explicit multipliers. | 3 |
| math.rational.signed.convergence | Real-analysis roadmap step 5: the epsilon-N convergence predicate over signed-rational sequences, and the SQUEEZE THEOREM -- the first genuinely-frontier analysis result and the checkpoint that the epsilon-N machinery goes through in this kernel. | 1 |
| math.rational.signed.convergent-bounded | Brick 1 of analysis/limit-product: a convergent sequence is bounded. | 1 |
| math.rational.signed.convergent-bounded-below | Brick 1 of analysis/limit-reciprocal: a convergent sequence is bounded BELOW near its limit. | 1 |
| math.rational.signed.convex-closure | Closure properties of signed-rational convexity -- the algebra that makes a convex objective composable from convex parts (the convex-optimization bedrock). | 3 |
| math.rational.signed.convex-combination | Two-point convex combination of signed rationals stays within [min, max] -- the signed lift of nnrat/convex-at-most-max / convex-at-least-min, and a foundation brick for convex optimization over signed rationals (connects to the KKT / Lagrangian lane). | 2 |
| math.rational.signed.convex-function | The two-point convex-function representation over signed rationals, and its first witnesses -- the base for Jensen's inequality and for connecting convexity to the KKT / Lagrangian optimization lane. | 3 |
| math.rational.signed.convex-optimality | First-order optimality for convex objectives over signed rationals. | 3 |
| math.rational.signed.decide-completeness | Completeness of Rainbow's exact-rational decision procedures. | 13 |
| math.rational.signed.decide-equivalence | A computable, sound equality test for signed rationals. | 1 |
| math.rational.signed.decide-order | A DECIDABLE signed-rational order -- the per-instance half of a certificate. | 2 |
| math.rational.signed.decide-reflexive | Decision-level reflexivity for exact rational order. | 3 |
| math.rational.signed.deviation-rows | The two-row encoding of a magnitude bound says exactly what it looks like. | 3 |
| math.rational.signed.distance | A quotient-safe scalar metric interface for signed rationals. | 10 |
| math.rational.signed.distance-additive | Paired-addition Lipschitz law for quotient-safe signed distance. | 1 |
| math.rational.signed.distance-multiply-absolute | Brick 2 of limit-product: distance scales by the ABSOLUTE value of a sign-indefinite left factor. | 1 |
| math.rational.signed.distance-multiply-nonnegative | Nonnegative signed multiplication bounds quotient-safe distance. | 1 |
| math.rational.signed.distance-negate | d(-a,-b) ~ d(a,b): distance is invariant under negating both points. | 1 |
| math.rational.signed.distance-product | Brick 4 (core) of limit-product: the bilinear distance bound for a product. | 2 |
| math.rational.signed.distance-translation | Translation invariance of quotient-safe signed distance. | 3 |
| math.rational.signed.distance-triangle | Triangle laws for quotient-safe signed absolute value and distance. | 3 |
| math.rational.signed.distributive | Distributivity of signed multiplication over addition, and the scaled finite sum. | 3 |
| math.rational.signed.dyadic-jensen | Dyadic (four-point) Jensen for signed-rational convex functions -- n-point Jensen for the power-of-two case, reachable WITHOUT the reciprocal wall that blocks general n-point Jensen (which needs weight renormalization by 1/(1-w0)). | 2 |
| math.rational.signed.equivalence-laws | Symmetry and negation transport for Grothendieck-pair signed equivalence. | 2 |
| math.rational.signed.fubini | Finite Fubini for signed sums, and the double-counting weak-duality theorem it powers. | 3 |
| math.rational.signed.gap-quality | Universal additive quality from a certified endpoint and reported gap. | 2 |
| math.rational.signed.geometric-bridge | Bridge exact NNRAT geometry into signed-rational proof data. | 5 |
| math.rational.signed.half-scale-subtract-self | B6e of the limit-reciprocal arc: subtracting half of a value from itself leaves half. | 1 |
| math.rational.signed.indexed-max | Index-aware MAX aggregation -- the argmax semantic core, continuing the non-invasive Level-6 line (indexed-sum -> indexed-max). | 3 |
| math.rational.signed.indexed-max-attains | Attainment for the index-aware max -- the other half of argmax correctness (with dominance). | 2 |
| math.rational.signed.indexed-max-dominates | Full dominance for the index-aware max: every index below n is bounded by the aggregate. | 1 |
| math.rational.signed.inverse-unique | B6f lever (replaces the awkward multiply-right-cancel): uniqueness of multiplicative inverse. | 1 |
| math.rational.signed.kkt-sufficiency | KKT sufficiency: a stationary, feasible, complementary point is a global optimum of a convex program. | 3 |
| math.rational.signed.lagrangian-duality | Lagrangian duality for general constrained optimization over signed rationals. | 3 |
| math.rational.signed.limit-arithmetic | Axiom-free additive arithmetic for signed-rational limits. | 3 |
| math.rational.signed.limit-difference | The difference limit law for signed-rational sequences. | 2 |
| math.rational.signed.limit-negate | Negation preserves signed-rational closeness and limits. | 2 |
| math.rational.signed.limit-order | Limits preserve the pointwise order of signed-rational sequences. | 1 |
| math.rational.signed.limit-product | The product limit law: the pointwise product of two convergent signed-rational sequences converges to the product of the limits. | 1 |
| math.rational.signed.limit-scalar-laws | Axiom-free constant and nonnegative-scalar laws for signed order bands. | 3 |
| math.rational.signed.limit-scale | Axiom-free nonnegative scaling of signed-rational order bands. | 1 |
| math.rational.signed.limit-scale-law | Scalar multiple of a limit -- the missing piece of limit linearity. | 2 |
| math.rational.signed.limit-square | A direct corollary of analysis/limit-product: the square of a convergent signed sequence converges to the square of the limit. | 1 |
| math.rational.signed.limit-uniqueness | Uniqueness of limits for the signed-rational epsilon-N convergence predicate. | 4 |
| math.rational.signed.list-sum | Finite sums of signed rationals over a list, and their order laws. | 5 |
| math.rational.signed.lp-capacity-sensitivity | Capacity sensitivity for signed LP dual bounds. | 2 |
| math.rational.signed.lp-certificate | A worked LP optimality certificate on concrete numbers, including a NEGATIVE cost -- the per-instance end of the verified-optimization pipeline. | 3 |
| math.rational.signed.lp-certificate-reflect | LP optimality certificates by reflection over finite row and column lists. | 2 |
| math.rational.signed.lp-duality | Linear-programming weak duality and the optimality certificate over SIGNED rationals -- arbitrary matrix, costs and right-hand side, any of them negative. | 3 |
| math.rational.signed.lp-duality-on | LP weak duality and the optimality certificate, quantified over the rows and columns an instance actually has. | 3 |
| math.rational.signed.lp-equality-row | Formal equality-row expansion into two signed inequality rows. | 3 |
| math.rational.signed.lp-equality-row-transport | Generic feasibility transport from an original equality to certified actual positive/negative row maps and RHS entries. | 2 |
| math.rational.signed.lp-free-price | Equality dual-price splitting over signed rationals. | 4 |
| math.rational.signed.lp-objective-negate | Generic finite-sum negation and formal LP minimization sense transport. | 3 |
| math.rational.signed.lp-scaling-bound | Transport a bound between formal D^2/D-scaled objectives to original sums. | 2 |
| math.rational.signed.lp-scaling-feasibility | Forward feasibility scaling and universal-bound transport on listed indices. | 3 |
| math.rational.signed.magnitude | Layer 3 (capstone) of the signed->nnrat magnitude foundation. | 2 |
| math.rational.signed.magnitude-monotone | B6 prerequisite: magnitude is monotone on nonnegatives. | 1 |
| math.rational.signed.map-sum-algebra | Algebra of signed finite sums: congruence, splitting, and the weighted bound. | 7 |
| math.rational.signed.map-sum-scale | Nonnegative-rational scaling of signed indexed sums and bilinear objectives. | 4 |
| math.rational.signed.matrix-lp-dimension-decision-duality | Signed matrix LP weak duality from executable dimension decisions. | 1 |
| math.rational.signed.matrix-lp-duality | Signed LP weak duality over native finite matrices and vectors. | 1 |
| math.rational.signed.matrix-lp-row-length-duality | Signed matrix LP weak duality from concrete dimension certificates. | 1 |
| math.rational.signed.max-three | Reusable optimality certificate for a fixed three-candidate maximum. | 5 |
| math.rational.signed.midpoint-convexity | Midpoint convexity over signed rationals: the midpoint stays in [min, max]. | 2 |
| math.rational.signed.minmax | Universal minimum and maximum over signed rationals. | 6 |
| math.rational.signed.minmax-algebra | Algebraic and monotonicity laws for signed extrema. | 8 |
| math.rational.signed.multiply | Signed-rational multiplication, extending the addition-only signed rationals. | 3 |
| math.rational.signed.multiply-associative | Associativity of signed multiplication, and the outer swap the LP column bound needs. | 2 |
| math.rational.signed.multiply-monotone | Scaling a signed inequality by a nonnegative signed scalar. | 2 |
| math.rational.signed.multiply-nonzero | General signed no-zero-divisors: signed/multiply-zero-split : (a*b ~ 0) -> (a ~ 0) or (b ~ 0) signed/multiply-nonzero : not(a ~ 0) -> not(b ~ 0) -> not(a*b ~ 0). | 2 |
| math.rational.signed.multiply-order | The sign rules for signed-rational multiplication. | 8 |
| math.rational.signed.multiply-positive | signed/multiply-positive : 0 < a -> 0 < b -> 0 < a*b. | 1 |
| math.rational.signed.multiply-ring | Signed multiplication is commutative and well defined on the Grothendieck quotient. | 5 |
| math.rational.signed.negate-additive | Signed negation distributes over addition up to signed equivalence. | 1 |
| math.rational.signed.no-zero-divisors | No-zero-divisors sub-foundation for strict convexity: nonzero facts and (building up) a != 0 -> b != 0 -> a*b != 0. | 3 |
| math.rational.signed.one-hot-attained | THE ONE-HOT SELECTOR / ATTAINMENT LEMMA, the shared Level-3 reading of every checker that certifies a minimum or maximum with a 0/1 witness (the max/min-type checks). | 2 |
| math.rational.signed.one-hot-keep | THE ONE-HOT ATTAINMENT LEMMA WITH A KEEP OPTION, in the sign convention the relaxation checkers use (Bellman-Ford round, Dijkstra step, Floyd-Warshall round). | 2 |
| math.rational.signed.one-hot-selects | THE ONE-HOT VALUE SELECTOR, the shared Level-3 reading of every checker that pins a value to a one-hot sum: Floyd-Warshall's pivot column and row, Dijkstra's chosen label and row, and the rest. | 2 |
| math.rational.signed.one-hot-unique | A ONE-HOT SELECTOR SELECTS ONE INDEX. | 3 |
| math.rational.signed.order | Order and structural laws for signed rationals. | 2 |
| math.rational.signed.order-cancellation | Additive cancellation for signed-rational order. | 2 |
| math.rational.signed.order-monotone | Real-analysis roadmap step 6a: signed order is monotone under addition -- signed/add-right-monotone : a <= b -> (a + c) <= (b + c) signed/add adds pos/neg componentwise (pos(a+c) = pos a + pos c, etc. | 3 |
| math.rational.signed.order-respects | Equivalence transport for signed order and signed-sequence convergence. | 2 |
| math.rational.signed.order-transitivity | Real-analysis roadmap step 4: transitivity of the signed-rational order. | 1 |
| math.rational.signed.pointwise-order | Pointwise order over the indices a problem actually has. | 4 |
| math.rational.signed.product-radius-nonneg | First sub-proof of the limit-product modulus assembly: the radius base V = (1 + |L|) + |M| is nonnegative (indeed a sum of nonnegatives), so signed/from-nnrat-magnitude applies to it. | 1 |
| math.rational.signed.product-radius-positive | Second sub-proof of the limit-product modulus assembly: the magnitude of the radius base V = (1+|L|)+|M| has a positive numerator, so nnrat/make-succ-of-positive-numerator and analysis/nnrat-radius-cancel apply to it. | 1 |
| math.rational.signed.rate-order | Order closure under vanishing signed-rational error bounds. | 2 |
| math.rational.signed.rational | Signed rationals as proof data: a pair (positive, negative) of nonnegative rationals denoting positive - negative. | 4 |
| math.rational.signed.reciprocal | The signed-rational reciprocal operation and its self-inverse law -- the missing field operation. | 2 |
| math.rational.signed.reciprocal-absolute-bound | Layer A of the limit-reciprocal assembly: bound the absolute reciprocal of x by the reciprocal of a positive lower bound on |x|. | 1 |
| math.rational.signed.reciprocal-antitone | B4 of the limit-reciprocal arc: reciprocal reverses order on positives, plus the two reusable order<->subtract-nonneg bridges it needs. | 3 |
| math.rational.signed.reciprocal-difference | The reciprocal-difference identity: the algebraic heart of the limit-reciprocal law. | 1 |
| math.rational.signed.reciprocal-nonnegative | B3 of the limit-reciprocal arc: the reciprocal of a nonnegative signed rational is nonnegative. | 1 |
| math.rational.signed.recovery-laws | Two general signed-rational laws that the corpus lacked, proved en route to the Gauss-Seidel exactness theorem and promoted here so any module can reuse them without depending on an application module. | 2 |
| math.rational.signed.scale-additive | Nonnegative-rational scaling distributes over signed addition up to Grothendieck equivalence. | 1 |
| math.rational.signed.scale-composition | Composition of nonnegative scaling on signed rationals. | 1 |
| math.rational.signed.scale-order | Nonnegative-rational scaling preserves signed order. | 1 |
| math.rational.signed.scale-reflection | Positive rational scaling reflects signed order. | 2 |
| math.rational.signed.square-convex | Square convexity over signed rationals -- the canonical non-trivial convex function. | 6 |
| math.rational.signed.square-minimizer-unique | Concrete OR-Commons decision object: the square objective (\x. | 1 |
| math.rational.signed.square-monotone | B6b of the limit-reciprocal arc: squaring is monotone on nonnegatives. | 1 |
| math.rational.signed.square-nonzero | signed/square-nonzero : not(d ~ 0) -> not(d*d ~ 0). | 2 |
| math.rational.signed.square-numerator-positive | B6d of the limit-reciprocal arc: the positivity derivation the assembly calls. | 1 |
| math.rational.signed.square-numerator-positive-of-absolute | B6f prerequisite (s-n positivity transfer): a lower bound on |x| makes x*x have positive magnitude-numerator. | 1 |
| math.rational.signed.square-of-sum | The four-term expansion of a squared sum over signed rationals -- a reusable step for square convexity (the variance inequality) and other quadratic identities. | 1 |
| math.rational.signed.square-strict-convex | Strict convexity of the square, the capstone of the no-zero-divisors work: signed/strict-convex-on f := forall w0 w1 x y, 0<w0 -> 0<w1 -> (w0+w1 ~ 1) -> x !~ y -> f(wsum) < wsum(f x, f y) signed/square-strict-convex : strict-convex-on (\x. | 3 |
| math.rational.signed.square-zero | A signed rational whose square is zero is itself zero. | 1 |
| math.rational.signed.stl | Signed minimum and maximum for signal temporal logic (STL) robustness. | 2 |
| math.rational.signed.strict-convex-unique | Uniqueness of the minimizer for a strictly convex function -- the OR-Commons payoff of the convexity lane: a strictly convex objective has at most one minimizer (up to equivalence). | 2 |
| math.rational.signed.strict-order | Strict order on signed rationals -- the foundation strict convexity (and unique-minimizer results) need, which the non-strict `signed/at-most` lane lacked. | 8 |
| math.rational.signed.structural-equality | Decidable STRUCTURAL equality for nonnegative and signed rationals. | 8 |
| math.rational.signed.unit-laws | The unit and self-cancellation laws the signed layer was missing. | 5 |
| math.rational.signed.upper-bound-program | A worked constrained program, certified end-to-end by the general duality theorem -- the non-vacuity witness for the signed Lagrangian stack. | 3 |
| math.rational.signed.vector-sup-congruence | Quotient-safe congruence of signed-list sup distance. | 3 |
| math.rational.signed.vector-sup-distance | Finite maxima and sup distance for signed-rational list vectors. | 18 |
| math.rational.signed.vector-sup-separation | Zero separation for signed-list sup distance at fixed shape. | 3 |
| math.rational.signed.vector-sup-translation | Fixed-shape translation invariance of signed-list sup distance. | 2 |
| math.rational.signed.vector-sup-triangle | Triangle inequality for equal-shaped signed-rational list vectors. | 1 |