Potential.lean`

58 declarations, 0 contain sorry, 0 declared as axioms

Profile paths and the no-expanding-neutral-leaf dependency.

theorem OAI.PureTypeSystem.Profile.nonempty_of_sorted line 13
theorem OAI.PureTypeSystem.Profile.context_head_conversion line 17
theorem OAI.PureTypeSystem.Profile.inclusion_path line 24
theorem OAI.PureTypeSystem.Profile.triple line 31
theorem OAI.PureTypeSystem.Profile.instantiate_product_path line 54
Source documentation
The exact positive ascent from an instantiated codomain to its product. It uses all sortings rather than choosing a functional specification.
```
theorem instantiate_product_path (hw : SystemWeaklyNormalizing P)
    {D E n : Expr S} {s : S} (h : HasType P Γ (.pi D E) (.sort s))
    (hn : HasType P Γ n D) :
    PositivePath (PrimaryEdge P) (Profile P Γ (E.instantiate n))
      (Profile P Γ (.pi D E)) := by
…
```
Mentions: OAI.PureTypeSystem.SystemWeaklyNormalizing, OAI.PureTypeSystem.Expr, OAI.PureTypeSystem.HasType, OAI.PureTypeSystem.Profile.pi, OAI.PureTypeSystem.Profile.sort, OAI.PureTypeSystem.PositivePath, OAI.PureTypeSystem.PrimaryEdge, OAI.PureTypeSystem.Profile
def OAI.PureTypeSystem.Expr.head line 70
theorem OAI.PureTypeSystem.Expr.head_apps line 73
theorem OAI.PureTypeSystem.HasType.neutral_profile_ascent line 84
Source documentation
Reading a neutral spine backwards gives a positive path from the exact result-type profile to the declaration-type profile of its head.
```
theorem neutral_profile_ascent (hw : SystemWeaklyNormalizing P)
    {M T : Expr S} (hn : Neutral M) (h : HasType P Γ M T) :
    ∃ n D, M.head = .var n ∧ Lookup Γ n D ∧
      PositivePath (PrimaryEdge P) (Profile P Γ T) (Profile P Γ D) := by
…
```
Mentions: OAI.PureTypeSystem.SystemWeaklyNormalizing, OAI.PureTypeSystem.Expr, OAI.PureTypeSystem.Neutral, OAI.PureTypeSystem.HasType, OAI.PureTypeSystem.Lookup, OAI.PureTypeSystem.PositivePath, OAI.PureTypeSystem.PrimaryEdge, OAI.PureTypeSystem.Profile
theorem OAI.PureTypeSystem.HasType.neutral_profile_seed line 106
Source documentation
This is the precise seed generated when a normal neutral type can be changed at its head by substitution. The sort axiom is derived, not assumed.
```
theorem neutral_profile_seed (hw : SystemWeaklyNormalizing P)
    {M : Expr S} {s : S} (hn : Neutral M) (hM : Normal M)
    (h : HasType P Γ M (.sort s)) :
    Profile P Γ M = {s} ∧ (AxProfile P s).Nonempty ∧
      ∃ n D, M.head = .var n ∧ Lookup Γ n D ∧
        PositivePath (PrimaryEdge P) (AxProfile P s) (Profile P Γ D) := by
…
```
Mentions: OAI.PureTypeSystem.SystemWeaklyNormalizing, OAI.PureTypeSystem.Expr, OAI.PureTypeSystem.Neutral, OAI.PureTypeSystem.Normal, OAI.PureTypeSystem.HasType, OAI.PureTypeSystem.Profile, OAI.PureTypeSystem.AxProfile, OAI.PureTypeSystem.Lookup, OAI.PureTypeSystem.PositivePath, OAI.PureTypeSystem.PrimaryEdge
theorem OAI.PureTypeSystem.Neutral.rename line 119
theorem OAI.PureTypeSystem.Neutral.subst_of_head line 124
theorem OAI.PureTypeSystem.Neutral.beta line 130
theorem OAI.PureTypeSystem.Neutral.reduces line 139
theorem OAI.PureTypeSystem.Neutral.normalForm line 144
theorem OAI.PureTypeSystem.Profile.rename_normal line 153
theorem OAI.PureTypeSystem.Profile.rename line 189
theorem OAI.PureTypeSystem.Profile.weaken line 197
def OAI.PureTypeSystem.SingleSource line 208
Source documentation
Every image which can replace a neutral head originates at the chosen outer binder profile. Ordinary one-variable substitution, and every lifting of it through additional binders, have this property.
```
def SingleSource {S : Type u} (P : Specification S) (Γ : List (Expr S))
    (σ : Nat → Expr S) (I : Set S) : Prop :=
