Blueprint Summary🔗

Overview

Total entries52completed: 39; deps incomplete: 11; sorries: 0; no proof: 2

Ready now1Entries with an actionable next formalization step.

Fully closed39Local code and prerequisite closure are both complete.

Actionable priorities1Entries ready now and already unlocking downstream work.

Actionable priorities (1)

R1(Theorem)

Ready for proof work.

tag: paper proofstage: proofstatement: ready to formalizedirect uses: 3downstream unlocks: 12proof: ready to formalize

Entry index (52)

Theorems52completed: 39; deps incomplete: 11; sorries: 0; no proof: 2

Informal-only entries2

Theorem / Proposition / Lemma / Corollary Index (52)

R2(Theorem)
Associated lean decls (2)
- NaturalLatents.General.race_frullani_log_one_add
- NaturalLatents.General.race_expected_log_one_add_laplace
R8(Theorem)
Associated lean decls (6)
R7(Theorem)
Associated lean decls (2)
- NaturalLatents.General.race_scalar_log_mean_of_stable_laplace
- NaturalLatents.General.race_scalar_log_ratio_law_of_stable_laplace
«C1.5»(Theorem)
Associated lean decls (3)
«C1.1»(Theorem)
Associated lean decls (7)
K12(Theorem)
Associated lean decls (6)
«L4.1»(Theorem)
Associated lean decls (6)
R11(Theorem)
Associated lean decls (6)
«P5.1»(Theorem)
Associated lean decls (6)
«PC5.3»(Theorem)
Associated lean decls (7)
«P5.4»(Theorem)
Associated lean decls (3)
«Q3.1»(Theorem)
Associated lean decls (5)
K13(Theorem)
Associated lean decls (7)
«M5.4»(Theorem)
Associated lean decls (1)
- NaturalLatents.General.T_le_of_connected
«PC4.0»(Theorem)
Associated lean decls (9)
«T6.6»(Theorem)
Associated lean decls (4)
«M5.1»(Theorem)
«E3.2»(Theorem)
Associated lean decls (2)
- _private.NaturalLatents.Upstream.Connected.0.stoch_to_det.restrict_score_gap
- _private.NaturalLatents.Upstream.Connected.0.stoch_to_det.glueLatent_score
«S1.1»(Theorem)
Associated lean decls (3)
«C1.2»(Theorem)
Associated lean decls (5)
«T6.5»(Theorem)
Associated lean decls (14)
«P5.5»(Theorem)
Associated lean decls (1)
- NaturalLatents.General.mismatch_payment
«T6.4»(Theorem)
Associated lean decls (5)
R4(Theorem)
Associated lean decls (4)
«PC4.4»(Theorem)
Associated lean decls (4)
«PC5.2»(Theorem)
Associated lean decls (4)
R3(Theorem)
Associated lean decls (4)
«PC5.1»(Theorem)
Associated lean decls (1)
- NaturalLatents.General.pairCharge_price
«P5.3»(Theorem)
Associated lean decls (4)
«T6.3»(Theorem)
Associated lean decls (3)
R9(Theorem)
Associated lean decls (3)
R10(Theorem)
Associated lean decls (4)
R1(Theorem)
«PC4.1»(Theorem)
Associated lean decls (10)
«E3.1»(Theorem)
Associated lean decls (2)
- stoch_to_det.ComponentDecomp
- stoch_to_det.exists_componentDecomp
«A2.1»(Theorem)
Associated lean decls (5)
«PC4.3»(Theorem)
Associated lean decls (4)
«E3.4»(Theorem)
Associated lean decls (2)
- NaturalLatents.General.extension_of_connected
- stoch_to_det.reduce_to_connected
«C1.4»(Theorem)
Associated lean decls (3)
R6(Theorem)
Associated lean decls (8)
«PC4.2»(Theorem)
Associated lean decls (8)
«S1.3»(Theorem)
Associated lean decls (3)
«E3.3»(Theorem)
Associated lean decls (4)
«C1.3»(Theorem)
Associated lean decls (2)
- stoch_to_det.contact_hypercontractive
- NaturalLatents.General.contact_hessian_cube_test
«S1.4»(Theorem)
Associated lean decls (2)
- stoch_to_det.contact_support_eq
- NaturalLatents.General.exists_setup_of_connected
«T6.1»(Theorem)
Associated lean decls (4)
«T6.2»(Theorem)
Associated lean decls (6)
«S1.2»(Theorem)
Associated lean decls (3)
«P5.2»(Theorem)
Associated lean decls (1)
- stoch_to_det.bhattacharyya_le
«A2.2»(Theorem)
Associated lean decls (2)
- NaturalLatents.General.affinity_bound
- NaturalLatents.General.affinityPoly_pos
R5(Theorem)
Associated lean decls (2)
- NaturalLatents.General.race_arrival_mass_ae_summable
- NaturalLatents.General.race_reference_isPMF
«PC4.5»(Theorem)
Associated lean decls (8)

