Model.lean`

34 declarations, 0 contain sorry, 0 declared as axioms

Finite Fortuin–Kasteleyn maps and the Brownian continuum random tree.

All combinatorial maps below have a distinguished dart 0 and are quotiented by orientation-preserving dart relabellings fixing that dart. A rotation system with Euler characteristic 2 encodes precisely a connected oriented-sphere map. No simplicity restriction is imposed. Vertices and edges are rotation and edge-reversal orbits, respectively. Every edge subset is included in the law. The index n here represents source size n+1, so the limit is through ALL positive edge sizes, not a subsequence.

MetricMeasureData packages the actual distance, measurable space and measure, without using arbitrary representatives of measure-preserving isometry classes as a global typeclass. Valid objects are compact metric probability spaces. The GHP extended distance is the infimum over common isometric embeddings, represented by pseudometrics on the disjoint union; zero cross distances simply identify points in the common ambient space. Tests are bounded functions continuous for that distance on valid objects. Thus GHP convergence is written in its bounded-continuous-test (weak distributional convergence) definition.

A standard normalized Brownian excursion is represented in its standard three-dimensional Bessel-bridge realization: the norm of three independent standard Brownian bridges of duration 1. No rescaling of the excursion is used.

abbrev OAI.FKCRT.Dart line 36
Also declared: ComparatorChallenges/FKCRT.lean:36 (same declaration text).
abbrev OAI.FKCRT.Orbit line 38
Also declared: ComparatorChallenges/FKCRT.lean:38 (same declaration text).
def OAI.FKCRT.orbit line 41
Also declared: ComparatorChallenges/FKCRT.lean:41 (same declaration text).
instance OAI.FKCRT.(instance at line 44) line 44
def OAI.FKCRT.spanningGraph line 49
Source documentation
The spanning graph with precisely the edges in A, with loops omitted only from adjacency: they still exist as edge orbits, have FK weight, and contribute two darts to the degree measure. Omitting loops does not change distance or k.
Also declared: ComparatorChallenges/FKCRT.lean:49 (same declaration text).
```
def spanningGraph {n : ℕ} (a s : Equiv.Perm (Dart n)) (A : Set (Orbit a)) :
    SimpleGraph (Orbit s) :=
…
```
Mentions: OAI.FKCRT.Dart, OAI.FKCRT.Orbit
def OAI.FKCRT.MapConditions line 55
Source documentation
Labelled connected orientable genus-zero rotation systems.
Also declared: ComparatorChallenges/FKCRT.lean:55 (same declaration text).
```
def MapConditions {n : ℕ} (P : Equiv.Perm (Dart n) × Equiv.Perm (Dart n)) : Prop :=
…
```
Mentions: OAI.FKCRT.Dart
abbrev OAI.FKCRT.LabelledMap line 60
Also declared: ComparatorChallenges/FKCRT.lean:60 (same declaration text).
def OAI.FKCRT.MapIso line 64
Source documentation
Root-preserving isomorphism of oriented maps (both dart permutations intertwine).
Also declared: ComparatorChallenges/FKCRT.lean:64 (same declaration text).
```
def MapIso {n : ℕ} (M N : LabelledMap n) : Prop :=
…
```
Mentions: OAI.FKCRT.LabelledMap
abbrev OAI.FKCRT.RootedMap line 69
Also declared: ComparatorChallenges/FKCRT.lean:69 (same declaration text).
instance OAI.FKCRT.(instance at line 71) line 71
def OAI.FKCRT.reversal line 73
Also declared: ComparatorChallenges/FKCRT.lean:73 (same declaration text).
def OAI.FKCRT.rotation line 75
Also declared: ComparatorChallenges/FKCRT.lean:75 (same declaration text).
abbrev OAI.FKCRT.Vertex line 77
Also declared: ComparatorChallenges/FKCRT.lean:77 (same declaration text).
abbrev OAI.FKCRT.Edge line 78
Also declared: ComparatorChallenges/FKCRT.lean:78 (same declaration text).
def OAI.FKCRT.graph line 80
Also declared: ComparatorChallenges/FKCRT.lean:80 (same declaration text).
def OAI.FKCRT.clusterCount line 84
Source documentation
The source k_M(A), including isolated vertices.
Also declared: ComparatorChallenges/FKCRT.lean:84 (same declaration text).
```
def clusterCount {n : ℕ} (M : RootedMap n) (A : Finset (Edge M)) : ℕ :=
…
```
Mentions: OAI.FKCRT.RootedMap, OAI.FKCRT.Edge
def OAI.FKCRT.fkWeight line 88
Source documentation
Exact decorated finite-map weight from eq:finite-law.
Also declared: ComparatorChallenges/FKCRT.lean:88 (same declaration text).
```
def fkWeight {n : ℕ} (q : ℝ) (M : RootedMap n) (A : Finset (Edge M)) : ℝ :=
…
```
Mentions: OAI.FKCRT.RootedMap, OAI.FKCRT.Edge
def OAI.FKCRT.partition line 92
Also declared: ComparatorChallenges/FKCRT.lean:92 (same declaration text).
structure OAI.FKCRT.MetricMeasureData line 96
Source documentation
Unbundled presentation of a measured metric space; validity is specified below.
Also declared: ComparatorChallenges/FKCRT.lean:96 (same declaration text).
```
structure MetricMeasureData where
…
```
def OAI.FKCRT.MetricMeasureData.Valid line 103
Source documentation
Exactly compact metric probability spaces, with their Borel sigma algebras.
Also declared: ComparatorChallenges/FKCRT.lean:103 (same declaration text).
```
def MetricMeasureData.Valid (X : MetricMeasureData) : Prop :=
…
```
Mentions: OAI.FKCRT.MetricMeasureData
def OAI.FKCRT.degreeMass line 111
Source documentation
Normalized degree measure is uniform dart mass pushed to vertices.
Also declared: ComparatorChallenges/FKCRT.lean:111 (same declaration text).
```
def degreeMass {n : ℕ} (M : RootedMap n) :
    @Measure (Vertex M) ⊤ :=