…
```
Mentions: OAI.PureTypeSystem.Specification, OAI.PureTypeSystem.Expr
theorem OAI.PureTypeSystem.SingleSource.single line 216
theorem OAI.PureTypeSystem.SingleSource.lift line 224
theorem OAI.PureTypeSystem.ForbiddenConfiguration.of_neutral_expansion line 242
Source documentation
The source's critical neutral-leaf argument. No beta-normal neutral leaf in this component can become a product under substitution of the outer binder: doing so would produce exactly the excluded graph configuration.
```
theorem of_neutral_expansion (hw : SystemWeaklyNormalizing P)
    (hD : IsComponent (SecondaryEdge P C) D) (hplain : ∀ I ∈ D, PlainLayer P C I)
    (hneg : ∃ I ∈ D, ∃ K ∈ D, SecondaryEdge P C I K true)
    {I J K : Set S} (htr : ProfileTriple P I J K) (hJ : J ∈ D) (hK : K ∈ D)
    {Γ Δ : List (Expr S)} (hΔ : ValidContext P Δ) {σ : Nat → Expr S}
    (hσ : TypedSubstitution P Γ Δ σ) (hsrc : SingleSource P Γ σ I)
    {M A B : Expr S} {s : S} (h : HasType P Γ M (.sort s))
    (hn : Normal M) (hne : Neutral M) (hM : Profile P Γ M ∈ D)
    (he : (M.subst σ).normalForm = .pi A B) : ForbiddenConfiguration P C := by
