Assuming large cardinal axioms, which real numbers are in $L[\mathrm{cf}]$, where $\mathrm{cf}$ is the cofinality function on ordinals?

$L[\mathrm{cf}]$ is the minimal inner model that 'knows' the cofinality of every ordinal in V, or more precisely, $∀α\,\{(β,\mathrm{cf}(β)):β<α\}∈L[\mathrm{cf}]$. Cofinality in $L[\mathrm{cf}]$ need not equal cofinality in $V$.

I have a solution to a simpler problem:
Theorem: A real number is in $L$[Card] iff it is in the minimal inner model with a proper class of measurable cardinals (assuming the sharp for this model exists). Here, Card is the cardinality function.
Corollary (under the same assumption): The theory of $(L[\mathrm{Card}],∈,\mathrm{Card})$ is $Δ^1_3$.
Proof sketch of the theorem: Starting with the minimal inner model $M$ with a proper class of measurable cardinals, iterate the first measurable cardinal until it becomes $ω_1^V$, the second until it becomes $ω_2^V$, and so on for every regular successor cardinal in $V$. For the converse, every $ω_{α+ω}$ can be shown to be measurable in HOD^L[Card] with $\{ω_{α+1}, ω_{α+2}, ω_{α+3}, ...\}$ Prikry generic over HOD^L[Card].

For the cofinality problem, my conjecture is to use a model $M$ (closely related to $L[\mathrm{cf}]$) such that:
nonmeasurable regular cardinals in $M$ have $V$-cofinality $ω$,
measurable cardinals of order $α$ in $M$ have $V$-cofinality $ω_{α+1}$ (or $ω_α$ if $α$ is weakly inaccessible (in $V$) plus a finite ordinal),
and $M$ is obtained by iterating away the least mouse with a measure concentrating on cardinals with $o(κ)=κ$, and iterating the measures until the above correspondences hold. However, I do not know whether this works, or for that matter, whether the theory of $L[\mathrm{cf}]$ is generically absolute.

An extension of the problem is to set $\mathrm{cf}(κ)=κ+α$ iff $κ$ is weakly $α$-Mahlo, which is well-defined for $α≤κ^+$. A $κ^+$-Mahlo $κ$ is called greatly Mahlo. For comparison, a limit ordinal $κ$ has cofinality $≥α$ iff for every (infinite) regular $β<α$, ordinals of cofinality $β$ are stationary below $κ$. (Also, if singular $κ$ pose a problem, I would be happy to see a solution for this extension with $\mathrm{cf}(κ)$ restricted to regular $κ$.) It appears plausible that the construction using orders of measurability can be extended to this problem, with weakly greatly Mahlo cardinals corresponding to $M$-cardinals that are strong up to a measurable. If that is the case, then under large cardinal axioms, all reals in $L[\mathrm{cf}]$ are still $Δ^1_3$.

Assuming large cardinal axioms, which real numbers are in $L[\mathrm{cf}]$, where $\mathrm{cf}$ is the cofinality function on ordinals?

$L[\mathrm{cf}]$ is the minimal inner model that 'knows' the cofinality of every ordinal in V, or more precisely, $∀α\,\{(β,\mathrm{cf}(β)):β<α\}∈L[\mathrm{cf}]$. Cofinality in $L[\mathrm{cf}]$ need not equal cofinality in $V$.