…
```
Mentions: OAI.FKCRT.RootedMap, OAI.FKCRT.Vertex
def OAI.FKCRT.mapSpace line 118
Source documentation
Root and decoration are not included in the metric probability space.
Also declared: ComparatorChallenges/FKCRT.lean:118 (same declaration text).
```
def mapSpace {n : ℕ} (scale : ℝ) (M : RootedMap n) : MetricMeasureData where
…
```
Mentions: OAI.FKCRT.RootedMap, OAI.FKCRT.MetricMeasureData
def OAI.FKCRT.Amalgamates line 125
Source documentation
An ambient pseudometric on the disjoint union giving isometric embeddings.
Also declared: ComparatorChallenges/FKCRT.lean:125 (same declaration text).
```
def Amalgamates (X Y : MetricMeasureData)
    (m : PseudoMetricSpace (X.Carrier ⊕ Y.Carrier)) : Prop :=
…
```
Mentions: OAI.FKCRT.MetricMeasureData
def OAI.FKCRT.ambientCost line 131
Also declared: ComparatorChallenges/FKCRT.lean:131 (same declaration text).
def OAI.FKCRT.ghpEDist line 144
Source documentation
The common-isometric-embedding definition of the source GHP distance.
Also declared: ComparatorChallenges/FKCRT.lean:144 (same declaration text).
```
def ghpEDist (X Y : MetricMeasureData) : ℝ≥0∞ :=
…
```
Mentions: OAI.FKCRT.MetricMeasureData
def OAI.FKCRT.IsGHPTest line 150
Source documentation
Bounded continuous tests on compact metric probability spaces modulo measure-preserving isometry, expressed on presentations.
Also declared: ComparatorChallenges/FKCRT.lean:150 (same declaration text).
```
def IsGHPTest (F : MetricMeasureData → ℝ) : Prop :=
…
```
Mentions: OAI.FKCRT.MetricMeasureData
def OAI.FKCRT.excursionDist line 156
Source documentation
Source excursion pseudometric, with the closed interval minimum.
Also declared: ComparatorChallenges/FKCRT.lean:156 (same declaration text).
```
def excursionDist (e : unitInterval → ℝ) (s t : unitInterval) : ℝ :=
…
```
abbrev OAI.FKCRT.ExcursionTree line 159
Also declared: ComparatorChallenges/FKCRT.lean:159 (same declaration text).
def OAI.FKCRT.treeProjection line 162
Also declared: ComparatorChallenges/FKCRT.lean:162 (same declaration text).
def OAI.FKCRT.treeSpace line 168
Source documentation
The quotient by d_e=0, its induced metric, and pushforward of uniform time. The equivalence closure is redundant for continuous e; the induced distance is independent of representatives, as required by the pseudometric proof.
Also declared: ComparatorChallenges/FKCRT.lean:168 (same declaration text).
```
def treeSpace (e : unitInterval → ℝ) : MetricMeasureData :=
…
```
Mentions: OAI.FKCRT.MetricMeasureData
def OAI.FKCRT.standardExcursion line 178
Source documentation
Standard normalized excursion, realized as the 3D Bessel bridge.
Also declared: ComparatorChallenges/FKCRT.lean:178 (same declaration text).
```
def standardExcursion {Ω : Type} (B : Fin 3 → ℝ≥0 → Ω → ℝ) (ω : Ω)
    (t : unitInterval) : ℝ :=
…
```
def OAI.FKCRT.finiteExpectation line 184
Source documentation
Exact expectation under the finite law, with n+1 edges.
Also declared: ComparatorChallenges/FKCRT.lean:184 (same declaration text).
```
def finiteExpectation (q scale : ℝ) (n : ℕ) (F : MetricMeasureData → ℝ) : ℝ :=
…
```
Mentions: OAI.FKCRT.MetricMeasureData
def OAI.FKCRT.brownianExpectation line 188
Also declared: ComparatorChallenges/FKCRT.lean:188 (same declaration text).
def OAI.FKCRT.MainStatement line 194
Source documentation
thm:main. The quantifiers over Brownian realizations express that the limit is the standard excursion-tree law, not a coupling-specific object.
Also declared: ComparatorChallenges/FKCRT.lean:194 (same declaration text).
```
def MainStatement : Prop :=
…
```