…
```
Mentions: OAI.PureTypeSystem.SystemWeaklyNormalizing, OAI.PureTypeSystem.IsComponent, OAI.PureTypeSystem.SecondaryEdge, OAI.PureTypeSystem.PlainLayer, OAI.PureTypeSystem.ProfileTriple, OAI.PureTypeSystem.Expr, OAI.PureTypeSystem.ValidContext, OAI.PureTypeSystem.TypedSubstitution, OAI.PureTypeSystem.SingleSource, OAI.PureTypeSystem.HasType, OAI.PureTypeSystem.Normal, OAI.PureTypeSystem.Neutral, OAI.PureTypeSystem.Profile, OAI.PureTypeSystem.ForbiddenConfiguration
theorem OAI.PureTypeSystem.ObservationLayers.positive line 268
theorem OAI.PureTypeSystem.ObservationLayers.secondary line 273
theorem OAI.PureTypeSystem.ActiveLayer.layer line 284
theorem OAI.PureTypeSystem.ActiveLayer.predecessor line 292
theorem OAI.PureTypeSystem.IsComponent.codomain_interpolation line 303
Source documentation
Interpolation of a counted post-substitution codomain through the original product triple.
```
theorem codomain_interpolation (hD : IsComponent (SecondaryEdge P C) D)
    (hl : ∀ X ∈ D, X ∈ ObservationLayers P C)
    {I J K J' : Set S} (htr : ProfileTriple P I J K) (hK : K ∈ D) (hJ' : J' ∈ D)
    (hJJ' : PositivePath (PrimaryEdge P) J' J) : J ∈ D := by
…
```
Mentions: OAI.PureTypeSystem.IsComponent, OAI.PureTypeSystem.SecondaryEdge, OAI.PureTypeSystem.ObservationLayers, OAI.PureTypeSystem.ProfileTriple, OAI.PureTypeSystem.PositivePath, OAI.PureTypeSystem.PrimaryEdge
theorem OAI.PureTypeSystem.IsComponent.domain_interpolation line 314
Source documentation
Domain interpolation also needs the post open codomain to be active; this is exactly the side condition in the source potential, not a stronger assumption that every domain dependency is retained.
```
theorem domain_interpolation (hD : IsComponent (SecondaryEdge P C) D)
    (hl : ∀ X ∈ D, X ∈ ObservationLayers P C)
    (ha : ∀ X ∈ D, ActiveLayer P C X)
    {I J K I' J' : Set S} (htr : ProfileTriple P I J K) (hK : K ∈ D)
    (hI' : I' ∈ D) (hJ' : ActiveLayer P C J')
    (hII' : PositivePath (PrimaryEdge P) I' I)
    (hJJ' : PositivePath (PrimaryEdge P) J' J) :
    I ∈ D ∧ ActiveLayer P C J := by
…
```
Mentions: OAI.PureTypeSystem.IsComponent, OAI.PureTypeSystem.SecondaryEdge, OAI.PureTypeSystem.ObservationLayers, OAI.PureTypeSystem.ActiveLayer, OAI.PureTypeSystem.ProfileTriple, OAI.PureTypeSystem.PositivePath, OAI.PureTypeSystem.PrimaryEdge
theorem OAI.PureTypeSystem.Profile.growth_path line 332
structure OAI.PureTypeSystem.ContextEquivalent line 345
Source documentation
Context conversion as exact equality of all judgments on unchanged syntax. Both contexts are required valid. This auxiliary relation carries no semantic or normalization assumption.
```
structure ContextEquivalent {S : Type u} (P : Specification S)
    (Γ Δ : List (Expr S)) : Prop where
…
```
Mentions: OAI.PureTypeSystem.Specification, OAI.PureTypeSystem.Expr
theorem OAI.PureTypeSystem.ContextEquivalent.symm line 353
theorem OAI.PureTypeSystem.ContextEquivalent.profile line 356
theorem OAI.PureTypeSystem.ContextEquivalent.cons line 361
theorem OAI.PureTypeSystem.ContextEquivalent.head_conversion line 379

def OAI.PureTypeSystem.PlainObservations.potential line 392

Source documentation

The exact source syntax-tree potential. Its recursive child conditions retain the active-open-codomain guard on a counted domain.

noncomputable def potential (P : Specification S) (C D : Set (Set S))
    (Γ : List (Expr S)) : Expr S → Nat
  | .pi A B => by
      classical
      exact 1 +
      (if Profile P Γ A ∈ D ∧ ActiveLayer P C (Profile P (A :: Γ) B)
       then potential P C D Γ A else 0) +
      (if Profile P (A :: Γ) B ∈ D then potential P C D (A :: Γ) B else 0)
  | _ => 1

variable {P : Specification S} {C D : Set (Set S)}

Mentions: OAI.PureTypeSystem.Specification, OAI.PureTypeSystem.Expr, OAI.PureTypeSystem.Profile, OAI.PureTypeSystem.ActiveLayer

theorem OAI.PureTypeSystem.PlainObservations.potential_context line 404
theorem OAI.PureTypeSystem.PlainObservations.potential_normalized_pi line 417
Source documentation
Normalizing a product does not change the contexts in which its child contributions are measured: raw and normalized annotations are context convertible. This keeps the dependent codomain count honest.
```
theorem potential_normalized_pi (hw : SystemWeaklyNormalizing P)
    {Γ : List (Expr S)} {A B : Expr S} {s : S}
    (h : HasType P Γ (.pi A B) (.sort s)) :
    potential P C D Γ (Expr.pi A B).normalForm = 1 +
      (if Profile P Γ A ∈ D ∧ ActiveLayer P C (Profile P (A :: Γ) B)
       then potential P C D Γ A.normalForm else 0) +
      (if Profile P (A :: Γ) B ∈ D then potential P C D (A :: Γ) B.normalForm else 0) := by
…
```
Mentions: OAI.PureTypeSystem.SystemWeaklyNormalizing, OAI.PureTypeSystem.Expr, OAI.PureTypeSystem.HasType, OAI.PureTypeSystem.PlainObservations.potential, OAI.PureTypeSystem.Profile, OAI.PureTypeSystem.ActiveLayer
theorem OAI.PureTypeSystem.PlainObservations.potential_subst_le line 436
Source documentation
The full potential inequality. The outer triple and its codomain/product vertices are fixed exactly as in the source legal-frame argument. SingleSource is proved above for the actual one-variable substitution and all binder lifts.
```
theorem potential_subst_le (hw : SystemWeaklyNormalizing P)
    (hno : ¬ ForbiddenConfiguration P C)
    (hD : IsComponent (SecondaryEdge P C) D) (hplain : ∀ I ∈ D, PlainLayer P C I)
    (hneg : ∃ I ∈ D, ∃ K ∈ D, SecondaryEdge P C I K true)
    {I J K : Set S} (htr : ProfileTriple P I J K) (hJ : J ∈ D) (hK : K ∈ D)
    {Γ Δ : List (Expr S)} (hΔ : ValidContext P Δ) {σ : Nat → Expr S}
    (hσ : TypedSubstitution P Γ Δ σ) (hsrc : SingleSource P Γ σ I)
    {T : Expr S} {s : S} (hT : HasType P Γ T (.sort s)) (hn : Normal T)
    (hTC : Profile P Γ T ∈ D) :
    potential P C D Δ (T.subst σ).normalForm ≤ potential P C D Γ T := by
…
```
Mentions: OAI.PureTypeSystem.SystemWeaklyNormalizing, OAI.PureTypeSystem.ForbiddenConfiguration, OAI.PureTypeSystem.IsComponent, OAI.PureTypeSystem.SecondaryEdge, OAI.PureTypeSystem.PlainLayer, OAI.PureTypeSystem.ProfileTriple, OAI.PureTypeSystem.Expr, OAI.PureTypeSystem.ValidContext, OAI.PureTypeSystem.TypedSubstitution, OAI.PureTypeSystem.SingleSource, OAI.PureTypeSystem.HasType, OAI.PureTypeSystem.Normal, OAI.PureTypeSystem.Profile, OAI.PureTypeSystem.PlainObservations.potential
theorem OAI.PureTypeSystem.PlainObservations.potential_pos line 494

theorem OAI.PureTypeSystem.PlainObservations.frame_potential_drop line 499

Source documentation

Exact legal-frame potential drop in the negative plain component, including the strict syntactic-child inequality.

theorem frame_potential_drop (hw : SystemWeaklyNormalizing P)
    (hno : ¬ ForbiddenConfiguration P C)
    (hD : IsComponent (SecondaryEdge P C) D) (hplain : ∀ I ∈ D, PlainLayer P C I)
    (hneg : ∃ I ∈ D, ∃ K ∈ D, SecondaryEdge P C I K true)
    {Γ : List (Expr S)} {A B n : Expr S} {s : S}
    (hT : HasType P Γ (.pi A B) (.sort s)) (hnT : Normal (.pi A B))
    (hn : HasType P Γ n A) (hK : Profile P Γ (.pi A B) ∈ D)
    (hL : Profile P Γ (B.instantiate n) ∈ D) :
    potential P C D Γ (B.instantiate n).normalForm ≤ potential P C D (A :: Γ) B ∧
      potential P C D (A :: Γ) B < potential P C D Γ (.pi A B) := by
…

Mentions: OAI.PureTypeSystem.SystemWeaklyNormalizing, OAI.PureTypeSystem.ForbiddenConfiguration, OAI.PureTypeSystem.IsComponent, OAI.PureTypeSystem.SecondaryEdge, OAI.PureTypeSystem.PlainLayer, OAI.PureTypeSystem.Expr, OAI.PureTypeSystem.HasType, OAI.PureTypeSystem.Normal, OAI.PureTypeSystem.Profile, OAI.PureTypeSystem.PlainObservations.potential

theorem OAI.PureTypeSystem.PlainObservations.frame_domain_drop line 520
theorem OAI.PureTypeSystem.PlainObservations.potential_rename line 531
Source documentation
The potential counts positions, so valid thinning does not change it. The equality is exact also under every dependent binder.
```
theorem potential_rename (hw : SystemWeaklyNormalizing P)
    {Γ Δ : List (Expr S)} {T : Expr S} {s : S}
    (hT : HasType P Γ T (.sort s)) (hΔ : ValidContext P Δ) (ρ : Nat → Nat)
    (hρ : ∀ n B, Lookup Γ n B → HasType P Δ (.var (ρ n)) (B.rename ρ)) :
    potential P C D Δ (T.rename ρ) = potential P C D Γ T := by
…
```
Mentions: OAI.PureTypeSystem.SystemWeaklyNormalizing, OAI.PureTypeSystem.Expr, OAI.PureTypeSystem.HasType, OAI.PureTypeSystem.ValidContext, OAI.PureTypeSystem.Lookup, OAI.PureTypeSystem.PlainObservations.potential
def OAI.PureTypeSystem.ContextTower.profile line 565
Source documentation
The source profile on syntax with fixed global variable names.
```
def profile (T : Expr S) : Set S := {s | Ω.HasType T.normalForm (.sort s)}
…
```
Mentions: OAI.PureTypeSystem.Expr
theorem OAI.PureTypeSystem.ContextTower.profile_at_next line 570
theorem OAI.PureTypeSystem.ContextTower.profile_at_mono line 581
theorem OAI.PureTypeSystem.ContextTower.profile_at line 592
Source documentation
A single available sorting fixes the exact profile at every later prefix. Extra sorting rules cannot appear merely by weakening.
```
theorem profile_at {n : Nat} {T : Expr S} {s : S}
    (ht : PureTypeSystem.HasType P (Ω.context n) (T.rename (Expr.reverseIndex n)) (.sort s)) :
    Ω.profile T = Profile P (Ω.context n) (T.rename (Expr.reverseIndex n)) := by
…
```
Mentions: OAI.PureTypeSystem.Expr, OAI.PureTypeSystem.HasType, OAI.PureTypeSystem.Expr.reverseIndex, OAI.PureTypeSystem.Profile
theorem OAI.PureTypeSystem.ContextTower.profile_normalForm line 612
theorem OAI.PureTypeSystem.ContextTower.profile_nonempty line 615
theorem OAI.PureTypeSystem.ContextTower.profile_feasible line 618
theorem OAI.PureTypeSystem.ContextTower.potential_at_next line 625
theorem OAI.PureTypeSystem.ContextTower.potential_at_mono line 637
def OAI.PureTypeSystem.ContextTower.potential line 647
theorem OAI.PureTypeSystem.ContextTower.potential_at line 652
theorem OAI.PureTypeSystem.ContextTower.frame_profiles line 665
Source documentation
Formation data for a global legal frame, retaining the open codomain profile instead of imposing functionality.
```
theorem frame_profiles {A B q : Expr S} {s : S}
    (hT : Ω.HasType (.pi A B) (.sort s)) (hq : Ω.HasType q A) :
    ∃ J, ProfileTriple P (Ω.profile A) J (Ω.profile (.pi A B)) ∧
      PositivePath (PrimaryEdge P) (Ω.profile (B.instantiate q)) J := by
…
```
Mentions: OAI.PureTypeSystem.Expr, OAI.PureTypeSystem.ProfileTriple, OAI.PureTypeSystem.PositivePath, OAI.PureTypeSystem.PrimaryEdge
theorem OAI.PureTypeSystem.ContextTower.domain_sorted line 689
theorem OAI.PureTypeSystem.ContextTower.frame_target_sorted line 696

theorem OAI.PureTypeSystem.ContextTower.frame_target_drop line 710

Source documentation

Global form of the source strict target-potential inequality.

theorem frame_target_drop {C D : Set (Set S)}
    (hno : ¬ ForbiddenConfiguration P C)
    (hD : IsComponent (SecondaryEdge P C) D) (hplain : ∀ I ∈ D, PlainLayer P C I)
    (hneg : ∃ I ∈ D, ∃ K ∈ D, SecondaryEdge P C I K true)
    {A B q : Expr S} {s : S} (hT : Ω.HasType (.pi A B) (.sort s))
    (hN : Normal (.pi A B)) (hq : Ω.HasType q A)
    (hK : Ω.profile (.pi A B) ∈ D) (hL : Ω.profile (B.instantiate q) ∈ D) :
    Ω.potential C D (B.instantiate q).normalForm < Ω.potential C D (.pi A B) := by
…

Mentions: OAI.PureTypeSystem.ForbiddenConfiguration, OAI.PureTypeSystem.IsComponent, OAI.PureTypeSystem.SecondaryEdge, OAI.PureTypeSystem.PlainLayer, OAI.PureTypeSystem.Expr, OAI.PureTypeSystem.Normal

theorem OAI.PureTypeSystem.ContextTower.frame_domain_drop line 739

Source documentation

Every active same-component domain is counted, even when a frame exits its component. This is why the potential's guard is activity, not membership of the open codomain in the component.

theorem frame_domain_drop {C D : Set (Set S)}
    {A B q : Expr S} {s : S} (hT : Ω.HasType (.pi A B) (.sort s)) (hq : Ω.HasType q A)
    (hK : ActiveLayer P C (Ω.profile (.pi A B)))
    (hL : ActiveLayer P C (Ω.profile (B.instantiate q)))
    (hI : Ω.profile A ∈ D) :
    Ω.potential C D A < Ω.potential C D (.pi A B) := by
…

Mentions: OAI.PureTypeSystem.Expr, OAI.PureTypeSystem.ActiveLayer

theorem OAI.PureTypeSystem.ContextTower.profile_subst_growth line 773
Source documentation
Substitution of a typed normal generic expression can only grow its exact profile. The common-stage reduction keeps nonfunctional sort choices.
```
theorem profile_subst_growth (hw : SystemWeaklyNormalizing P) {Γ : List (Expr S)}
    {T : Expr S} {s : S} {σ : Nat → Expr S} (ht : PureTypeSystem.HasType P Γ T (.sort s))
    (hσ : Ω.TypedSubstitution Γ σ) : Profile P Γ T ⊆ Ω.profile (T.subst σ) := by
…
```
Mentions: OAI.PureTypeSystem.SystemWeaklyNormalizing, OAI.PureTypeSystem.Expr, OAI.PureTypeSystem.HasType, OAI.PureTypeSystem.Profile