Pipeline-generated

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Regulated generalized-entropy model — Examples

1 · Prerequisites

2 · Summary

3 · Logical flowchart

4 · Definitions, postulates, theorems and proofs

RemarkRemark: AI-adaptedProof: AI-adaptedprecheck passverified 2026-10-22 (gpt-6.1-sol)Open item page →

Generalized entropy requires a separate physical inequality

Physical scope

A conditional finite-data comparison for the regulated generalized-entropy definition at one fixed section and in one declared scheme, with a common finite geometric contribution, one-dimensional input factor, and two constant finite-regulator state sequences. It shows only that the additive definition and geometric area information do not impose monotonicity on the outside entropy. The sequence labels do not denote physical time, and the item asserts no empirical result or violation of a physical generalized second law.

Statement

Fix one section $Σ$ , one declared scheme, and one regulator-label sequence $(Λ_{n})_{n \geq 1}$ . For each $r \in {0, 1}$ , take $H_{i n, n} = C$ and $H_{o u t, n} = C^{2}$ with their standard inner products and bases $(1)$ and $(f_{0}, f_{1})$ . In the ordered product basis $(1 \otimes f_{0}, 1 \otimes f_{1})$ , use the joint density matrices $ρ_{n}^{(0)} = diag (1 / 2, 1 / 2)$ and $ρ_{n}^{(1)} = diag (1, 0)$ for every $n \geq 1$ . Use the same finite geometric value $S_{g r a v, n} [Σ] = G$ for both sequences and all $n$ , where $G$ is a fixed finite real value with units $J K^{- 1}$ . The index $r$ labels these two sequences only; it is neither physical time nor regulator order. Define $S_{g e n}^{r e n, r} [Σ] : = \lim_{n \to \infty} (S_{g r a v, n} [Σ] + S_{o u t, n}^{(r)})$ . These limits exist and satisfy

$S_{g e n}^{r e n, 1} [Σ] - S_{g e n}^{r e n, 0} [Σ] = - k_{B} \log 2 < 0.$

The fixed-section definition supplies no ordered parameter set $J \subseteq R$ , cut family $s \mapsto Σ_{s}$ , state family $s \mapsto (ρ_{s, n})_{n \geq 1}$ , or comparison inequality such as $S_{g e n}^{r e n} [Σ_{s_{2}}] \geq S_{g e n}^{r e n} [Σ_{s_{1}}]$ for $s_{1} \leq s_{2}$ in $J$ . The displayed comparison is between independently specified model-data sequences, not a physical evolution. The restricted classical area-increase result and the restricted area-entropy calibration result do not supply an inequality for the outside-state entropy.

Statement references

Specified regulated generalized entropy

Conditional restricted classical area increase

Conditional area entropy coefficient with free offset

Facts & Assumptions

Given: One fixed section $Σ$ , one declared scheme, and a regulator-label sequence $(Λ_{n})_{n \geq 1}$ . For each comparison label $r \in {0, 1}$ and every $n \geq 1$ , take $H_{i n, n} = C$ and $H_{o u t, n} = C^{2}$ in their standard inner products and bases $(1)$ and $(f_{0}, f_{1})$ . In the ordered product basis $(1 \otimes f_{0}, 1 \otimes f_{1})$ , set $ρ_{n}^{(0)} = diag (1 / 2, 1 / 2)$ and $ρ_{n}^{(1)} = diag (1, 0)$ . The same specified finite geometric contribution $S_{g r a v, n} [Σ] = G$ is used for both sequences and all $n$ . The labels $r = 0, 1$ index these two sequences only; $n$ is the regulator index, and no cut family or physical evolution is supplied.

[F1]

Specified regulated generalized entropy: at each finite regulator, $S_{g e n} [Σ] = S_{g r a v} [Σ] + S_{o u t}$ , with the geometric and finite-normalization data fixed by the declared scheme; the physical Boltzmann constant satisfies $k_{B} > 0$ and has units $J K^{- 1}$ .

[F2]

Finite-regulator outside density and entropy: the outside density is the partial trace over the input factor, and its entropy is $- k_{B} \sum_{j} λ_{j} \log λ_{j}$ over eigenvalues counted with multiplicity, using natural logarithms and $0 \log 0 : = 0$ .

[F3]

Density operator: a density operator on a nonzero finite-dimensional complex inner-product space is a non-negative endomorphism of trace one.

[F4]

Non-negative and positive operators: a non-negative operator is self-adjoint and has non-negative quadratic form on every vector.

[F5]

The natural logarithm as the inverse of the exponential function: for $x > 0$ , $\log x$ is the unique real number $y$ with $\exp (y) = x$ .

[F6]

The real exponential function and the number $e$ by a power series: $\exp (0) = 1$ by the defining power series.

[F7]

The exponential function is strictly increasing: $\exp$ is strictly increasing on $R$ .

[F8]

The exponential is positive and satisfies $\exp (- x) = 1 / \exp (x)$ : for real $x$ , $\exp (- x) = 1 / \exp (x)$ .