By parent groups (10)

The cap on the race price. (2)

The table form. (6)

«T6.2»(Theorem)
Associated lean decls (6)
«T6.1»(Theorem)
Associated lean decls (4)
«T6.3»(Theorem)
Associated lean decls (3)
«T6.4»(Theorem)
Associated lean decls (5)
«T6.5»(Theorem)
Associated lean decls (14)
«T6.6»(Theorem)
Associated lean decls (4)

The extension by component split. (4)

«E3.3»(Theorem)
Associated lean decls (4)
«E3.4»(Theorem)
Associated lean decls (2)
- NaturalLatents.General.extension_of_connected
- stoch_to_det.reduce_to_connected
«E3.1»(Theorem)
Associated lean decls (2)
- stoch_to_det.ComponentDecomp
- stoch_to_det.exists_componentDecomp
«E3.2»(Theorem)
Associated lean decls (2)
- _private.NaturalLatents.Upstream.Connected.0.stoch_to_det.restrict_score_gap
- _private.NaturalLatents.Upstream.Connected.0.stoch_to_det.glueLatent_score

The affinity bound. (2)

«A2.2»(Theorem)
Associated lean decls (2)
- NaturalLatents.General.affinity_bound
- NaturalLatents.General.affinityPoly_pos
«A2.1»(Theorem)
Associated lean decls (5)

The setup on a connected support. (4)

«S1.2»(Theorem)
Associated lean decls (3)
«S1.4»(Theorem)
Associated lean decls (2)
- stoch_to_det.contact_support_eq
- NaturalLatents.General.exists_setup_of_connected
«S1.3»(Theorem)
Associated lean decls (3)
«S1.1»(Theorem)
Associated lean decls (3)

The mismatch payment. (5)

«P5.2»(Theorem)
Associated lean decls (1)
- stoch_to_det.bhattacharyya_le
«P5.3»(Theorem)
Associated lean decls (4)
«P5.5»(Theorem)
Associated lean decls (1)
- NaturalLatents.General.mismatch_payment
«P5.4»(Theorem)
Associated lean decls (3)
«P5.1»(Theorem)
Associated lean decls (6)

The pair charge. (9)

Contact moments and the feasible Hessian. (5)

«C1.3»(Theorem)
Associated lean decls (2)
- stoch_to_det.contact_hypercontractive
- NaturalLatents.General.contact_hessian_cube_test
«C1.4»(Theorem)
Associated lean decls (3)
«C1.2»(Theorem)
Associated lean decls (5)
«C1.1»(Theorem)
Associated lean decls (7)
«C1.5»(Theorem)
Associated lean decls (3)

The exponential race. (11)

R5(Theorem)
Associated lean decls (2)
- NaturalLatents.General.race_arrival_mass_ae_summable
- NaturalLatents.General.race_reference_isPMF
R6(Theorem)
Associated lean decls (8)
R1(Theorem)
R10(Theorem)
Associated lean decls (4)
R9(Theorem)
Associated lean decls (3)
R3(Theorem)
Associated lean decls (4)
R4(Theorem)
Associated lean decls (4)
R11(Theorem)
Associated lean decls (6)
R7(Theorem)
Associated lean decls (2)
- NaturalLatents.General.race_scalar_log_mean_of_stable_laplace
- NaturalLatents.General.race_scalar_log_ratio_law_of_stable_laplace
R8(Theorem)
Associated lean decls (6)
R2(Theorem)
Associated lean decls (2)
- NaturalLatents.General.race_frullani_log_one_add
- NaturalLatents.General.race_expected_log_one_add_laplace

