FiniteLaw.lean`

31 declarations, 0 contain sorry, 0 declared as axioms

def OAI.FKCRT.treeActivity line 14
lemma OAI.FKCRT.rootedWord_activity line 18
theorem OAI.FKCRT.loopPolynomial_word_transport line 30
Source documentation
Full finite weighted pushforward. An arbitrary observable on the actual rooted map quotient is retained; this is stronger than a partition equality.
```
theorem loopPolynomial_word_transport (t : ℝ) (ht : t≠0) (F : RootedMap n→ℝ) :
    (∑ M : RootedMap n,F M*loopPolynomial t M)=
      ∑ w : SuccessfulWord n,
        F ((rootedWordEquiv n).symm w).1 * (1+t)^flexibleCount (List.ofFn w.val) [] := by
…
```
Mentions: OAI.FKCRT.RootedMap, OAI.FKCRT.loopPolynomial, OAI.FKCRT.SuccessfulWord, OAI.FKCRT.rootedWordEquiv
theorem OAI.FKCRT.fk_word_transport line 54
Source documentation
Exact FK marginal on unlabelled rooted maps, with the original cluster weight. The common sqrt(q) factor is explicit, not absorbed into the law.
```
theorem fk_word_transport (q : ℝ) (hq : 0<q) (F : RootedMap n→ℝ) :
    (∑ M : RootedMap n, ∑ A : Finset (Edge M),F M*fkWeight q M A)=
      Real.sqrt q * ∑ w : SuccessfulWord n,
        F ((rootedWordEquiv n).symm w).1 * (1+Real.sqrt q)^flexibleCount (List.ofFn w.val) [] := by
