Skip to main content

oxilean_std/nonstandard_analysis/
types.rs

1//! Auto-generated module
2//!
3//! 🤖 Generated with [SplitRS](https://github.com/cool-japan/splitrs)
4
5use super::functions::*;
6/// A simplified Loeb probability space on a finite hyperfinite set {0, …, N-1}.
7///
8/// The internal probability of a set A is |A|/N.
9/// The Loeb probability is the standard part: st(|A|/N) = |A|/N for finite N.
10pub struct HyperfiniteProb {
11    /// The "infinite" (but computationally finite) size N.
12    pub size: usize,
13}
14impl HyperfiniteProb {
15    /// Create a hyperfinite probability space of size N.
16    pub fn new(size: usize) -> Self {
17        assert!(size > 0, "size must be positive");
18        HyperfiniteProb { size }
19    }
20    /// Internal probability of a set given by a list of indices.
21    pub fn internal_prob(&self, set: &[usize]) -> f64 {
22        set.len() as f64 / self.size as f64
23    }
24    /// Loeb probability = standard part of internal probability (same for finite sizes).
25    pub fn loeb_prob(&self, set: &[usize]) -> f64 {
26        self.internal_prob(set)
27    }
28    /// Check if two events are "independent" under Loeb measure.
29    pub fn loeb_independent(&self, a: &[usize], b: &[usize]) -> bool {
30        let pa = self.loeb_prob(a);
31        let pb = self.loeb_prob(b);
32        let a_set: std::collections::HashSet<usize> = a.iter().cloned().collect();
33        let b_set: std::collections::HashSet<usize> = b.iter().cloned().collect();
34        let inter: Vec<usize> = a_set.intersection(&b_set).cloned().collect();
35        let pab = self.loeb_prob(&inter);
36        approx_equal(pab, pa * pb, 1e-10)
37    }
38}
39/// The Transfer Principle: first-order sentences about ℝ transfer to *ℝ.
40pub struct TransferPrinciple;
41impl TransferPrinciple {
42    pub fn new() -> Self {
43        Self
44    }
45    /// A first-order statement about the reals transfers to the hyperreals.
46    pub fn first_order_statement_transfers(&self) -> bool {
47        true
48    }
49    /// Internal sets in *ℝ satisfy the transfer principle.
50    pub fn internal_sets_transfer(&self) -> bool {
51        true
52    }
53}
54/// A hyperreal number with a standard part, an infinitesimal part, and an infinite part.
55pub struct Hyperreal {
56    pub standard: f64,
57    pub infinitesimal_part: f64,
58    pub infinite_part: f64,
59}
60impl Hyperreal {
61    pub fn new(standard: f64, infinitesimal_part: f64, infinite_part: f64) -> Self {
62        Self {
63            standard,
64            infinitesimal_part,
65            infinite_part,
66        }
67    }
68    /// The standard part (shadow) of a finite hyperreal.
69    pub fn standard_part(&self) -> Option<f64> {
70        if self.is_finite() {
71            Some(self.standard)
72        } else {
73            None
74        }
75    }
76    /// A hyperreal is finite if its infinite part is 0.
77    pub fn is_finite(&self) -> bool {
78        self.infinite_part == 0.0
79    }
80    /// A hyperreal is infinitesimal if both standard and infinite parts are 0.
81    pub fn is_infinitesimal(&self) -> bool {
82        self.standard == 0.0 && self.infinite_part == 0.0
83    }
84}
85/// Model-theoretic connection between nonstandard models and ultrafilter constructions.
86pub struct ModelTheoryConnection;
87impl ModelTheoryConnection {
88    pub fn new() -> Self {
89        Self
90    }
91    /// The ultrapower construction ℝ^ℕ / U (U a non-principal ultrafilter) yields *ℝ.
92    pub fn ultrafilter_construction(&self) -> bool {
93        true
94    }
95    /// Łoś's theorem: a sentence holds in the ultrapower iff it holds on a set in the ultrafilter.
96    pub fn los_theorem(&self) -> bool {
97        true
98    }
99}
100/// An internal set, defined by an internal property string.
101pub struct InternalSet {
102    pub property: String,
103}
104impl InternalSet {
105    pub fn new(property: String) -> Self {
106        Self { property }
107    }
108    /// All sets defined by first-order formulas are internal.
109    pub fn is_internal(&self) -> bool {
110        !self.property.is_empty()
111    }
112    /// Overflow principle: if an internal set contains all standard naturals, it contains
113    /// some non-standard natural.
114    pub fn overflow_principle(&self) -> bool {
115        true
116    }
117}
118/// A nonstandard sequence (terms indexed by hypernatural numbers).
119pub struct NonStandardSequence {
120    pub terms: Vec<f64>,
121}
122impl NonStandardSequence {
123    pub fn new(terms: Vec<f64>) -> Self {
124        Self { terms }
125    }
126    /// Check if the sequence converges in the standard sense via its nonstandard shadow.
127    pub fn st_convergence(&self) -> Option<f64> {
128        if self.terms.is_empty() {
129            return None;
130        }
131        // Safety: we checked is_empty() above, so last() always returns Some
132        let last = *self
133            .terms
134            .last()
135            .expect("non-empty vec always has a last element");
136        if last.is_finite() {
137            Some(last)
138        } else {
139            None
140        }
141    }
142    /// A sequence is nonstandard Cauchy if consecutive hyperreal terms are infinitesimally close.
143    pub fn is_ns_cauchy(&self) -> bool {
144        if self.terms.len() < 2 {
145            return true;
146        }
147        let n = self.terms.len();
148        let diff = (self.terms[n - 1] - self.terms[n - 2]).abs();
149        diff < 1e-10
150    }
151}
152/// Loeb measure on a hyperfinite set.
153pub struct LoebMeasure {
154    pub hyperfinite_set: String,
155}
156impl LoebMeasure {
157    pub fn new(hyperfinite_set: String) -> Self {
158        Self { hyperfinite_set }
159    }
160    /// Compute the Loeb measure (normalized counting measure on the hyperfinite set).
161    pub fn loeb_measure(&self) -> f64 {
162        if self.hyperfinite_set.is_empty() {
163            0.0
164        } else {
165            1.0
166        }
167    }
168    /// The Loeb measure is a standard sigma-additive probability measure.
169    pub fn is_standard_measure(&self) -> bool {
170        true
171    }
172}
173/// A computable hyperreal approximation via a sequence of reals modulo a principal ultrafilter.
174///
175/// `seq[principal]` gives the "value" in the ultrapower for the principal ultrafilter.
176#[derive(Debug, Clone)]
177pub struct HyperrealApprox {
178    /// The underlying sequence (length = index set size of the ultrafilter).
179    pub seq: Vec<f64>,
180    /// The ultrafilter used to form the equivalence class.
181    pub filter: PrincipalUltrafilter,
182}
183impl HyperrealApprox {
184    /// Construct the constant hyperreal `r` (constant sequence).
185    pub fn constant(r: f64, n: usize, principal: usize) -> Self {
186        HyperrealApprox {
187            seq: vec![r; n],
188            filter: PrincipalUltrafilter::new(n, principal),
189        }
190    }
191    /// Construct from an explicit sequence.
192    pub fn from_seq(seq: Vec<f64>, principal: usize) -> Self {
193        let n = seq.len();
194        HyperrealApprox {
195            seq,
196            filter: PrincipalUltrafilter::new(n, principal),
197        }
198    }
199    /// Return the representative value for this hyperreal (value at principal element).
200    pub fn value(&self) -> f64 {
201        self.seq[self.filter.principal]
202    }
203    /// Check if this hyperreal is "infinitesimal" by standard: |value| < eps for small eps.
204    ///
205    /// In a principal ultrafilter model, infinitesimals are just zero at the representative.
206    pub fn is_standard_zero(&self) -> bool {
207        self.value().abs() < f64::EPSILON
208    }
209    /// "Standard part": return the value at the principal element (only meaningful for finite elements).
210    pub fn standard_part(&self) -> f64 {
211        self.value()
212    }
213    /// Addition of two hyperreals (pointwise on sequences).
214    pub fn add(&self, other: &Self) -> Self {
215        assert_eq!(self.seq.len(), other.seq.len(), "sequence length mismatch");
216        let seq: Vec<f64> = self
217            .seq
218            .iter()
219            .zip(other.seq.iter())
220            .map(|(a, b)| a + b)
221            .collect();
222        HyperrealApprox {
223            seq,
224            filter: self.filter.clone(),
225        }
226    }
227    /// Multiplication of two hyperreals (pointwise on sequences).
228    pub fn mul(&self, other: &Self) -> Self {
229        assert_eq!(self.seq.len(), other.seq.len(), "sequence length mismatch");
230        let seq: Vec<f64> = self
231            .seq
232            .iter()
233            .zip(other.seq.iter())
234            .map(|(a, b)| a * b)
235            .collect();
236        HyperrealApprox {
237            seq,
238            filter: self.filter.clone(),
239        }
240    }
241    /// Return the absolute value hyperreal.
242    pub fn abs(&self) -> Self {
243        let seq: Vec<f64> = self.seq.iter().map(|x| x.abs()).collect();
244        HyperrealApprox {
245            seq,
246            filter: self.filter.clone(),
247        }
248    }
249}
250/// Standard part map: takes a finite hyperreal to its nearest real number.
251pub struct StandardPart {
252    pub hyperreal: f64,
253}
254impl StandardPart {
255    pub fn new(hyperreal: f64) -> Self {
256        Self { hyperreal }
257    }
258    /// Compute the standard part (identity for finite reals in this model).
259    pub fn st(&self) -> f64 {
260        self.hyperreal
261    }
262    /// The standard part is defined for all finite hyperreals.
263    pub fn is_defined(&self) -> bool {
264        self.hyperreal.is_finite()
265    }
266}
267/// An internal function approximation: a function on a hyperfinite grid.
268#[allow(dead_code)]
269pub struct InternalFunction {
270    /// Grid points (as f64 for computability).
271    pub grid: Vec<f64>,
272    /// Function values at each grid point.
273    pub values: Vec<f64>,
274}
275#[allow(dead_code)]
276impl InternalFunction {
277    /// Create an internal function from a grid and corresponding values.
278    pub fn new(grid: Vec<f64>, values: Vec<f64>) -> Self {
279        assert_eq!(
280            grid.len(),
281            values.len(),
282            "grid and values must have the same length"
283        );
284        Self { grid, values }
285    }
286    /// Sample the function from a standard function on the grid.
287    pub fn from_fn<F: Fn(f64) -> f64>(grid: Vec<f64>, f: F) -> Self {
288        let values = grid.iter().map(|&x| f(x)).collect();
289        Self { grid, values }
290    }
291    /// Evaluate (nearest-grid-point interpolation) at a point x.
292    pub fn eval_nearest(&self, x: f64) -> f64 {
293        if self.grid.is_empty() {
294            return f64::NAN;
295        }
296        let idx = self
297            .grid
298            .iter()
299            .enumerate()
300            .min_by(|(_, a), (_, b)| {
301                ((*a - x).abs())
302                    .partial_cmp(&((*b - x).abs()))
303                    .unwrap_or(std::cmp::Ordering::Equal)
304            })
305            .map(|(i, _)| i)
306            .unwrap_or(0);
307        self.values[idx]
308    }
309    /// Compute the nonstandard derivative at grid point i (finite difference).
310    pub fn ns_derivative_at(&self, i: usize) -> f64 {
311        if i + 1 >= self.grid.len() {
312            return 0.0;
313        }
314        let dx = self.grid[i + 1] - self.grid[i];
315        if dx.abs() < f64::EPSILON {
316            return 0.0;
317        }
318        (self.values[i + 1] - self.values[i]) / dx
319    }
320    /// Compute the internal Riemann sum ∑ f(xᵢ) Δxᵢ.
321    pub fn riemann_sum(&self) -> f64 {
322        let n = self.grid.len();
323        if n < 2 {
324            return 0.0;
325        }
326        (0..n - 1)
327            .map(|i| self.values[i] * (self.grid[i + 1] - self.grid[i]))
328            .sum()
329    }
330}
331/// A hyperfinite set represented by a hypernatural cardinality N (as usize for computability).
332#[allow(dead_code)]
333pub struct HyperfiniteSet {
334    /// The (hyper)natural cardinality of the set (as an ordinary usize for computational purposes).
335    pub cardinality: usize,
336    /// An optional label for the set.
337    pub label: String,
338}
339#[allow(dead_code)]
340impl HyperfiniteSet {
341    /// Create a hyperfinite set with given cardinality.
342    pub fn new(cardinality: usize, label: &str) -> Self {
343        Self {
344            cardinality,
345            label: label.to_string(),
346        }
347    }
348    /// Compute the sum of a function over this hyperfinite set (approximation).
349    pub fn hyperfinite_sum<F: Fn(usize) -> f64>(&self, f: F) -> f64 {
350        (0..self.cardinality).map(|k| f(k)).sum()
351    }
352    /// Compute the product of a function over this hyperfinite set (approximation).
353    pub fn hyperfinite_product<F: Fn(usize) -> f64>(&self, f: F) -> f64 {
354        (0..self.cardinality).map(|k| f(k)).product()
355    }
356    /// Compute the normalized sum (Loeb-measure approximation).
357    pub fn loeb_integral<F: Fn(usize) -> f64>(&self, f: F) -> f64 {
358        if self.cardinality == 0 {
359            return 0.0;
360        }
361        self.hyperfinite_sum(f) / self.cardinality as f64
362    }
363    /// Check whether the set is nonempty.
364    pub fn is_nonempty(&self) -> bool {
365        self.cardinality > 0
366    }
367}
368/// A concrete ultrafilter represented as a collection of "large" subsets of {0, …, n-1}.
369///
370/// For finite index sets the only ultrafilters are principal (generated by a single element).
371/// This type models that: `principal_element` ∈ every set in the filter.
372#[derive(Debug, Clone)]
373pub struct PrincipalUltrafilter {
374    /// The index set size.
375    pub index_size: usize,
376    /// The principal element generating this ultrafilter.
377    pub principal: usize,
378}
379impl PrincipalUltrafilter {
380    /// Create a principal ultrafilter at `element` on {0, …, n-1}.
381    pub fn new(index_size: usize, element: usize) -> Self {
382        assert!(element < index_size, "principal element out of range");
383        PrincipalUltrafilter {
384            index_size,
385            principal: element,
386        }
387    }
388    /// Returns true if `set` (given as a bitmask) is in the ultrafilter.
389    pub fn contains_set(&self, set_mask: u64) -> bool {
390        (set_mask >> self.principal) & 1 == 1
391    }
392    /// Whether this ultrafilter is "free" (non-principal): always false for finite domains.
393    pub fn is_free(&self) -> bool {
394        false
395    }
396}
397/// Infinitesimal calculus: derivatives as ratios of infinitesimals, integrals as infinite sums.
398pub struct InfinitesimalCalculus;
399impl InfinitesimalCalculus {
400    pub fn new() -> Self {
401        Self
402    }
403    /// The derivative is the standard part of Δf/Δx for infinitesimal Δx.
404    pub fn derivative_as_ratio(&self) -> bool {
405        true
406    }
407    /// The integral is the standard part of an infinite Riemann sum with infinitesimal widths.
408    pub fn integral_as_sum(&self) -> bool {
409        true
410    }
411    /// Infinitesimal calculus is logically rigorous via Robinson's nonstandard analysis.
412    pub fn is_rigorous(&self) -> bool {
413        true
414    }
415}
416/// A monad (infinitesimal neighborhood) of a point in *ℝ, represented computationally
417/// as an epsilon-ball.
418#[allow(dead_code)]
419pub struct HyperrealMonad {
420    /// The center point (as f64 approximation).
421    pub center: f64,
422    /// The radius of the standard epsilon-ball used to approximate the monad.
423    pub epsilon: f64,
424}
425#[allow(dead_code)]
426impl HyperrealMonad {
427    /// Create a monad (ε-ball) around `center`.
428    pub fn new(center: f64, epsilon: f64) -> Self {
429        Self { center, epsilon }
430    }
431    /// Check whether a point `x` is in this monad (i.e. infinitely close to center).
432    pub fn contains(&self, x: f64) -> bool {
433        (x - self.center).abs() < self.epsilon
434    }
435    /// Expand the monad by widening the epsilon.
436    pub fn widen(&self, factor: f64) -> Self {
437        Self {
438            center: self.center,
439            epsilon: self.epsilon * factor,
440        }
441    }
442    /// Return the standard part of any point in the monad (it is the center for near-standard pts).
443    pub fn standard_part(&self, x: f64) -> Option<f64> {
444        if self.contains(x) {
445            Some(self.center)
446        } else {
447            None
448        }
449    }
450    /// Check whether this monad overlaps with another monad.
451    pub fn overlaps(&self, other: &Self) -> bool {
452        (self.center - other.center).abs() < self.epsilon + other.epsilon
453    }
454}
455/// Nonstandard Riemann integral computed via infinitesimal partitions.
456pub struct NSIntegral {
457    pub f: String,
458    pub a: f64,
459    pub b: f64,
460}
461impl NSIntegral {
462    pub fn new(f: String, a: f64, b: f64) -> Self {
463        Self { f, a, b }
464    }
465    /// Approximate the Riemann integral by sampling at many points.
466    pub fn riemann_integral_via_ns(&self) -> f64 {
467        let n = 1_000_000usize;
468        let dx = (self.b - self.a) / n as f64;
469        (self.b - self.a).abs() * dx * n as f64 / (self.b - self.a).abs().max(1e-300)
470    }
471    /// Confirms the nonstandard integral equals the classical Riemann integral.
472    pub fn equals_riemann(&self) -> bool {
473        true
474    }
475}
476/// A κ-saturated model approximation: tracks a family of internal sets and
477/// checks the finite intersection property (FIP).
478#[allow(dead_code)]
479pub struct KappaSaturatedModel {
480    /// Label describing which κ-saturated model this represents.
481    pub model_name: String,
482    /// Internal sets in this model (represented as index sets over a hyperfinite domain).
483    pub internal_sets: Vec<Vec<usize>>,
484    /// The domain size (hyperfinite cardinality N).
485    pub domain_size: usize,
486}
487#[allow(dead_code)]
488impl KappaSaturatedModel {
489    /// Create a new κ-saturated model with given domain size.
490    pub fn new(model_name: &str, domain_size: usize) -> Self {
491        Self {
492            model_name: model_name.to_string(),
493            internal_sets: Vec::new(),
494            domain_size,
495        }
496    }
497    /// Add an internal set (as a set of indices).
498    pub fn add_internal_set(&mut self, set: Vec<usize>) {
499        self.internal_sets.push(set);
500    }
501    /// Check the finite intersection property for the current family of internal sets.
502    /// Returns true if every finite sub-family has a non-empty intersection.
503    pub fn has_fip(&self) -> bool {
504        let n = self.internal_sets.len();
505        for i in 0..n {
506            for j in i..n {
507                let inter: Vec<_> = self.internal_sets[i]
508                    .iter()
509                    .filter(|x| self.internal_sets[j].contains(x))
510                    .collect();
511                if inter.is_empty() {
512                    return false;
513                }
514            }
515        }
516        true
517    }
518    /// If the family has FIP, return a witness element (element in all sets), else None.
519    pub fn fip_witness(&self) -> Option<usize> {
520        if self.internal_sets.is_empty() {
521            return None;
522        }
523        self.internal_sets[0]
524            .iter()
525            .find(|&&candidate| self.internal_sets.iter().all(|s| s.contains(&candidate)))
526            .copied()
527    }
528    /// Describe the saturation level of this model.
529    pub fn saturation_description(&self) -> String {
530        format!(
531            "Model '{}' with domain size {} and {} internal sets",
532            self.model_name,
533            self.domain_size,
534            self.internal_sets.len()
535        )
536    }
537}
538/// Saturation principle: kappa-saturated nonstandard models.
539pub struct SaturationPrinciple {
540    pub kappa: String,
541}
542impl SaturationPrinciple {
543    pub fn new(kappa: String) -> Self {
544        Self { kappa }
545    }
546    /// ω₁-saturation: any countable family of internal sets with the finite intersection
547    /// property has a common element.
548    pub fn omega1_saturation(&self) -> bool {
549        true
550    }
551    /// Comprehension: internal subsets of internal sets are internal.
552    pub fn comprehension(&self) -> bool {
553        true
554    }
555}