TauLib · API Book VI

TauLib.BookVI.Consumer.Reproduction

TauLib.BookVI.Consumer.Reproduction

Sexual reproduction: recombination functor and the second distinction.

Registry Cross-References

  • [VI.D49] Recombination Functor — RecombinationFunctor

  • [VI.T26] Sex as Second Distinction — sex_is_second_distinction

Cross-Book Authority

  • Book II, Part III: lemniscate 𝕃 = S¹ ∨ S¹ (gamete channels via two lobes)

  • Book II, Part II: τ³ fibration (haploid/diploid cycling on fiber T²)

Ground Truth Sources

  • Book VI Chapter 36 (2nd Edition): Sexual Reproduction

Tau.BookVI.Reproduction.RecombinationFunctor

source structure Tau.BookVI.Reproduction.RecombinationFunctor :Type

[VI.D49] Recombination Functor: binary input, stochastic output. Gamete fusion: two haploid inputs → one diploid output. The two lemniscate lobes (Book II, Part III) provide two independent channels for gamete production.

  • input_arity : ℕ Number of inputs (gametes).

  • arity_eq : self.input_arity = 2 Binary: exactly 2 inputs.

  • haploid_fusion : Bool Haploid fusion produces diploid.

  • stochastic : Bool Crossover is stochastic.

  • channels : ℕ Number of gamete channels (= lemniscate lobes).

  • channels_eq : self.channels = 2 Exactly 2 channels.

Instances For

Tau.BookVI.Reproduction.instReprRecombinationFunctor

source instance Tau.BookVI.Reproduction.instReprRecombinationFunctor :Repr RecombinationFunctor

Equations

  • Tau.BookVI.Reproduction.instReprRecombinationFunctor = { reprPrec := Tau.BookVI.Reproduction.instReprRecombinationFunctor.repr }

Tau.BookVI.Reproduction.instReprRecombinationFunctor.repr

source def Tau.BookVI.Reproduction.instReprRecombinationFunctor.repr :RecombinationFunctor → ℕ → Std.Format

Equations

  • One or more equations did not get rendered due to their size. Instances For

Tau.BookVI.Reproduction.recomb

source def Tau.BookVI.Reproduction.recomb :RecombinationFunctor

Equations

  • Tau.BookVI.Reproduction.recomb = { input_arity := 2, arity_eq := Tau.BookVI.Reproduction.recomb._proof_1, channels := 2, channels_eq := Tau.BookVI.Reproduction.recomb._proof_1 } Instances For

Tau.BookVI.Reproduction.recombination_is_functor

source theorem Tau.BookVI.Reproduction.recombination_is_functor :recomb.input_arity = 2 ∧ recomb.haploid_fusion = true ∧ recomb.stochastic = true ∧ recomb.channels = 2

Tau.BookVI.Reproduction.SecondDistinction

source structure Tau.BookVI.Reproduction.SecondDistinction :Type

[VI.T26] Sex as Second Distinction. Life’s first distinction (VI.D04): self vs non-self. Sex introduces a second: self vs other-self. This is a refinement (level 1) of the base distinction.

  • first : String First distinction: self vs non-self (VI.D04).

  • second : String Second distinction: self vs other-self.

  • refinement_level : ℕ Refinement level (0 = base, 1 = first refinement).

  • level_eq : self.refinement_level = 1 Exactly level 1.

Instances For

Tau.BookVI.Reproduction.instReprSecondDistinction

source instance Tau.BookVI.Reproduction.instReprSecondDistinction :Repr SecondDistinction

Equations

  • Tau.BookVI.Reproduction.instReprSecondDistinction = { reprPrec := Tau.BookVI.Reproduction.instReprSecondDistinction.repr }

Tau.BookVI.Reproduction.instReprSecondDistinction.repr

source def Tau.BookVI.Reproduction.instReprSecondDistinction.repr :SecondDistinction → ℕ → Std.Format

Equations

  • One or more equations did not get rendered due to their size. Instances For

Tau.BookVI.Reproduction.second_dist

source def Tau.BookVI.Reproduction.second_dist :SecondDistinction

Equations

  • Tau.BookVI.Reproduction.second_dist = { refinement_level := 1, level_eq := Tau.BookVI.Reproduction.second_dist._proof_1 } Instances For

Tau.BookVI.Reproduction.sex_is_second_distinction

source theorem Tau.BookVI.Reproduction.sex_is_second_distinction :second_dist.refinement_level = 1 ∧ second_dist.first = “self_nonself” ∧ second_dist.second = “self_otherself”