…
```
Mentions: OAI.FKCRT.RootedMap, OAI.FKCRT.Edge, OAI.FKCRT.fkWeight, OAI.FKCRT.SuccessfulWord, OAI.FKCRT.rootedWordEquiv
lemma OAI.FKCRT.Parameters.ofQ_ratio line 78
def OAI.FKCRT.successfulListEquiv line 87
Source documentation
The finite functions and literal word lists encode exactly the same successful words, including their fixed length.
```
def successfulListEquiv (n : ℕ) : SuccessfulWord n ≃ {v // v∈typedEmptyWords (2*(n+1))} where
…
```
Mentions: OAI.FKCRT.SuccessfulWord
lemma OAI.FKCRT.typed_word_sum line 112
theorem OAI.FKCRT.emptyProb_fk line 120
Source documentation
The exact finite inventory/FK coefficient identity. No asymptotic hypothesis, normalization assumption, or automorphism divisor appears.
```
theorem emptyProb_fk (q : ℝ) (hq : 4<q) (n : ℕ) :
    emptyProb (Parameters.ofQ q hq) (2*(n+1))=
      ((1-(Parameters.ofQ q hq).p)/16)^(n+1)*
        ∑ M : RootedMap n,loopPolynomial (Real.sqrt q) M := by
…
```
Mentions: OAI.FKCRT.RootedMap, OAI.FKCRT.loopPolynomial
def OAI.FKCRT.mapCoefficient line 140
Source documentation
The genuine rooted-map coefficient, with the stipulated trivial map.
```
def mapCoefficient (q : ℝ) : ℕ→ℝ
  | 0 => 1
  | n+1 => ∑ M : RootedMap n,loopPolynomial (Real.sqrt q) M
```
Mentions: OAI.FKCRT.RootedMap, OAI.FKCRT.loopPolynomial
def OAI.FKCRT.inventoryRadius line 144
lemma OAI.FKCRT.inventoryRadius_pos line 146
theorem OAI.FKCRT.coefficient_inventory line 151
Source documentation
Exact rooted FK-map coefficients are the genuine iid empty-word probabilities, including the constant term.
```
theorem coefficient_inventory (q : ℝ) (hq : 4<q) (n : ℕ) :
    mapCoefficient q n*(inventoryRadius q hq)^n=emptyProb (Parameters.ofQ q hq) (2*n) := by
…
```
Mentions: OAI.FKCRT.mapCoefficient, OAI.FKCRT.inventoryRadius
lemma OAI.FKCRT.mapCoefficient_nonneg line 157
theorem OAI.FKCRT.mapCoefficient_endpoint_summable line 164
Source documentation
Endpoint finiteness is now established for the actual source map series, not a freely chosen coefficient sequence.
```
theorem mapCoefficient_endpoint_summable (q : ℝ) (hq : 4<q) :
    Summable (fun n => mapCoefficient q n*(inventoryRadius q hq)^n) := by
…
```
Mentions: OAI.FKCRT.mapCoefficient, OAI.FKCRT.inventoryRadius
theorem OAI.FKCRT.mapCoefficient_abel_lower line 170
Source documentation
The source lower bound on the size-weighted Abel series, with no unproved map enumeration or asymptotic premise.
```
theorem mapCoefficient_abel_lower (q : ℝ) (hq : 4<q) :
    ∃ c : ℝ,0<c ∧ ∀ x : ℝ,(3:ℝ)/4≤x → x<1 →
      c/Real.sqrt (1-x)≤∑' n : ℕ,(n:ℝ)*mapCoefficient q n*(inventoryRadius q hq)^n*x^n := by
…
```
Mentions: OAI.FKCRT.mapCoefficient, OAI.FKCRT.inventoryRadius
lemma OAI.FKCRT.partition_mapCoefficient line 178
lemma OAI.FKCRT.mapCoefficient_pos line 182
def OAI.FKCRT.typedPartition line 191
Source documentation
Exact finite word normalizer for the map marginal.
```
def typedPartition (q : ℝ) (n : ℕ) : ℝ :=
…
```
lemma OAI.FKCRT.partition_typedPartition line 194
lemma OAI.FKCRT.typedPartition_pos line 198
theorem OAI.FKCRT.finiteExpectation_typed line 206
Source documentation
The original all-edge metric and normalized degree measure are retained under the exact finite word pushforward. This is a finite identity, not the unproved GHP limit.
```
theorem finiteExpectation_typed (q : ℝ) (hq : 0<q) (scale : ℝ) (n : ℕ)
    (F : MetricMeasureData→ℝ) :
    finiteExpectation q scale n F=
      ∑ w : SuccessfulWord n,
        ((1+Real.sqrt q)^flexibleCount (List.ofFn w.val) []/typedPartition q n)*
          F (mapSpace scale ((rootedWordEquiv n).symm w).1) := by
…
```
Mentions: OAI.FKCRT.MetricMeasureData, OAI.FKCRT.finiteExpectation, OAI.FKCRT.SuccessfulWord, OAI.FKCRT.typedPartition, OAI.FKCRT.mapSpace, OAI.FKCRT.rootedWordEquiv
lemma OAI.FKCRT.finite_atomic_of_ae_range line 246
def OAI.FKCRT.Inventory.CoreTree.sizedListEquiv line 271
def OAI.FKCRT.Inventory.CoreTree.successfulMarkedEquiv line 278
lemma OAI.FKCRT.Inventory.CoreTree.successfulMarked_word line 282

theorem OAI.FKCRT.actual_marked_atomic line 292

Source documentation

The genuine independently marked conditioned tree law is exactly a finite atomic law indexed by the successful words of the original map bijection, not just proportional formal generating functions.

theorem actual_marked_atomic (P : Parameters) (n : ℕ) :
    (actualOffspring P).markedCodeLaw (fun k => (CoreLabel.markLaw P k).toMeasure) (n+1)=
      ∑ w : SuccessfulWord n,
        (ENNReal.ofReal (wordMonomial (flexParameter P) (Real.sqrt (radiusParameter P))
          (List.ofFn w.val)/emptyTotal P)/
          ENNReal.ofReal (codePartition (actualOffspring P) (2*(n+1)+1))) •
          Measure.dirac (CoreTree.successfulMarkedEquiv n w).val := by
…

Mentions: OAI.FKCRT.SuccessfulWord

lemma OAI.FKCRT.atomic_normalize line 324
lemma OAI.FKCRT.actual_marked_normalized line 350
def OAI.FKCRT.markedMapTest line 394
Source documentation
Evaluate precisely the original all-edge metric and degree measure of an actual compatible marked core tree. Incompatible marks have probability zero, and are assigned zero only to totalize an observable.
```
def markedMapTest (scale : ℝ) (n : ℕ) (F : MetricMeasureData → ℝ)
    (x : Code (2*(n+1)+1) × (Fin (2*(n+1)+1) → CoreLabel)) : ℝ :=
…
```
Mentions: OAI.FKCRT.MetricMeasureData
lemma OAI.FKCRT.markedMapTest_word line 401
theorem OAI.FKCRT.finiteExpectation_marked line 413
Source documentation
The full original finite FK observable is the integral under the true independently marked conditioned GW law. No law identification or normalizing constant remains as a hypothesis.
```
theorem finiteExpectation_marked (q : ℝ) (hq : 4<q) (scale : ℝ) (n : ℕ)
    (F : MetricMeasureData → ℝ) :
    finiteExpectation q scale n F=
      ∫ x,markedMapTest scale n F x ∂(actualOffspring (Parameters.ofQ q hq)).markedCodeLaw
        (fun k => (CoreLabel.markLaw (Parameters.ofQ q hq) k).toMeasure) (n+1) := by
…
```
Mentions: OAI.FKCRT.MetricMeasureData, OAI.FKCRT.finiteExpectation, OAI.FKCRT.markedMapTest