The pricing. (2)

«M5.1»(Theorem)
«M5.4»(Theorem)
Associated lean decls (1)
- NaturalLatents.General.T_le_of_connected

Dependency insights

Statement-used entries51Entries reused in statement dependencies.

Tracked parent groups10Grouped health rollups for parents with more than one child entry.

Most used in statements (51)

«C1.1»(Theorem)

Reverse dependencies recorded in statement dependencies.

statement uses: 6proof uses: 0direct uses: 6downstream unlocks: 20
Associated lean decls (7)
«PC4.0»(Theorem)

Reverse dependencies recorded in statement dependencies.

statement uses: 6proof uses: 0direct uses: 6downstream unlocks: 11
Associated lean decls (9)
«C1.2»(Theorem)

Reverse dependencies recorded in statement dependencies.

statement uses: 5proof uses: 0direct uses: 5downstream unlocks: 19
Associated lean decls (5)
«C1.4»(Theorem)

Reverse dependencies recorded in statement dependencies.

statement uses: 3proof uses: 0direct uses: 3downstream unlocks: 19
Associated lean decls (3)
R1(Theorem)

Reverse dependencies recorded in statement dependencies.

statement uses: 3proof uses: 0direct uses: 3downstream unlocks: 12
R3(Theorem)

Reverse dependencies recorded in statement dependencies.

statement uses: 3proof uses: 0direct uses: 3downstream unlocks: 11
Associated lean decls (4)
«A2.2»(Theorem)

Reverse dependencies recorded in statement dependencies.

statement uses: 3proof uses: 0direct uses: 3downstream unlocks: 10
Associated lean decls (2)
- NaturalLatents.General.affinity_bound
- NaturalLatents.General.affinityPoly_pos
«PC4.1»(Theorem)

Reverse dependencies recorded in statement dependencies.

statement uses: 3proof uses: 0direct uses: 3downstream unlocks: 10
Associated lean decls (10)
«Q3.1»(Theorem)

Reverse dependencies recorded in statement dependencies.

statement uses: 3proof uses: 0direct uses: 3downstream unlocks: 10
Associated lean decls (5)
«E3.1»(Theorem)

Reverse dependencies recorded in statement dependencies.