I have a solution to a simpler problem:
Theorem: A real number is in $L$[Card] iff it is in the minimal inner model with a proper class of measurable cardinals (assuming the sharp for this model exists). Here, Card is the cardinality function.
Corollary (under the same assumption): The theory of $(L[\mathrm{Card}],∈,\mathrm{Card})$ is $Δ^1_3$.
Proof sketch of the theorem: Starting with the minimal inner model $M$ with a proper class of measurable cardinals, iterate the first measurable cardinal until it becomes $ω_1^V$, the second until it becomes $ω_2^V$, and so on for every regular successor cardinal in $V$. For the converse, every $ω_{α+ω}$ can be shown to be measurable in HOD^L[Card] with $\{ω_{α+1}, ω_{α+2}, ω_{α+3}, ...\}$ Prikry generic over HOD^L[Card].
Additional details on the proof: If $M$ is iterated until we get $M'$ with measurable cardinals matching regular $V$-cardinals except that the next measurable cardinal after $ω_α^V$ is $ω_{α+ω}^V$, then $S = (ω_{α+1},ω_{α+2},...)$ is Prikry generic over $M'$ since if a measurable cardinal is iterated, a cofinal sequence of length $ω$ of its past values is Prikry generic. Now, $\mathrm{HOD}^{L[\mathrm{Card}]}⊂\mathrm{HOD}^{M'[S]}=M'$ and $S∈L[\mathrm{Card}]$, so $S$ is also Prikry generic over $\mathrm{HOD}^{L[\mathrm{Card}]}$.

For the cofinality problem, my conjecture is to use a model $M$ (closely related to $L[\mathrm{cf}]$) such that:
nonmeasurable regular cardinals in $M$ have $V$-cofinality $ω$,
measurable cardinals of order $α$ in $M$ have $V$-cofinality $ω_{α+1}$ (or $ω_α$ if $α$ is weakly inaccessible (in $V$) plus a finite ordinal),
and $M$ is obtained by iterating away the least mouse with a measure concentrating on cardinals with $o(κ)=κ$, and iterating the measures until the above correspondences hold. However, I do not know whether this works, or for that matter, whether the theory of $L[\mathrm{cf}]$ is generically absolute.

An extension of the problem is to set $\mathrm{cf}(κ)=κ+α$ iff $κ$ is weakly $α$-Mahlo, which is well-defined for $α≤κ^+$. A $κ^+$-Mahlo $κ$ is called greatly Mahlo. For comparison, a limit ordinal $κ$ has cofinality $≥α$ iff for every (infinite) regular $β<α$, ordinals of cofinality $β$ are stationary below $κ$. (Also, if singular $κ$ pose a problem, I would be happy to see a solution for this extension with $\mathrm{cf}(κ)$ restricted to regular $κ$.) It appears plausible that the construction using orders of measurability can be extended to this problem, with weakly greatly Mahlo cardinals corresponding to $M$-cardinals that are strong up to a measurable. If that is the case, then under large cardinal axioms, all reals in $L[\mathrm{cf}]$ are still $Δ^1_3$.

Assuming large cardinal axioms, which real numbers are in $L[\mathrm{cf}]$, where $\mathrm{cf}$ is the cofinality function on ordinals?

$L[\mathrm{cf}]$ is the minimal inner model that 'knows' the cofinality of every ordinal in V, or more precisely, $∀α\,\{(β,\mathrm{cf}(β)):β<α\}∈L[\mathrm{cf}]$. Cofinality in $L[\mathrm{cf}]$ need not equal cofinality in $V$.

I have a solution to a simpler problem:
Theorem: A real number is in $L$[Card] iff it is in the minimal inner model with a proper class of measurable cardinals (assuming the sharp for this model exists). Here, Card is the cardinality function.
Corollary (under the same assumption): The theory of $(L[\mathrm{Card}],∈,\mathrm{Card})$ is $Δ^1_3$.
Proof sketch of the theorem: Starting with the minimal inner model $M$ with a proper class of measurable cardinals, iterate the first measurable cardinal until it becomes $ω_1^V$, the second until it becomes $ω_2^V$, and so on for every regular successor cardinal in $V$. For the converse, every $ω_{α+ω}$ can be shown to be measurable in HOD^L[Card] with $\{ω_{α+1}, ω_{α+2}, ω_{α+3}, ...\}$ Prikry generic over HOD^L[Card].

For the cofinality problem, my conjecture is to use a model $M$ (closely related to $L[\mathrm{cf}]$) such that:
nonmeasurable regular cardinals in $M$ have $V$-cofinality $ω$,
measurable cardinals of order $α$ in $M$ have $V$-cofinality $ω_{α+1}$ (or $ω_α$ if $α$ is weakly inaccessible (in $V$) plus a finite ordinal),
and $M$ is obtained by iterating away the least mouse with a measure concentrating on cardinals with $o(κ)=κ$, and iterating the measures until the above correspondences hold. However, I do not know whether this works, or for that matter, whether the theory of $L[\mathrm{cf}]$ is generically absolute.

An extension of the problem is to set $\mathrm{cf}(κ)=κ+α$ iff $κ$ is weakly $α$-Mahlo, which is well-defined for $α≤κ^+$. A $κ^+$-Mahlo $κ$ is called greatly Mahlo. For comparison, an ordinal has cofinality $ω_{α+2}$ iff ordinals of cofinality $ω_{α+1}$ are stationary below it. (Also, if singular $κ$ pose a problem, I would be happy to see a solution for this extension with $\mathrm{cf}(κ)$ restricted to regular $κ$.) It appears plausible that the construction using orders of measurability can be extended to this problem, with weakly greatly Mahlo cardinals corresponding to $M$-cardinals that are strong up to a measurable. If that is the case, then under large cardinal axioms, all reals in $L[\mathrm{cf}]$ are still $Δ^1_3$.

Assuming large cardinal axioms, which real numbers are in $L[\mathrm{cf}]$, where $\mathrm{cf}$ is the cofinality function on ordinals?

$L[\mathrm{cf}]$ is the minimal inner model that 'knows' the cofinality of every ordinal in V, or more precisely, $∀α\,\{(β,\mathrm{cf}(β)):β<α\}∈L[\mathrm{cf}]$. Cofinality in $L[\mathrm{cf}]$ need not equal cofinality in $V$.

I have a solution to a simpler problem:
Theorem: A real number is in $L$[Card] iff it is in the minimal inner model with a proper class of measurable cardinals (assuming the sharp for this model exists). Here, Card is the cardinality function.
Corollary (under the same assumption): The theory of $(L[\mathrm{Card}],∈,\mathrm{Card})$ is $Δ^1_3$.
Proof sketch of the theorem: Starting with the minimal inner model $M$ with a proper class of measurable cardinals, iterate the first measurable cardinal until it becomes $ω_1^V$, the second until it becomes $ω_2^V$, and so on for every regular successor cardinal in $V$. For the converse, every $ω_{α+ω}$ can be shown to be measurable in HOD^L[Card] with $\{ω_{α+1}, ω_{α+2}, ω_{α+3}, ...\}$ Prikry generic over HOD^L[Card].

For the cofinality problem, my conjecture is to use a model $M$ (closely related to $L[\mathrm{cf}]$) such that:
nonmeasurable regular cardinals in $M$ have $V$-cofinality $ω$,
measurable cardinals of order $α$ in $M$ have $V$-cofinality $ω_{α+1}$ (or $ω_α$ if $α$ is weakly inaccessible (in $V$) plus a finite ordinal),
and $M$ is obtained by iterating away the least mouse with a measure concentrating on cardinals with $o(κ)=κ$, and iterating the measures until the above correspondences hold. However, I do not know whether this works, or for that matter, whether the theory of $L[\mathrm{cf}]$ is generically absolute.

An extension of the problem is to set $\mathrm{cf}(κ)=κ+α$ iff $κ$ is weakly $α$-Mahlo, which is well-defined for $α≤κ^+$. A $κ^+$-Mahlo $κ$ is called greatly Mahlo. For comparison, a limit ordinal $κ$ has cofinality $≥α$ iff for every (infinite) regular $β<α$, ordinals of cofinality $β$ are stationary below $κ$. (Also, if singular $κ$ pose a problem, I would be happy to see a solution for this extension with $\mathrm{cf}(κ)$ restricted to regular $κ$.) It appears plausible that the construction using orders of measurability can be extended to this problem, with weakly greatly Mahlo cardinals corresponding to $M$-cardinals that are strong up to a measurable. If that is the case, then under large cardinal axioms, all reals in $L[\mathrm{cf}]$ are still $Δ^1_3$.