[F9]

Conditional restricted classical area increase: under its stated ${A C}_{ω}$ , smooth classical Einstein–Maxwell, null-energy, affine-completeness, and persistent-compact-cut hypotheses, the classical horizon area is nondecreasing. Its conclusion contains no outside quantum entropy.

[F10]

Conditional area entropy coefficient with free offset: under its exact selected stationary-family, ${A C}_{ω}$ , reversible-heat, and reduced-temperature assumptions, the calibrated entropy has coefficient $k_{B} c^{3} / (4 G_{N} ℏ)$ and a free additive offset. It makes no statement about an outside state or an ordered cut/state family.

[A1]

For every $n$ , the same finite geometric contribution $G$ is used in both sequences; their outside matrices are the only changed inputs in this comparison.

[A2]

The Axiom of Countable Choice ( ${A C}_{ω}$ ): every sequence $(X_{n})_{n \geq 1}$ of nonempty sets has a function $f$ with $f (n) \in X_{n}$ . This premise is carried only with the exact contextual area-theorem inputs [F9]–[F10]; steps 1.1–2.2 use no choice.

Proof

1.1givenF2F3F4algebra

The matrices $ρ_{n}^{(0)}$ and $ρ_{n}^{(1)}$ are self-adjoint for every $n$ . For every $z = (z_{0}, z_{1}) \in C^{2}$ , $⟨ ρ_{n}^{(0)} z, z ⟩ = (∣ z_{0} ∣^{2} + ∣ z_{1} ∣^{2}) / 2 \geq 0$ and $⟨ ρ_{n}^{(1)} z, z ⟩ = ∣ z_{0} ∣^{2} \geq 0$ ; each diagonal trace is one. Hence both matrices are density operators by [F3]–[F4]. Since the input factor is one-dimensional, its partial trace has one summand and returns the same matrix in each sequence at every $n$ by [F2].

1.2givenF1

The index $n$ in [F1] is the regulator index within each named sequence; it is distinct from the comparison label $r$ . The definition assigns the sequence at the fixed section $Σ$ and declares no ordered family of cuts $Σ_{s}$ , no corresponding state family $ρ_{s, n}$ , and no comparison inequality between different cuts. Thus the two sequences in [given] are not states related by a physical evolution.

2.1givenF2F5F6F7F8step 1.1algebra

For every $n$ , the eigenvalues of $ρ_{n}^{(0)}$ are $1 / 2, 1 / 2$ , and those of $ρ_{n}^{(1)}$ are $1, 0$ . By [F5]–[F7], $\log 1 = 0$ and $\log 2 > 0$ : $\exp (0) = 1 < 2 = \exp (\log 2)$ , so strict increase gives $0 < \log 2$ . By [F8], $\exp (- \log 2) = 1 / 2$ , and uniqueness in [F5] gives $\log (1 / 2) = - \log 2$ . Therefore [F2] yields $S_{o u t, n}^{(0)} = k_{B} \log 2$ and $S_{o u t, n}^{(1)} = 0$ for every $n$ .

3.1givenF1A1step 2.1algebra

For every $n$ , [F1] and [A1] give $S_{g e n, n}^{(1)} [Σ] - S_{g e n, n}^{(0)} [Σ] = S_{o u t, n}^{(1)} - S_{o u t, n}^{(0)} = - k_{B} \log 2 < 0$ , because $k_{B} > 0$ . Both generalized-entropy sequences are constant in $n$ , so they converge finitely and their renormalized values satisfy the same strict inequality. It is only a comparison of the two model-data sequences in [given], not an asserted evolution or a counterexample to an independently specified physical inequality.

4.1F1F9F10A2step 3.1step 1.2∎

The comparison in step 3.1 has one fixed section and two independently specified state-data sequences; it has no cut parameter or physical ordering. Under the countable-choice premise [A2], [F9] gives a conditional area inequality only for its stated smooth classical null-cut family, while [F10] gives an entropy coefficient and free offset only on its selected stationary family. Neither supplier specifies the state family or an inequality for the outside entropy required to compare different cuts. Therefore these fixed-section assignments and the two restricted geometric results do not establish a monotonicity inequality across any physical cut family. Such a claim requires separately specified cut and state data and a proof of the corresponding inequality.

Remarks

The calculation compares two independent sequences of model data at one fixed section. A monotonicity claim for a specified family of cuts would require an ordered parameter set $J \subseteq R$ , a section $Σ_{s}$ and a regulator/state/geometric sequence at each $s \in J$ , finite convergence at each $s$ if renormalized values are used, and a proof that $S_{g e n}^{r e n} [Σ_{s_{2}}] \geq S_{g e n}^{r e n} [Σ_{s_{1}}]$ whenever $s_{1} \leq s_{2}$ in $J$ . None of this comparison data or inequality is part of the fixed-section definition or supplied by the finite example.

5 · Examples, experiments and counterexamples

None yet.