statement uses: 3proof uses: 0direct uses: 3downstream unlocks: 7
Associated lean decls (2)
- stoch_to_det.ComponentDecomp
- stoch_to_det.exists_componentDecomp
Show all 41 more statement-used entries
- «C1.5»(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 18
  Associated lean decls (3)
- R2(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 12
  Associated lean decls (2)
  - NaturalLatents.General.race_frullani_log_one_add
  - NaturalLatents.General.race_expected_log_one_add_laplace
- R6(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 10
  Associated lean decls (8)
- «S1.1»(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 10
  Associated lean decls (3)
- «P5.1»(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 9
  Associated lean decls (6)
- «PC4.3»(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 8
  Associated lean decls (4)
- «S1.2»(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 8
  Associated lean decls (3)
- «S1.3»(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 7
  Associated lean decls (3)
- R11(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 6
  Associated lean decls (6)
- «L4.1»(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 6
  Associated lean decls (6)
- «P5.5»(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 6
  Associated lean decls (1)
  - NaturalLatents.General.mismatch_payment
- «S1.4»(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 6
  Associated lean decls (2)
  - stoch_to_det.contact_support_eq
  - NaturalLatents.General.exists_setup_of_connected
- «C1.3»(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 20
  Associated lean decls (2)
  - stoch_to_det.contact_hypercontractive
  - NaturalLatents.General.contact_hessian_cube_test
- R5(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 11
  Associated lean decls (2)
  - NaturalLatents.General.race_arrival_mass_ae_summable
  - NaturalLatents.General.race_reference_isPMF
- «A2.1»(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 11
  Associated lean decls (5)
- R7(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 10
  Associated lean decls (2)
  - NaturalLatents.General.race_scalar_log_mean_of_stable_laplace
  - NaturalLatents.General.race_scalar_log_ratio_law_of_stable_laplace
- R4(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 9
  Associated lean decls (4)
- R8(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 9
  Associated lean decls (6)
- «PC4.2»(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 9
  Associated lean decls (8)
- R9(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 8
  Associated lean decls (3)
- «P5.2»(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 8
  Associated lean decls (1)
  - stoch_to_det.bhattacharyya_le
- R10(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 7
  Associated lean decls (4)
- «P5.3»(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 7
  Associated lean decls (4)
- «P5.4»(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 7
  Associated lean decls (3)
- «PC4.4»(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 7
  Associated lean decls (4)
- K12(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 6
  Associated lean decls (6)
- «E3.2»(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 6
  Associated lean decls (2)
  - _private.NaturalLatents.Upstream.Connected.0.stoch_to_det.restrict_score_gap
  - _private.NaturalLatents.Upstream.Connected.0.stoch_to_det.glueLatent_score
- «PC4.5»(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 6
  Associated lean decls (8)
- «PC5.1»(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 6
  Associated lean decls (1)
  - NaturalLatents.General.pairCharge_price
- «PC5.2»(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 6
  Associated lean decls (4)
- K13(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 5
  Associated lean decls (7)
- «E3.3»(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 5
  Associated lean decls (4)
- «M5.1»(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 5
- «PC5.3»(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 5
  Associated lean decls (7)
- «E3.4»(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 4
  Associated lean decls (2)
  - NaturalLatents.General.extension_of_connected
  - stoch_to_det.reduce_to_connected
- «M5.4»(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 4
  Associated lean decls (1)
  - NaturalLatents.General.T_le_of_connected
- «T6.1»(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 3
  Associated lean decls (4)
- «T6.2»(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 3
  Associated lean decls (6)
- «T6.3»(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 3
  Associated lean decls (3)
- «T6.4»(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 2
  Associated lean decls (5)
- «T6.5»(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
  Associated lean decls (14)

Group health (10)

The exponential race.race

Grouped view over entries sharing the same parent.

total: 11closed: 4local-only: 6ready: 1blocked: 0incomplete Lean: 0unlock score: 105

Next: R1 stage: proofdownstream unlocks: 12
Contact moments and the feasible Hessian.contact

Grouped view over entries sharing the same parent.

total: 5closed: 5local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 96

Next: no ready child currently unlocks downstream work.
The pair charge.«pair-charge»

Grouped view over entries sharing the same parent.

total: 9closed: 9local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 68

Next: no ready child currently unlocks downstream work.
The mismatch payment.payment

Grouped view over entries sharing the same parent.

total: 5closed: 5local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 37

Next: no ready child currently unlocks downstream work.
The setup on a connected support.setup

Grouped view over entries sharing the same parent.

total: 4closed: 4local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 31

Next: no ready child currently unlocks downstream work.
The extension by component split.extension

Grouped view over entries sharing the same parent.

total: 4closed: 4local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 22

Next: no ready child currently unlocks downstream work.
The affinity bound.affinity

Grouped view over entries sharing the same parent.

total: 2closed: 2local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 21

Next: no ready child currently unlocks downstream work.
The table form.«table-form»

Grouped view over entries sharing the same parent.

total: 6closed: 2local-only: 4ready: 0blocked: 0incomplete Lean: 0unlock score: 12

Next: no ready child currently unlocks downstream work.
The cap on the race price.cap

Grouped view over entries sharing the same parent.

total: 2closed: 2local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 11

Next: no ready child currently unlocks downstream work.
The pricing.assembly

Grouped view over entries sharing the same parent.

total: 2closed: 0local-only: 1ready: 0blocked: 1incomplete Lean: 0unlock score: 9

Next: no ready child currently unlocks downstream work.