Documentation

LeanPool.PointwiseComposition.CategoricalRiceShapiro.Evaluator.PersistenceInduction

Supporting results for pointwise provable equality.

The conditional induction principle for certificate persistence #

For a standard index q, write C(s, q, u, y) for the raw evaluator certificate evalnCertificateFormula at ![s, q, u, y], and P_q(s) for โˆ€ t u y, s โ‰ค t โ†’ C(s, q, u, y) โ†’ C(t, q, u, y).

persistenceFormula q is an explicit arithmetic formula in one variable, and persistenceFormula_eval_iff proves that it defines P_q in every model of ๐ˆ๐Ž๐ฉ๐ž๐ง. models_inductionScheme_univ proves that a model of ๐๐€ satisfies the full induction scheme that ๐๐€ contains. certificate_persistence_of_stage_induction applies successor induction from that scheme to persistenceFormula q: from P_q(0) and โˆ€ s, P_q(s) โ†’ P_q(s + 1) it derives P_q(s) for every s.

The successor premise is a hypothesis of that theorem. The stage-zero premise is proved here, by evalnCertificateFormula_natCode_persist_of_stage_zero, for every standard index and independently of its constructor number: at stage 0 no evaluator history has a row, so the source certificate is refutable and the implication holds vacuously.

The file proves no conditional persistence case at a constructor number. The constructor-6 cases and the full tag-6 theorem are in Evaluator.PrimitiveRecursionPersistence; persistence for every standard index, which needs the external induction on the index, is not proved anywhere in the library.

source
def PointwiseComposition.CategoricalRiceShapiro.Evaluator.certificateSentence :
FFL.FirstOrder.ArithmeticSemisentence 4

The certificate formula as a plain four-place arithmetic semisentence.

Equations
Instances For
    source
    def PointwiseComposition.CategoricalRiceShapiro.Evaluator.persistenceFormula (q : โ„•) :
    FFL.FirstOrder.ArithmeticSemisentence 1

    The persistence predicate at the standard index q, as an arithmetic formula in the source stage: โˆ€ t u y, s โ‰ค t โ†’ C(s, q, u, y) โ†’ C(t, q, u, y).

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem PointwiseComposition.CategoricalRiceShapiro.Evaluator.persistenceFormula_eval_iff {M : Type u_1} [FFL.ORingStructure M] [Mโ†“[โ„’โ‚’แตฃ] โŠง* ๐ˆ๐Ž๐ฉ๐ž๐ง] (q : โ„•) (s : M) :
      (FFL.FirstOrder.Semiformula.Evalb ![s]) (persistenceFormula q) โ†” โˆ€ (t u y : M), s โ‰ค t โ†’ (FFL.FirstOrder.Semiformula.Evalb ![s, โ†‘q, u, y]) โ†‘evalnCertificateFormula โ†’ (FFL.FirstOrder.Semiformula.Evalb ![t, โ†‘q, u, y]) โ†‘evalnCertificateFormula

      The persistence formula defines the actual persistence predicate.

      source
      theorem PointwiseComposition.CategoricalRiceShapiro.Evaluator.models_inductionScheme_univ {M : Type u_1} [FFL.ORingStructure M] [Mโ†“[โ„’โ‚’แตฃ] โŠง* ๐๐€] :
      Mโ†“[โ„’โ‚’แตฃ] โŠง* FFL.FirstOrder.Arithmetic.InductionScheme โ„’โ‚’แตฃ Set.univ

      The full induction scheme of ๐๐€ holds in every model of ๐๐€.

      source
      theorem PointwiseComposition.CategoricalRiceShapiro.Evaluator.certificate_persistence_of_stage_induction {M : Type u_1} [FFL.ORingStructure M] [Mโ†“[โ„’โ‚’แตฃ] โŠง* ๐๐€] [Mโ†“[โ„’โ‚’แตฃ] โŠง* ๐ˆ๐Ž๐ฉ๐ž๐ง] (q : โ„•) (hzero : โˆ€ (t u y : M), 0 โ‰ค t โ†’ (FFL.FirstOrder.Semiformula.Evalb ![0, โ†‘q, u, y]) โ†‘evalnCertificateFormula โ†’ (FFL.FirstOrder.Semiformula.Evalb ![t, โ†‘q, u, y]) โ†‘evalnCertificateFormula) (hsucc : โˆ€ (s : M), (โˆ€ (t u y : M), s โ‰ค t โ†’ (FFL.FirstOrder.Semiformula.Evalb ![s, โ†‘q, u, y]) โ†‘evalnCertificateFormula โ†’ (FFL.FirstOrder.Semiformula.Evalb ![t, โ†‘q, u, y]) โ†‘evalnCertificateFormula) โ†’ โˆ€ (t u y : M), s + 1 โ‰ค t โ†’ (FFL.FirstOrder.Semiformula.Evalb ![s + 1, โ†‘q, u, y]) โ†‘evalnCertificateFormula โ†’ (FFL.FirstOrder.Semiformula.Evalb ![t, โ†‘q, u, y]) โ†‘evalnCertificateFormula) (s t u y : M) :
      s โ‰ค t โ†’ (FFL.FirstOrder.Semiformula.Evalb ![s, โ†‘q, u, y]) โ†‘evalnCertificateFormula โ†’ (FFL.FirstOrder.Semiformula.Evalb ![t, โ†‘q, u, y]) โ†‘evalnCertificateFormula

      Conditional internal induction for certificate persistence at a fixed standard index q. The base and successor premises are explicit; this is not a proof of persistence. The induction is the successor induction of ๐๐€ applied to persistenceFormula q.

      The stage-zero premise #

      At stage 0 no evaluator history has a row, so no certificate holds there and the premise is vacuous. Its conclusion is the hzero hypothesis of certificate_persistence_of_stage_induction verbatim.

      The theory assumptions are ๐๐€ and ๐๐€โป. The second is an elaboration requirement of the statement, since the standard-index cast ((q : โ„•) : M) needs it; it is no additional strength, ๐๐€ proving every axiom of ๐๐€โป. Wherever ๐ˆ๐Ž๐ฉ๐ž๐ง is in scope the instance is synthesized and the argument is invisible.

      source
      theorem PointwiseComposition.CategoricalRiceShapiro.Evaluator.evalnCertificateFormula_natCode_persist_of_stage_zero {M : Type u_1} [FFL.ORingStructure M] [Mโ†“[โ„’โ‚’แตฃ] โŠง* ๐๐€] [Mโ†“[โ„’โ‚’แตฃ] โŠง* ๐๐€โป] (q : โ„•) (t u y : M) :
      0 โ‰ค t โ†’ (FFL.FirstOrder.Semiformula.Evalb ![0, โ†‘q, u, y]) โ†‘evalnCertificateFormula โ†’ (FFL.FirstOrder.Semiformula.Evalb ![t, โ†‘q, u, y]) โ†‘evalnCertificateFormula

      Stage-zero persistence. For a standard index q, a certificate at stage 0 persists to every stage t, vacuously: at stage 0 the certificate is refutable. The proof uses no persistence theorem, no induction, no constructor-number hypothesis and no smaller-index hypothesis, so the theorem holds at every standard index.